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.



Zu den Kontaktdetails des Verantwortlichen dieser Seite

This page in english. Diese Seite auf englisch.