A framework for formal verification of systems of synchronous components
Günther H, Hedayati R, Löding H, Milius S, Möller O, Peleska J, Sulzmann M, Zechner A (2012)
Publication Type: Conference contribution
Publication year: 2012
Publisher: fortiss GmbH
Edited Volumes: Tagungsband - Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme VIII, MBEES 2012
City/Town: München
Pages Range: 145-154
Conference Proceedings Title: Tagungsband Modellbasierte Entwicklung eingebetteter Systeme (MBEES12)
Event location: Dagstuhl
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 in a rely-guarantee style logic. Formal verification of global system properties is then done transforming a network of contracts to PROMELA/SPIN. Synchronous components are implemented in SCADE, and contract validation is done by transforming the contracts into synchronous observers and using the SCADE Design Verifier for formal verification. We also discuss first experiences from an ongoing industrial case study applying our approach.
Authors with CRIS profile
Involved external institutions
Technische Universität Wien / Vienna University of Technology
Austria (AT)
Universität Bremen
Germany (DE)
Hochschule Karlsruhe – Technik und Wirtschaft
Germany (DE)
Austria (AT)
Universität Bremen
Germany (DE)
Hochschule Karlsruhe – Technik und Wirtschaft
Germany (DE)
How to cite
APA:
Günther, H., Hedayati, R., Löding, H., Milius, S., Möller, O., Peleska, J.,... Zechner, A. (2012). A framework for formal verification of systems of synchronous components. In Tagungsband Modellbasierte Entwicklung eingebetteter Systeme (MBEES’12) (pp. 145-154). Dagstuhl: München: fortiss GmbH.
MLA:
Günther, Henning, et al. "A framework for formal verification of systems of synchronous components." Proceedings of the MBEES 2012, Dagstuhl München: fortiss GmbH, 2012. 145-154.
BibTeX: Download