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

fYear

1995

fDate

5-8 Apr 1995

Firstpage

132

Lastpage

145

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Industrial-Strength Formal Specification Techniques, 1995. Proceedings., Workshop on

Conference_Location

Boca Raton, FL

Print_ISBN

0-8186-7005-3

Type

conf

DOI

10.1109/WIFT.1995.515485

Filename

515485