Formal specification and verification of the real-time scheduler in FIP

Author

Durante, L. ; Sisto, R. ; Valenzano, A.

Author_Institution

Dipartimento di Autom. e Inf., Politecnico di Torino, Italy

fYear

1995

fDate

4-6 Oct 1995

Firstpage

99

Lastpage

106

Abstract

ET-LOTOS is a timed and probabilistic extension of the standard specification language LOTOS. In this paper, it is shown how such an extension can be used to model the behaviour of the real time scheduler of the FIP protocol. Since ET-LOTOS has been designed specifically to enable direct performance evaluation from formal specifications, the possibility of analyzing the performance and the correctness of FIP real time scheduler directly from the specification is also discussed

Keywords

formal specification; formal verification; performance evaluation; protocols; real-time systems; specification languages; ET-LOTOS; FIP protocol; direct performance evaluation; formal specification; formal verification; probabilistic extension; real time scheduler; real-time scheduler; standard specification language LOTOS; timed extension; Analytical models; Formal specifications; Formal verification; Performance analysis; Protocols; Stochastic processes; Time sharing computer systems; Upper bound;

fLanguage

English

Publisher

ieee

Conference_Titel

Factory Communication Systems, 1995. WFCS '95, Proceedings., 1995 IEEE International Workshop on

Conference_Location

Leysin

Print_ISBN

0-7803-3059-5

Type

conf

DOI

10.1109/WFCS.1995.482655

Filename

482655