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

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

doi:10.7146/brics.v2i60.19961

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

Authors

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

DOI:

https://doi.org/10.7146/brics.v2i60.19961

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.

Downloads

Published

1995-06-30

How to Cite

Andersen, J. H., Kristensen, C. H., & 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