INRIA Rhone-Alpes (FRANCE)
Department of Computing Science and Mathematics, University of Stirling (SCOTLAND)
E-LOTOS and LOTOS
CADP (Construction and Analysis of Distributed Processes)
187 lines of E-LOTOS
407 lines of LOTOS
The Invoicing case study is a typical business system proposed by Henri Habrias as a common example for a contest on the capacity of particular formal methods to capture requirements from the client.
We use the formal description technique LOTOS for requirements capture, formal description and verification of the Invoicing case study. First, we analyse and interpret the informal requirements of the case study using the LOTOS approach for description of systems. This leads to a set of twenty questions about the informal description. By answering these questions, we obtain a high-level specification architecture that can be formalised. Then, we present the formal description of the case study in LOTOS and, for comparison, in E-LOTOS. Since LOTOS allows a balance to be struck between process-oriented and data-oriented modeling, descriptions in both styles are given.
We verify the LOTOS descriptions by model-checking using the CADP toolbox. The underlying Labelled Transition Systems (LTS) models corresponding to various scenarios are generated using the CAESAR compiler.
We formalize in temporal logic six properties of the system: absence of deadlocks and livelocks, and four logical ordering properties between visible actions. These properties have been extracted from the revised informal statements resulted from formalisation, expressed in XTL (using the ACTL operators), and then checked on the generated models.
We study the equivalence of the process-oriented and data-oriented descriptions using the ALDEBARAN tool. We show that the LTSs corresponding to the initial description cannot be equivalent modulo the equivalence relations offered by ALDEBARAN. However, by performing a slight modification of the data-oriented description, we obtain the safety equivalence of the two descriptions.
We successfully used LOTOS, E-LOTOS, and the CADP toolbox for the requirement analysis, formal description, and verification of the Invoicing case study.
This experience conduct us to ask twenty-three questions on the informal description of the Invoicing system. These questions arise either from the formal description of the system, or from the verification of the description.
As regards the specification formalisms, the authors are most satisfied with the E-LOTOS process-oriented description. It is clear that E-LOTOS offers a much cleaner and more compact style of specification compared to current LOTOS. In particular, modularity, typed gates, and functional data types are felt to be much preferable.
M. Allemand and C. Attiogbé and H. Habrias,
International Workshop on Comparing System Specification Techniques,
University of Nantes and IRIN (France),
[Sighireanu-98-a] Mihaela Sighireanu. Model-Checking Validation of the LOTOS Descriptions of the Invoicing Case Study, In Proceedings of the International Workshop on Comparing System Specification Techniques (Nantes, France), March 1998. Available on-line at: http://cadp.inria.fr/publications/Sighireanu-98-a.html
[Turner-98] Kenneth J. Turner. The Invoicing Case Study in (E-)LOTOS, In Proceedings of the International Workshop on Comparing System Specification Techniques (Nantes, France), March 1998
[Sighireanu-Turner-98] Mihaela Sighireanu and Kenneth J. Turner, Requirement Capture, Formal Description and Verification of a Business System: the Invoicing Case-Study, INRIA Research Report RR-3575, 1998. Available on-line at: http://cadp.inria.fr/publications/Sighireanu-Turner-98.html
655 avenue de l'Europe
F-38330 Montbonnot Saint-Martin
Tel: +33 4 76 61 52 89
Fax: +33 4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|