Formal verifications: an industrial case study

Author

Vergauwen, B. ; Lewi, J.

Author_Institution

Dept. of Comput. Sci., Katholieke Univ., Leuven, Belgium

fYear

1992

fDate

4-8 May 1992

Firstpage

208

Lastpage

213

Abstract

By means of the mu PABX example, the adequacy of temporal logic was demonstrated for the specification and formal verification of industrial reactive systems. The aim of the mu PABX system is to provide services that are issued by phone-users of the mu PABX. In contrast to a real PABX, the mu PABX offers only one type of service to its subscribers: two-party voice calls. Formal verification avoids the deficiencies of testing by proving mathematically that the system behaves according to the specification. For this to be possible, the system behavior must be defined with mathematical precision. The focus is on the formal verification of the mu PABX. It is demonstrated that, if temporal logic is used, the task of proof construction can be 100% automated. An implementation of the mu PABX system is discussed.<>

Keywords

formal verification; private telephone exchanges; telecommunications computing; temporal logic; formal verification; industrial case study; industrial reactive systems; mathematical precision; mu PABX example; phone-users; proof construction; system behavior; temporal logic; two-party voice calls; Computer aided software engineering; Computer industry; Computer science; Context; Formal verification; Maintenance; Operating systems; Process control; System testing; Telephony;

fLanguage

English

Publisher

ieee

Conference_Titel

CompEuro '92 . 'Computer Systems and Software Engineering',Proceedings.

Conference_Location

The Hague, Netherlands

Print_ISBN

0-8186-2760-3

Type

conf

DOI

10.1109/CMPEUR.1992.218507

Filename

218507