Application name:

Automatic Protection Switching (Comparative Study of Formalisms)

Organisation:

Lucent Technologies, Bell Laboratories

Method:

Esterel, LOTOS, Modechart, SDL, VFSM, Z

Tools:

Agel tool-set for Esterel (from ILOG); PLOTOS tools developed at AT&T; MT tool-set for Modechart (from the University of Texas at Austin); SDL tools developed at AT&T; VFSM tools developed at AT&T; Fuzz for Z (from Mike Spivey).

Domain:

Telecommunications

Period:

1994

Size:

Small transition system (26 states, 138 transitions).

Description:

Several descriptions of the same telecommunications standard were composed in different formalisms (Esterel, LOTOS, Modechart, SDL, VFSM, and Z). The formalisms were then evaluated according to a set of software engineering criteria. All the specifications were constructed by researchers.

Conclusions:

Different formalisms and their associated technologies have different strengths and weaknesses. We were surprised that so many differences could be observed on only a small problem.

Publications:

"A Framework for Evaluating Specification Methods for Reactive Systems". M. Ardis, J. Chaves, L. Jagadeesan, P. Mataga, C. Puchol, M. Staskauskas, J. Von Olnhausen. IEEE Transactions on Software Engineering, 22(6):378-389, June 1996.

Contact:

Name:	Mark A. Ardis
Organisation:	Lucent Technologies, Bell Laboratories
Address:	1000 East Warrenville Road P.O. Box 3013 Naperville, IL 60566-7013
Country:	USA
Phone number:	+1 (630) 9790042
Fax:	+1 (630) 7134982
E-mail:	maa@research.bell-labs.com
Personal website:	http://www.bell-labs.com/~maa

© copyright 2004 | Formal Methods Europe