Günther H, Milius S, Möller O (2012)
Publication Type: Conference contribution
Publication year: 2012
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
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.
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