Formal Engineering Methods, International Conference on (1998)
Dec. 9, 1998 to Dec. 11, 1998
This paper examines the applicability of the new specification language ELOTOS in the description of real time applications. E-LOTOS is the new extended version of LOTOS, currently under consideration by the ISO/IEC committee. The paper presents the complete process of producing the formal specification of a real time scheduler from its informal description. During this process, a semi-formal model of the scheduler is first built that helps identify the critical parts of the scheduler. This model is then used as the basis for the formal specification of the scheduler. Finally, the degree at which ELOTOS has succeeded in describing the critical parts of the scheduler is examined. The chosen, real life, paradigm is the Link Active Scheduler (LAS) of the Fieldbus Foundation (FF) Data Link Layer (DLL) protocol. Its formal specification has not been presented before.
D. Gill and N. Petalidis, "The Formal Specification of the Fieldbus Foundation Link Scheduler in E-LOTOS," Formal Engineering Methods, International Conference on(ICFEM), Brisbane, Australia, 1998, pp. 200.