A framework for formal verification of systems of synchronous components

Conference contribution


Publication Details

Author(s): Günther H, Hedayati R, Löding H, Milius S, Möller O, Peleska J, Sulzmann M, Zechner A
Title edited volumes: Tagungsband - Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme VIII, MBEES 2012
Publisher: fortiss GmbH
Publishing place: München
Publication year: 2012
Conference Proceedings Title: Tagungsband Modellbasierte Entwicklung eingebetteter Systeme (MBEES’12)
Pages range: 145-154


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.



FAU Authors / FAU Editors

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


External institutions with authors

Hochschule Karlsruhe – Technik und Wirtschaft
Technische Universität Wien
Universität Bremen


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: 

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