HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Requirement Capture, Formal Description and Verification of an Invoicing System

Mihaela Sighireanu 1 Kenneth J. Turner
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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. 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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 11:52:31 AM
Last modification on : Friday, February 4, 2022 - 3:23:31 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:34:27 PM


  • HAL Id : inria-00073106, version 1



Mihaela Sighireanu, Kenneth J. Turner. Requirement Capture, Formal Description and Verification of an Invoicing System. RR-3575, INRIA. 1998. ⟨inria-00073106⟩



Record views


Files downloads