Requirement Capture, Formal Description and Verification of an Invoicing System

Projet VASY-RAThe 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. For this, the case study is informally described by half a page of English text. In this report, we use the formal description technique LOTOS for requirement 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 to 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, the new version of LOTOS currently being standardized. Since LOTOS allows a balance to be struck between process-oriented and data-oriented modeling, descriptions in both styles are given. After that, we verify the LOTOS descriptions by model-checking using the CADP (CÆSAR/ALDEBARAN) toolbox. The underlying Labelled Transition System (LTS) models corresponding to various scenarios are generated using the CÆSAR compiler. We push further the analysis of the case study by formalizing in temporal logic six properties of the system. We verify these properties on the LTS models using the XTL model-checker. Finally, we study the equivalence of the process-oriented and data-oriented descriptions using the ALDEBARAN tool