Abstract
This paper presents a toolset we built for supporting verification of Statemate 1 designs. Statemate is a widely used design tool for embedded control applications. Designs are translated into finite state machines which are optimized and then verified by symbolic model checking. To express requirement specifications the visual formalism of symbolic timing diagrams is used. Their semantics is given by translation into temporal logic. If the model checker generates a counterexample, it is retranslated into either a symbolic timing diagram or a stimulus for the Statemate simulator.
Part of this work has been funded by the Commission of the European Communities under the ESPRIT project 20897, SACRES and the German BMBF project KORSYS, grant number 01-IS-519-E-0
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
S.B. Akers: Binary decision diagrams. In: Transactions on Computers, No. 6 in Vol. C-27, IEEE (1978) 509–516
K. S. Brace, Richard L. Rudell and Randal E. Bryant: Efficient implementation of a BDD package. In: Proceedings 27th Design Automation Conference, Orlando, Florida, ACM/IEEE (1990) 40–45
J.R. Burch, E.M. Clarke, K.L. McMillan and D.L. Dill: Sequential circuit verification using symbolic model checking. In: Design Automation Conference ACM/IEEE (1990)
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and Jim Hwang: Symbolic model checking: 1020 states and beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer science (1990)
W. Damm, U. Brockmeyer, H.J. Holberg, G. Wittich and M. Eckrich: Einsatz formaler Methoden zur Erhöhung der Sicherheit eingebetteter Systeme im KFZ. VDI/VW Gemeinschaftstagung (1997)
W. Damm, H. Hungar, B. Josko and A. Pnueli: A Compositional Real-Time Semantics of STATEMATE Designs. In: Proceedings of COMPOS 97, edt. H. Langmaack and W.P. de Roever, Springer Verlag, to appear 1998
W. Damm, B. Josko, R. Schlör: Specification and verification of VHDL-based system-level hardware designs. In: E. Börger, editor, Specification and Validation Methods. Oxford University Press, (1995) 331–410
K. Feyerabend and B. Josko: A Visual Formalism for Real Time Requirement Specifications, Transformation-Based Reactive Systems Development. In: Proceedings of 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, edt. M. Bertran and T. Rus. Lecture Notes in Computer Science Vol. 1231. Springer Verlag (1997) 156–168
T. Filkorn, SIEMENS AG: Applications of Formal Verification in Industrial Automation and Telecommunication. In: Proceedings of Workshop on Formal Design of Safety Critical Embedded Systems, (1997)
D. Harel: Statecharts: A Visual Formalism for Complex Systems. In: Science of Computer Programming 8, (1987)
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 of complex reactive systems. In: IEEE Transactions on Software Engineering, (1990) 403–414
D. Harel and A. Naamad: The STATEMATE Semantics of Statecharts. In: ACM transactions on software engineering and methodology, Vol 5 No 4 (1996)
D. Harel, A. Pnueli, J.P. Schmidt and R.Sherman: On the Formal Semantics of StateCharts. In: Proceedings of First IEEE, Symposium on Logic in Computer Science, (1987)
D. Harel and M. Politi: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. i-LOGIX INC., Three Riverside Drive, Andover, MA 01810, Part No, D-1100-43 (1996)
E. Mikk, Y. Lakhnech, C. Petersohn and M. Siegel: On Formal Semantics of Statecharts as Supported by STATEMATE. In: Proceedings of BCS-FACS Northern Formal Methods Workshop, (1997)
S. Owre, N. Shankar and J.M. Rushby: A Tutorial on Specification and Verification Using PVS. In: Computer Science Laboratory, SRI Int., (1993)
R. Schlör: Symbolic Timing Diagrams: A visual formalism for specification and verification of system-level hardware designs. In: Dissertation (to appear), Universität Oldenburg, (1998)
R. Schlör and W. Damm: Specification and Verification of System-Level Hardware Designs using Timing Diagrams. In: EDAC-EUROASIC, (1993)
VIS: A system for Verification and Synthesis. The VIS Group. In Proceedings of the 8th International Conference on Computer Aided Verification, Springer Lecture Notes in Computer Science, Vol. 1102, Edited by R. Alur and T. Henzinger, New Brunswick, NJ (1996) 428–432
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brockmeyer, U., Wittich, G. (1998). Tamagotchis need not die — Verification of statemate designs. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054174
Download citation
DOI: https://doi.org/10.1007/BFb0054174
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive