Modelchecking non-functional requirements for interface specifications.
Conference paper
Kammueller, F. and Preibusch, S. 2008. Modelchecking non-functional requirements for interface specifications. European Joint Conference on Theory and Practice of Software, 2008, (Foundations of Interface technologies). Budapest 29 Mar - 06 Apr 2008
Type | Conference paper |
---|---|
Title | Modelchecking non-functional requirements for interface specifications. |
Authors | Kammueller, F. and Preibusch, S. |
Abstract | In this paper we present a combination of formal specification and mechanical analysis enabling a simple and flexible development process for interface specifications from requirements. Using the potential of temporal logic for describing non-functional requirements we derive an analysis model from functional requirements. Slightly abusing its original object-oriented incentives we employ the precision and modularity of formal specification in Object-Z for representing interface descriptions. A structure preserving translation of Object-Z specifications to the model checker SMV unifies the temporal logic specification of requirements with the analysis model. The automated verification in SMV supports a feedback loop for a stepwise improvement of the requirement specification and its analysis model. We illustrate this technique on the case study of the safety-critical TWIN elevator system. |
Research Group | Artificial Intelligence group |
Foundations of Computing group | |
Conference | European Joint Conference on Theory and Practice of Software, 2008, (Foundations of Interface technologies) |
Proceedings Title | Foundations of Interface Technologies, FIT 2008. Satellite to ETAPS’08 |
Publication process dates | |
Deposited | 02 Mar 2011 |
Output status | Published |
Web address (URL) | http://fit2008.cs.aau.dk/FIT2008Kammueller.pdf |
Language | English |
File |
https://repository.mdx.ac.uk/item/83277
Download files
44
total views11
total downloads3
views this month0
downloads this month