Specification and Automated Verification of Real-Time Behaviour - A Case Study

Jørgen H. Andersen
Carsten H. Kristensen
Arne Skou

December 1995


In this paper we sketch a method for specification and automatic verification of real-time software properties. The method combines the IEC 848 norm and the recent specification techniques TCCS (Timed Calculus of Communicating Systems) and TML (Timed Modal Logic) -- supported by an automatic verification tool, EPSILON. The method is illustrated by modelling a small real-life steam generator example and subsequent automated analysis of its properties.

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.