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


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


Go to the contact details of the person in charge of this page

This page in german. Diese Seite auf deutsch.