Abstract
In the context of large scale industrial installations, model checking often fails to tap its full potential because of a missing link between a system’s specification and its functional and non-functional requirements, like safety. Our work bridges this gap by providing a translation from the formal specification language Object-Z to the SMV model checker input language to combine their advantages.
This paper focuses on the translation of the object-oriented features of Object-Z: operation promotion and communication between objects. We demonstrate the feasibility of our approach using the example of the TWIN Elevator system and embed the translation process in the industrial software production workflow.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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
Amnell, T.: Code Synthesis for Timed Automata. Thesis, Uppsala University (2003)
The Community Z Tools project (2006), http://czt.sourceforge.net/
Derrick, J., Smith, G.: Linear temporal logic and Z refinement. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116. Springer, Heidelberg (2004)
Duke, R., Rose, G.: Formal Object-Oriented Specification Using Object-Z. Cornerstones of Computing. MacMillan (2000)
International Organization for Standardization: ISO/IEC 13568:2002: Information technology – Z formal specification notation – Syntax, type system and semantics, http://www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573
Kammüller, F.: Interactive Theorem Proving in Software Engineering. In: Habilitationsschrift, Technische Universität Berlin (2006)
Kammüller, F., Preibusch, S.: An Industrial Application of Symbolic Model Checking – The TWIN-Elevator Case Study. In: Informatik Forschung und Entwicklung. Springer, Heidelberg (accepted for publication, 2007)
Liu, S.: Formal Engineering for Industrial Software Development. Springer, Heidelberg (2004)
McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1995)
Preibusch, S.: TWIN Elevator System, Concise Object-Z Specification (2007) http://preibusch.de/projects/TWIN/Concise_OZ
Preibusch, S.: TWIN Elevator System, Concise Object-Z Specification (Translation to SMV) (2007), http://preibusch.de/projects/TWIN/Concise_OZ_Translation_SMV
Smith, G.: The Object-Z Specification Language. In: Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)
Smith, G., Kammüller, F., Santen, T.: Encoding Object-Z in Isabelle/HOL. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272. Springer, Heidelberg (2002)
Smith, G., Wildman, L.: Model Checking Z Specifications Using SAL. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455. Springer, Heidelberg (2005)
Smith, G., Winter, K.: Proving temporal properties of Z specifications using abstraction. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651. Springer, Heidelberg (2003)
Software Design Group, MIT Computer Science and Artificial Intelligence Laboratory. The Alloy Analyzer (2007), http://alloy.mit.edu/
ThyssenKrupp Elevator. TWIN Report (2005), http://www.twin.thyssenkrupp-elevator.de/?&L=1
Winter, K., Duke, R.: Model Checking Object-Z using ASM. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335. Springer, Heidelberg (2002)
The World Wide Web Virtual Library: The Z notation. Tool support (2005), http://vl.zuser.org/#tools
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Preibusch, S., Kammüller, F. (2008). Checking the TWIN Elevator System by Translating Object-Z to SMV. In: Leue, S., Merino, P. (eds) Formal Methods for Industrial Critical Systems. FMICS 2007. Lecture Notes in Computer Science, vol 4916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79707-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-79707-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79706-7
Online ISBN: 978-3-540-79707-4
eBook Packages: Computer ScienceComputer Science (R0)