Specification and Automated Verification of Real-Time Behaviour —A Case Study - Andersen, Jørgen H.; Kristensen, Carsten H.; Skou, Arne (BRICS Report Series, 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. Keywords: Control system analysis; formal specification; formal verification; real-time systems; standards.