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

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

Full description

Saved in:
Bibliographic Details
Main Authors: Lakas, A., Blair, G.S., Chetwynd, A.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Formal specifications
Logic
Monitoring
Real time systems
Time factors
Timing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/IWSSD.1996.501149