Specifying and Reasoning about Generic Real-Time Requirements - A Case Study
SFB 501 Report 15/1996, Department of Computer Sciences, University of Kaiserslautern, Germany, 1996
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.
- ps.gz (721kb)
|Superordinated page: Year 1996|
|Go to the contact details of the person in charge of this page|
|This page in german. Diese Seite auf deutsch.|