On the Formal Verification of Systems of Synchronous Software Components

Günther H, Milius S, Möller O (2012)


Publication Type: Conference contribution

Publication year: 2012

Journal

Publisher: Springer-verlag

Edited Volumes: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Series: Lecture Notes Computer Science

City/Town: Berlin Heidelberg

Book Volume: 7612

Pages Range: 291-304

Conference Proceedings Title: Computer Safety, Reliability, and Security

Event location: Magdeburg

ISBN: 978-3-642-33677-5

URI: http://link.springer.com/chapter/10.1007%2F978-3-642-33678-2_25

DOI: 10.1007/978-3-642-33678-2_25

Abstract

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.

Authors with CRIS profile

Involved external institutions

How to cite

APA:

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.

MLA:

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.

BibTeX: Download