Abstract
This paper presents a reference semantics for a verication tool currently under development allowing to verify temporal properties of embedded control sys- tems modelled using the StateMate system. The semantics reported divert from others reported in the literature [24] by faithfully modelling the semantics as supported in the StateMate simulation tool. It divers from the recent paper by Harel and Naamad [8] by providing a compositional semantics, a prerequisite for the support of compositional verication methods, and by the degree of math- ematical rigour. We use a variant of synchronous transition systems introduced by Manna and Pnueli [18] as base model for our semantics.
The StateMate modelling language constructs covered in this paper are Activity charts, modelling the functional decomposition of a design into subunits called activities as well as the information flow between these, and Statecharts, modelling reactive behaviour using the well established approach of hierarchically organized state-machines. We strive for a verication approach which is compositional w.r.t. the decomposition of systems into subsystems. This will allow activities of “reasonable” complexity to be veried using symbolic model checking [5], [4], [19]. Larger activities will be veried on the basis of proof-systems relating properties of individual activities to properties of compound activities, using the well known assumption commitment paradigm [1], [21], [15]. A key topic for this paper is the construction of so called compositional models, which are “rich enough” to model the StateMate parallel composition by intersection of the innite traces generated by the components of the parallel composition. Roughly, compositional models have to provide room for padding arbitrary (but still “legal”) environment interactions into computations of a component. Alternatively, the construction of compositional models can be phrased as a requirement on the model to support a sufficiently rich class of observables for assumption-commitment style reasoning to be complete. In this sense, this paper derives the set of atomic propositions included as observables in the assumption- commitment style temporal logic supported by the verication tool.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Martín Abadi and Leslie Lamport. Composing specifications. In Jaco W. de Bakker, Willem-Paul de Roever, and Grzegorz Rozenberg, editors, Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness, Lecture Notes in Computer Science430, pages 1–41. Springer-Verlag, 1990.
A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79(9):1270–1282, September 1991.
U. Brockmeyer and G. Wittich. Tamagotchis need not die-verification of Statemate designs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), 1998. (To appear).
J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Sequential circuit verification using symbolic model checking. In ACM/IEEE Design Automation Conference, June 1990.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 428–439, June 1990.
Werner Damm and Johannes Helbig. Linking visual formalisms: A compositional proof system for statecharts based on symbolic timing diagrams. In Proc. IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET’94), pages 337–356, 1994.
D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot. STATEMATE: A working environment for the development od complex reactive systems. IEEE Transactions on Software Engineering, 16:403–414, 1990.
D. Harel and A. Naamad. The STATEMATE semantics of statecharts. Technical Report CS95-31, The Weizmann Institute of Science, Rehovot, 1995.
D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman. On the formal semantics of statecharts. In Proceeding IEEE Symposium on Logic in Computer Science, pages 54–64, 1987.
David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
David Harel. On visual formalism. CACM, 31:514–530, 1988.
David Harel and Amir Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI Series F13, pages 477–498. Springer-Verlag, 1985.
David Harel and Michal Politi. Modeling reactive systems with statecharts: The statemate approach. Technical report, 1996.
J.J.M. Hooman, S. Ramesh, and W.P. de Roever. A compositional axiomatization of statecharts. TCS, 101:289–335, 1992.
Bernhard Josko. Modular Specification and Verification of Reactive Systems. Habilitationsschrift, Universität Oldenburg, 1993.
Andrea Maggiolo-Schettini, Andriano Peron, and Simone Tini. Equivalences of statecharts. In CONCUR 96, Seventh Int. Conf. on Concurrency Theory, Pisa, LNCS 1119, pages 687–702. Springer-Verlag, 1996.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer-Verlag, 1992.
Kenneth L. McMillian. Symbolic Model Checking. An approach to the state explosion problem. PhD thesis, Carnegie Mellon University, Pittsburgh, 1992.
A. Pnueli and M. Shalev. What is in a step: On the semantics of statecharts. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 526. Springer-Verlag, 1991.
Amir Pnueli. In transition from global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI Series, Vol. F13, pages 123–144. Springer-Verlag, 1985.
Gerard Tel and Friedemann Mattern. The derivation of distributed termination detection algorithms from garbage collection schemes. In E.H.L. Aarts, J. van Leeuwen, and M. Rem, editors, PARLE’91 Parallel Architectures and Languages, Volume I: Parallel Architectures and Algorithms, Lecture Notes in Computer Science 505, pages 137–149. Springer-Verlag, 1991.
Andrew C. Uselton and Scott A. Smolka. A compositional semantics for statecharts using labeled transition systems. In CONCUR 94, LNCS 836, pages 2–17. Springer-Verlag, 1994.
M. van der Beek. A comparison of statechart variants. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pages 128–148. Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Josko, B., Hungar, H., Pnueli, A. (1998). A Compositional Real-time Semantics of STATEMATE Designs. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_8
Download citation
DOI: https://doi.org/10.1007/3-540-49213-5_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65493-3
Online ISBN: 978-3-540-49213-9
eBook Packages: Springer Book Archive