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

Abderrahmane Lakas, Gordon S. Blair, Amanda Chetwynd

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

In this paper 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.

Original languageEnglish
Title of host publicationProceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996
PublisherAssociation for Computing Machinery
Pages75-84
Number of pages10
ISBN (Electronic)0818673613, 9780818673610
DOIs
Publication statusPublished - Mar 22 1996
Externally publishedYes
Event8th International Workshop on Software Specification and Design, IWSSD 1996 - Velen, Germany
Duration: Mar 22 1996Mar 23 1996

Publication series

NameProceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996

Other

Other8th International Workshop on Software Specification and Design, IWSSD 1996
Country/TerritoryGermany
CityVelen
Period3/22/963/23/96

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Specification and verification of real-time properties using LOTOS and SQTL'. Together they form a unique fingerprint.

Cite this