Abstract
The Statemate Verification Environment supports requirement analysis and specification development of embedded controllers as part of the Statemate product offering of I-Logix, Inc. This paper discusses key enhancements of the prototype tool reported in [2,5] in order to enable full scale industrial usage of the tool-set. It thus reports on a successfully completed technology transfer from a prototype tool-set to a commercial offering. The discussed enhancements are substantiated with performance results all taken from real industrial applications of leading companies in automotive and avionics.
Chapter PDF
Similar content being viewed by others
References
Bienmüller, T., Bohn, J., Brinkmann, H., Brockmeyer, U., Damm, W., Hungar, H., Jansen, P.: Verification of automotive control units. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 319–341. Springer, Heidelberg (1999)
Bienmüller, T., Brockmeyer, U., Damm, W., Döhmen, G., Eßmann, C., Holberg, H.J., Hungar, H., Josko, B., Schlör, R., Wittich, G., Wittke, H., Clements, G., Rowlands, J., Sefton, E.: Formal Verification of an AvionicsApplication using Abstraction and Symbolic Model Checking. In: Redmill, F., Anderson, T. (eds.) Towards System Safety – Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK. Safety-Critical Systems Club, pp. 150–173. Springer, Heidelberg (1999)
Bohn, J., Brockmeyer, U., Essmann, C., Hungar, H.: SMI – system modeling interface, draft version 0.1. Technical report, Kuratorium OFFIS, e.V., Oldenburg (1999)
Brockmeyer, U.: Verifikation von Statemate Designs. PhD thesis, Carl von Ossietzky Universität Oldenburg (December 1999)
Brockmeyer, U., Wittich, G.: Tamagotchis Need Not Die – Verification of STATEMATE Designs. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 217–231. Springer, Heidelberg (1998)
Clarke, E., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. Formal Methods in System Design 10(1), 47–71 (1997)
Damm, W., Brockmeyer, U., Holberg, H.-J., Wittich, G., Eckrich, M.: Einsatz formaler Methoden zur Erhöhung der Sicherheit eingebetteter Systeme im KFZ, VDI/VW Gemeinschaftstagung (1997)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. In: FMOODS 1999 IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (1999)
Feyeraband, K., Josko, B.: A visual formalism for real time requirement specifications. In: Rus, T., Bertrán, M. (eds.) AMAST-ARTS 1997, ARTS 1997, and AMAST-WS 1997. LNCS, vol. 1231, pp. 156–168. Springer, Heidelberg (1997)
Filkorn, T.: Applications on Formal Verification in Industrial Automation and Telecommunication. In: Workshop on Formal Design of Safety Critical Embedded Systems (April 1997)
The VIS Group. VIS: A System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996), VIS 1.3 is available from the VIS home-page: http://www-cad.eecs.Berkeley.EDU/~vis
Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. Technical Report CS95-31, TheWeizmann Institute of Science, Rehovot (1995)
Hoffmann, J., Holberg, H.-J., Schlör, R.: Industrieller Einsatz formaler Verifikationsmethoden (February 2000); To appear in ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Frankfurt/Main
Mikk, E., Lakhnech, Y., Siegel, M.: Hierarchical automata as model for statecharts. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol. 1345. Springer, Heidelberg (1997)
Mikk, E., Lakhnech, Y., Siegel, M.: Towards Efficient Modelchecking Statecharts: A Statecharts to Promela Compiler (April 1997)
Pilarski, F.: Cost effectiveness of formal methods in the development of avionics systems at Aerospatiale. In: 17th Digital Avionics Systems Conference, Seattle, WA. Springer, Heidelberg (1998)
Somenzi, F.: CU Decision Diagram Package (1998), CUDD 2.3.0 is available from http://vlsi.Colorado.EDU/~fabio
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bienmüller, T., Damm, W., Wittke, H. (2000). The Statemate Verification Environment. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_45
Download citation
DOI: https://doi.org/10.1007/10722167_45
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive