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
Conference papers

Formalisation and Proofs of the Chilean Electronic Invoices System

Isabelle Attali 1 Tomás Barros 1 Eric Madelaine 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We present the complete process of a formal specification and verification of the Chilean electronic invoice system which has been defined by the tax agency. We use this case study as a real-world and real-size example to illustrate our methodology for specification and verification of distributed applications. Our approach is based on a new hierarchical and parameterized model for synchronised networks of labelled transition systems. In this case study, we use a subset of the model as a graphical specification language. We check this formal specification of the invoice system against its informal requirements, described in terms of parameterized temporal logic formulas. Their satisfiability cannot be checked directly on the parameterized model\,: we introduce a method and a tool to instantiate the parameterized models and properties, allowing to use standard (finite-state, bisimulation-based) model-checkers for the verification. We also illustrate the use of different methods to avoid the state explosion problem by taking advantage of the parameterized structure and instantiations.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

Contributor : Eric Madelaine Connect in order to contact the contributor
Submitted on : Friday, July 21, 2006 - 3:25:11 PM
Last modification on : Friday, February 4, 2022 - 3:19:09 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 12:21:15 AM


  • HAL Id : inria-00087210, version 1



Isabelle Attali, Tomás Barros, Eric Madelaine. Formalisation and Proofs of the Chilean Electronic Invoices System. in proc. of the XXIV International Conference of the Chilean Computer Science Society (SCCC'04), INRIA, Oct 2004, Arica, Chili. ⟨inria-00087210⟩



Record views


Files downloads