On the Formal Verification of Systems of Synchronous Software Components

Beitrag bei einer Tagung

Details zur Publikation

Autorinnen und Autoren: Günther H, Milius S, Möller O
Titel Sammelwerk: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Verlag: Springer-verlag
Verlagsort: Berlin Heidelberg
Jahr der Veröffentlichung: 2012
Titel der Reihe: Lecture Notes Computer Science
Band: 7612
Tagungsband: Computer Safety, Reliability, and Security
Seitenbereich: 291-304
ISBN: 978-3-642-33677-5
ISSN: 0302-9743


Large asynchronous systems composed from synchronous components (so called GALS-globally asynchronous, locally synchronous-systems) pose a challenge to formal verification. We present an approach which abstracts components with contracts capturing the behavior by a mixture of temporal logic formulas and non-deterministic state machines. Formal verification of global system properties is then done transforming a network of contracts to model checking tools such as Promela/SPIN or UPPAAL. Synchronous components are implemented in Scade, and contract validation is done using the Scade Design Verifier for formal verification. We also discuss first experiences from an ongoing industrial case study applying our approach. © 2012 Springer-Verlag.

FAU-Autorinnen und Autoren / FAU-Herausgeberinnen und Herausgeber

Milius, Stefan apl. Prof. Dr.
Lehrstuhl für Informatik 8 (Theoretische Informatik)

Einrichtungen weiterer Autorinnen und Autoren

Technische Universität Wien


Günther, H., Milius, S., & Möller, O. (2012). On the Formal Verification of Systems of Synchronous Software Components. In Computer Safety, Reliability, and Security (pp. 291-304). Magdeburg: Berlin Heidelberg: Springer-verlag.

Günther, Henning, Stefan Milius, and Oliver Möller. "On the Formal Verification of Systems of Synchronous Software Components." Proceedings of the 31st International Conference, SAFECOMP 2012, Magdeburg Berlin Heidelberg: Springer-verlag, 2012. 291-304.


Zuletzt aktualisiert 2018-07-08 um 23:23