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
Formal Specification and Verification of the Real-Time Scheduler in FIP
L Durante;A Valenzano
1995
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 discussedFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
