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 / 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
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11583/2500720
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo