A framework for specification and validation of real-time systems using Circus actions. (English) Zbl 1108.68522

Sherif, Adnan; He, Jifeng; Cavalcanti, Ana; Sampaio, Augusto

Liu, Zhiming (ed.) et al., Theoretical aspects of computing – ICTAC 2004. First international colloquium, Guiyang, China, September 20–24, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-25304-1/pbk). Lecture Notes in Computer Science 3407, 478-493 (2005).

Summary: In this work we propose a framework for specification and validation of real-time programs using Circus actions. Circus is a language that combines CSP, Z, and refinement calculus constructs. We have extended Circus and its model to capture time properties, and explored the relationship between the timed and the untimed model. Here we present a framework based on the integration of the timed and untimed versions of Circus. The integration aims at building a heterogeneous model that can express time properties using the untimed model. It is useful for the validation of real-time systems properties based on techniques and tools available for untimed languages. To illustrate the use of the framework, we apply it to an alarm system controller.
For the entire collection see [Zbl 1069.68010].

MSC:

68Q60

Specification and verification (program logics, model checking, etc.)

Keywords:

Formal methods integration, formal verification, real-time systems.