Title :
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
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;
Conference_Titel :
Factory Communication Systems, 1995. WFCS '95, Proceedings., 1995 IEEE International Workshop on
Conference_Location :
Leysin
Print_ISBN :
0-7803-3059-5
DOI :
10.1109/WFCS.1995.482655
