Archivio Istituzionale della RicercaET-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 / Durante, Luca; Sisto, Riccardo; Valenzano, Adriano. - STAMPA. - (1995), pp. 99-106. (Intervento presentato al convegno 1995 IEEE International Workshop on Factory Communication Systems, WFCS '95 tenutosi a Leysin, Switzerland nel 4-6 October 1995) [10.1109/WFCS.1995.482655].
Formal Specification and Verification of the Real-time Scheduler in FIP
DURANTE, LUCA;SISTO, Riccardo;VALENZANO, ADRIANO
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 discussed
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2500720
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo