A framework for evaluating specification methods for reactive systems-experience report

Author

Ardis, Mark A. ; Chaves, John A. ; Jagadeesan, Lalita Jategaonkar ; Mataga, Peter ; Puchol, Carlos ; Staskauskas, Mark G. ; Von Olnhausen, James

Author_Institution

Bell Labs., Naperville, IL, USA

Volume

22

Issue

6

fYear

1996

fDate

6/1/1996 12:00:00 AM

Firstpage

378

Lastpage

389

Abstract

Numerous formal specification methods for reactive systems have been proposed in the literature. Because the significant differences between the methods are hard to determine, choosing the best method for a particular application can be difficult. We have applied several different methods, including Modechart, VFSM, ESTEREL, Basic LOTOS, Z, SDL, and C, to an application problem encountered in the design of software for AT&T´s 5ESS telephone switching system. We have developed a set of criteria for evaluating and comparing the different specification methods. We argue that the evaluation of a method must take into account not only academic concerns, but also the maturity of the method, its compatibility with the existing software development process and system execution environment, and its suitability for the chosen application domain

Keywords

formal specification; specification languages; telecommunication computing; telecommunication switching; Basic LOTOS; C; ESTEREL; Modechart; SDL; VFSM; Z; formal specification methods; industrial applications; reactive systems; software development process; specification languages; specification methods; system execution environment; technology assessment; telephone switching system; Application software; Design methodology; Formal specifications; Programming; Protocols; Software design; Specification languages; Switching systems; System testing; Telephony;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.508312

Filename

508312