Abstract
We present a method for symbolic model checking of μ-Charts, a Statecharts dialect with instantaneous broadcast communication. Due to this communication concept, μ-Charts satisfy the perfect synchrony hypothesis. The well-known causality conflicts that arise under instantaneous feedback from negative trigger conditions are resolved semantically through oracle signals. We have implemented a prototypical tool that translates μ-Charts specifications into μ-calculus formulae. These formulae are checked against temporal specifications using a μ-calculus verifier.
This work is partially funded by the German Federal Ministry of Education and Research (BMBF) as part of the compound project “KorSys”.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
G. Berry. Real Time Programming: Special Purpose or General Purpose Languages. Information Processing 89, 1989.
G Berry and G. Gonthier. The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation. Technical Report 842, INRIA, 1988.
A. Biere. Eine Methode zur μ-Kalkül-Modellprüfung. Slides for the AKFM from 23.05.96, GI/ITG-Fachgespräch “Formale Beschreibungstechniken für verteilte Systeme” (in German), 1996.
D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231–274, 1987.
J.J.M. Hooman, S. Ramesh, and W.P. de Roever. A Compositional Axiomatization of Statecharts. Theoretical Computer Science, 101:289–335, 1992.
C. Huizing and W.-P. de Roever. Introduction to Design Choices in the Semantics of Statecharts. Information Processing Letters, 37, 1991.
i-Logix Inc., 22 Third Avenue, Burlington, Mass. 01803, U.S.A. Languages of Statemate, 1990.
K. Inoue, M. Koshimura, and R. Hasegawa. Embedding Negation as Failure into a Model Generation Theorem Prover. In D. Kapur, editor, CADE-11, number 607 in Lecture Notes in Artificial Intelligence, pages 400–415, 1992.
F. Maraninchi. Operational and Compositional Semantics of Synchronous Automaton Compositions. volume 630 of Lecture Notes in Computer Science, pages 550–564. Springer-Verlag, 1992.
F. Maraninchi and N. Halbwachs. Compositional Semantics of Non-deterministic Synchronous Languages. ESOP'96, 1996.
D. Nazareth, F. Regensburger, and P. Scholz. Mini-Statecharts: A Lean Version of Statecharts. Technical Report TUM-I9610, Technische Universität München, D-80290 München, 1996.
J. Philipps and P. Scholz. The Tao of Statecharts. 1996. To appear in: TAP-SOFT'97.
J. Philipps and T. Yoneda. Symbolic Model Checking of Statecharts. Technical Report FTS-95-37, IEICE, 1995.
A. Pnueli and M. Shalev. What is in a Step: On the Semantics of Statecharts. In T. Ito and A.R. Meyer, editors, Proccedings of the “Theoretical Aspects in Computer Software 91”, volume 526 of Lecture Notes in Computer Science, pages 244–264. Springer-Verlag, 1991.
P. Scholz. An Extended Version of Mini-Statecharts. Technical Report TUM-I9628, Technische Universität München, D-80290 München, 1996.
P. Scholz. A Light-Weight Formalism for the Specification of Reactive Systems. 1996. SOFSEM'96.
P. Scholz, D. Nazareth, and F. Regensburger. Mini-Statecharts: A Compositional Way to Model Parallel Systems. 1996. PDCS'96.
M. von der Beeck. A Comparison of Statecharts Variants. volume 863 of Lecture Notes in Computer Science, pages 128–148. Springer, 1.994.
L. Wall and R.L. Schwartz. Programming in perl. Carl Hanser, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Philipps, J., Scholz, P. (1997). Formal verification of statecharts with instantaneous chain reactions. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035391
Download citation
DOI: https://doi.org/10.1007/BFb0035391
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive