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

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

Abstract

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.

Published
1995-06-30
How to Cite
Andersen, J., Kristensen, C., & Skou, A. (1995). Specification and Automated Verification of Real-Time Behaviour —A Case Study. BRICS Report Series, 2(60). https://doi.org/10.7146/brics.v2i60.19961