Open AccessSpecification and Automated Verification of Real-Time Behaviour —A Case Study
Author(s) -
Jørgen H. Andersen,
C.H. Kristensen,
Arne Skou
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i60.19961
Subject(s) - programming language , computer science , formal specification , formal methods , formal verification , sketch , embedded system , algorithm
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.