Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070777
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:36:13 PM
Last modification on : Friday, January 8, 2021 - 11:14:19 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:53:43 PM

Identifiers

  • HAL Id : inria-00070777, version 1

Collections

Citation

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

Share

Metrics

Record views

283

Files downloads

418