Specifying and Reasoning about Generic Real-Time Requirements - A Case Study
R. Gotzhein, M. Kronenburg, C. Peper
SFB 501 Report 15/1996, Department of Computer Sciences, University of Kaiserslautern, Germany, 1996
Abstract
A non-trivial real-time requirement obeying a pattern that can be found in various instantiations in the application domain building automation and which is therefore called generic, is investigated in detail. Starting point is a description of a real-time problem in natural language augmented by a diagram, in a style often found in requirements documents. Step by step, this description is made more precise and finally transformed into a surprisingly concise formal specification, written in real-time temporal logic with customized operators. We reason why this formal specification precisely captures the original description - as far as this is feasible due to the lack of precision of natural language.
Full paper
- ps.gz (721kb)
Superordinated page: Year 1996 | |
Feedback | |
Go to the contact details of the person in charge of this page |
Deutsch | |
This page in german. Diese Seite auf deutsch. |