On the Formal Verification of Systems of Synchronous Software Components

Conference contribution

Publication Details

Author(s): Günther H, Milius S, Möller O
Title edited volumes: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher: Springer-verlag
Publishing place: Berlin Heidelberg
Publication year: 2012
Title of series: Lecture Notes Computer Science
Volume: 7612
Conference Proceedings Title: Computer Safety, Reliability, and Security
Pages range: 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 Authors / FAU Editors

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

External institutions with authors

Technische Universität Wien

How to cite

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.


Last updated on 2018-07-08 at 23:23