Specification and verification of real-time properties using LOTOS and SQTL

Author

Lakas, Abderrahmane ; Blair, Gordon S. ; Chetwynd, Amanda

Author_Institution

Dept. of Comput., Lancaster Univ., UK

fYear

1996

Firstpage

75

Lastpage

84

Abstract

We present a new approach to the formal specification of distributed real-time systems using the formal description technique LOTOS together with a real-time temporal logic SQTL. This approach characterized by a separation of concerns, aims to construct abstractly a model from the a functional specification according to real-time constraints. The functional behaviour is described in LOTOS without regard for the time critical constraints. The specification is then extended with precise real-time properties written in SQTL. We present a method to generate a timing event scheduler from the properties in order to monitor the functional behaviour. The model of event schedulers is based on timed automata and intended to be used for an automata-based verification technique

Keywords

automata theory; distributed processing; formal specification; formal verification; real-time systems; specification languages; system monitoring; temporal logic; timing; LOTOS formal description technique; SQTL real-time temporal logic; abstract model construction; automata-based verification technique; distributed real-time systems; formal specification; functional behaviour monitoring; functional specification; real-time constraints; real-time property specification; real-time property verification; time critical constraints; timed automata; timing event scheduler; Algebra; Automata; Delay; Distributed computing; Formal specifications; Logic; Monitoring; Real time systems; Stochastic processes; Time factors; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Specification and Design, 1996., Proceedings of the 8th International Workshop on

Conference_Location

Schloss Velen

Print_ISBN

0-8186-7361-3

Type

conf

DOI

10.1109/IWSSD.1996.501149

Filename

501149