Model-Checking Validation of the LOTOS Descriptions of the Invoicing Case Study

Mihaela Sighireanu

Proceedings of the 1st International Workshop on on Comparing System Specification Techniques (Nantes, France), March 1998.

Abstract:

This paper deals with the verification by model-checking of the LOTOS descriptions given by Ken Turner for the invoicing case study. Both data-oriented and process-oriented descriptions are considered. The underlying LTS models corresponding to various scenarios are generated using the CAESAR compiler. The verifications are performed using the CADP (CAESAR/ALDEBARAN) toolbox. We push further the analysis of the case study by giving a formal specification in the ACTL temporal logic of some of the informal statements presenting the case study and by specifying four new properties. Thus, we verify these properties using the XTL model-checker. Then, we formally verify that the two descriptions are safety equivalent using the ALDEBARAN tool. This experience shows the interest of the automatic verification methods in the analysis of informal specifications. Thus, a specification technique shall not only be able to model a large spectrum of systems, but it also have to support the automatic analysis of these descriptions.

16 pages. There exists a refined version of this work, available from here.