Formal validation of virtual finite state machines

Author

Flora-Holmquist, Alan R. ; Staskauskas, Mark G.

Author_Institution

Dept. of Core Switching Dev., AT&T Bell Labs., Naperville, IL, USA

fYear

1995

fDate

5-8 Apr 1995

Firstpage

122

Lastpage

129

Abstract

We describe our experiences in introducing a formal validation tool in several projects that are developing software for AT&T´s 5ESS telephone switching system. The tool validates networks of communicating processes implemented in the virtual finite state machine (VFSM) notation, using Holzmann´s (1991) super-trace algorithm to check for errors in process interaction such as deadlock, livelock, unexpected inputs, message buffer overflow, and unreachable code. The validator has been used by several 5ESS developers to find bugs in their VFSM designs. We discuss the extent to which the validator has been successfully employed in 5ESS software development, and describe our present research efforts to eliminate some of the roadblocks that stand in the way of its more widespread use

Keywords

electronic switching systems; finite state machines; formal specification; program verification; software tools; telecommunication computing; 5ESS; AT&T; communicating processes; deadlock; formal validation; formal validation tool; livelock; message buffer overflow; process interaction; software development; super-trace algorithm; telephone switching system; unexpected inputs; unreachable code; virtual finite state machine; virtual finite state machines; Automata; Buffer overflow; Computer bugs; Explosions; Hardware; Message passing; Switches; Switching systems; System recovery; Telephony;

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.515484

Filename

515484