Checking the TWIN elevator system by translating object-Z to SMV
Article
Preibusch, S. and Kammueller, F. 2008. Checking the TWIN elevator system by translating object-Z to SMV. Lecture Notes in Computer Science. 4916, pp. 38-55. https://doi.org/10.1007/978-3-540-79707-4
Type | Article |
---|---|
Title | Checking the TWIN elevator system by translating object-Z to SMV |
Authors | Preibusch, S. and Kammueller, F. |
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. |
Research Group | Artificial Intelligence group |
Foundations of Computing group | |
Publisher | Springer |
Journal | Lecture Notes in Computer Science |
ISSN | 0302-9743 |
Publication dates | |
2008 | |
Publication process dates | |
Deposited | 18 Jan 2011 |
Output status | Published |
Copyright Statement | Post refereed version as allowed by publisher. |
Additional information | Conference details: Formal Methods for Industrial Critical Systems, 12th International Workshop, FMICS 2007. Held in Berlin, Germany, July 1-2, 2007. |
Digital Object Identifier (DOI) | https://doi.org/10.1007/978-3-540-79707-4 |
Language | English |
Series | LNCS |
First submitted version |
https://repository.mdx.ac.uk/item/8312y
Download files
43
total views10
total downloads0
views this month0
downloads this month