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

Jørgen H. Andersen | Zendy; C.H. Kristensen | Zendy; Arne Skou | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Specification 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research