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.

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.