Title :
A formal approach to reactive systems software: a telecommunications application in ESTEREL
Author :
Jagadeesan, Lalita Jategaonkar ; Puchol, Carlos ; von Olnhausen, J.E.
Author_Institution :
Dept. of Software Production Res., AT&T Bell Labs., Naperville, IL, USA
Abstract :
ESTEREL is a formally-defined language designed for programming reactive systems; namely, those that maintain a permanent interaction with their environment. The AT&T 5ESS telephone switching system is an example of a legacy reactive system. As a case study, we describe an implementation in ESTEREL of one feature of a 5ESS switch; this implementation has been tested in the 5ESS switch simulator. Furthermore, it has been formally verified that this implementation satisfies some safety properties required for telecommunications applications. Our case study provides some evidence that ESTEREL is suitable for programming legacy reactive systems, and that it may afford significant advantages in software development over more traditional programming languages used in industrial settings
Keywords :
automatic telephone systems; electronic switching systems; formal specification; parallel languages; program verification; real-time systems; telecommunication computing; 5ESS; AT&T; ESTEREL; formal approach; formally-defined language; industrial settings; legacy reactive system; legacy reactive systems; programming; programming languages; reactive systems software; safety properties; software development; switch simulator; telecommunications application; telephone switching system; Application software; Computer languages; Programming; Safety; Switches; Switching systems; System software; Telecommunication switching; Telephony; Testing;
Conference_Titel :
Industrial-Strength Formal Specification Techniques, 1995. Proceedings., Workshop on
Conference_Location :
Boca Raton, FL
Print_ISBN :
0-8186-7005-3
DOI :
10.1109/WIFT.1995.515485
