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

Formalisation and verification of the Chilean electronic invoice system

Tomás Barros 1 Eric Madelaine
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 a case study describing the formal specification and verification of the Chilean electronic invoice system, which has been defined by the Chilean taxes administration. The system is described by graphical specifications consisting of labelled transition systems, composed using synchronisation networks. Both, transition systems and networks, are parameterized. We use verification tools based on Process Algebra theories to check the requirements on those graphical specifications. We introduce a method and a tool to obtain finite systems from these parameterized ones by fixing the parameters domains, so we can use standard tools for verifying properties in finite systems. We also analyse different methods to avoid the state explosion problem by taking advantage of the parameterized structure and instantiations.
Document type :
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 9:36:13 PM
Last modification on : Friday, February 4, 2022 - 3:19:01 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:53:43 PM


  • HAL Id : inria-00070777, version 1



Tomás Barros, Eric Madelaine. Formalisation and verification of the Chilean electronic invoice system. RR-5217, INRIA. 2004, pp.55. ⟨inria-00070777⟩



Record views


Files downloads