Specification and Automated Verification of Real-Time Behaviour —A Case Study
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.
Keywords: Control system analysis; formal specification; formal verification; real-time systems; standards.
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.