Title :
Formal verifications: an industrial case study
Author :
Vergauwen, B. ; Lewi, J.
Author_Institution :
Dept. of Comput. Sci., Katholieke Univ., Leuven, Belgium
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;
Conference_Titel :
CompEuro '92 . 'Computer Systems and Software Engineering',Proceedings.
Conference_Location :
The Hague, Netherlands
Print_ISBN :
0-8186-2760-3
DOI :
10.1109/CMPEUR.1992.218507
