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

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Specification and verification of real-time properties using LOTOS and SQTL. / Lakas, Abderrahmane; Blair, Gordon S.; Chetwynd, Amanda.
Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996. Association for Computing Machinery, Inc, 1996. p. 75-84.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Lakas, A, Blair, GS & Chetwynd, A 1996, Specification and verification of real-time properties using LOTOS and SQTL. in Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996. Association for Computing Machinery, Inc, pp. 75-84, 8th International Workshop on Software Specification and Design, IWSSD 1996, Velen, Germany, 22/03/96.

APA

Lakas, A., Blair, G. S., & Chetwynd, A. (1996). Specification and verification of real-time properties using LOTOS and SQTL. In Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996 (pp. 75-84). Association for Computing Machinery, Inc.

Vancouver

Lakas A, Blair GS , Chetwynd A. Specification and verification of real-time properties using LOTOS and SQTL. In Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996. Association for Computing Machinery, Inc. 1996. p. 75-84

Author

Lakas, Abderrahmane ; Blair, Gordon S. ; Chetwynd, Amanda. / Specification and verification of real-time properties using LOTOS and SQTL. Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996. Association for Computing Machinery, Inc, 1996. pp. 75-84

Bibtex

@inproceedings{5ab7a6a728864cd5b4b8a4fd0e8acc53,

title = "Specification and verification of real-time properties using LOTOS and SQTL",

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.",

author = "Abderrahmane Lakas and Blair, {Gordon S.} and Amanda Chetwynd",

year = "1996",

month = mar,

day = "22",

language = "English",

pages = "75--84",

booktitle = "Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996",

publisher = "Association for Computing Machinery, Inc",

note = "8th International Workshop on Software Specification and Design, IWSSD 1996 ; Conference date: 22-03-1996 Through 23-03-1996",

}

RIS

TY - GEN

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

AU - Lakas, Abderrahmane

AU - Blair, Gordon S.

AU - Chetwynd, Amanda

PY - 1996/3/22

Y1 - 1996/3/22

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

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

M3 - Conference contribution/Paper

AN - SCOPUS:0042989064

SP - 75

EP - 84

BT - Proceedings of the 8th International Workshop on Software Specification and Design, IWSSD 1996

PB - Association for Computing Machinery, Inc

T2 - 8th International Workshop on Software Specification and Design, IWSSD 1996

Y2 - 22 March 1996 through 23 March 1996

ER -

Research