Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS

Hubert Garavel and Mihaela Sighireanu

Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems FMICS'98 (Amsterdam, The Netherlands), pages 187-230, May 1998

Abstract: Process algebras are often advocated as suitable formalisms for the specification of telecommunication protocols and distributed systems. However, despite their mathematical basis, despite standardization attempts (most notably the Formal Description Technique LOTOS), and despite an ever growing number of successful case-studies, process algebras have not yet reached a wide acceptance in industry. On the other hand, description languages such as PROMELA or SDL are quite popular, although they lack a formal semantics, which should prohibit their use for safety-critical systems. In this paper, we seek to merge the "best of both worlds" by attempting to define a "second generation Formal Description Technique" that would combine the strong theoretical foundations of process algebras with language features suitable for a wider industrial dissemination of formal methods. Taking the international standard LOTOS as a basis, we suggest several enhancements, which fall into three categories: data part, behaviour part, and modules. Our work was initiated in 1992 in the framework of the ISO/IEC Committee for the revision of the LOTOS standard. Several of our suggestions have been accepted and will be integrated into the revised standard E-LOTOS. The other suggestions are considered in the context of LOTOS NT, a variant of E-LOTOS for which a prototype compiler/model-checker is under development at INRIA.

28 pages

PDF

PostScript