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.
Type de document :
Communication dans un congrès
in proc. of the XXIV International Conference of the Chilean Computer Science Society (SCCC'04), Oct 2004, Arica, Chili, IEEE, 2004
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00087210
Contributeur : Eric Madelaine <>
Soumis le : vendredi 21 juillet 2006 - 15:25:11
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:21:15

Fichiers

Madelaine_E.pdf

Identifiants

  • HAL Id : inria-00087210, version 1

Collections

INRIA | UNICE | I3S | UNIV-COTEDAZUR

Citation

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), Oct 2004, Arica, Chili, IEEE, 2004. 〈inria-00087210〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

312

Téléchargements de fichiers

168

Contact


archive-ouverte@inria.fr