Verification of the Chilean Electronic Invoices System.

Organisation:	OASIS project, INRIA Sophia-Antipolis (FRANCE)
Method:	ACTL mu-calculus Synchronized Networks of Labelled Transition Systems
Tools used:	FC2TOOLS CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2004
Size:	n/a
Description:	The Chilean law requires any commercial transaction done in Chile to be supported by a legal document previously authorised by the tax agency. For electronic exchange of documents between sales actors, the Chilean tax agency (SII) has recently provided an informal specification (using natural language) of an electronic invoice system. This case study concerns the complete process of formal specification and verification of the Chilean electronic invoice system. First, the invoice system is specified using a graphical language from which a formal specification in the form of parameterized hierarchical synchronization networks of processes can be derived automatically. Then, finite labeled transition systems were obtained by instantiation of the formal parameterized model, taking advantage of the hierarchical structure to avoid state explosion. Two techniques were used for the formal verification of properties. Reachability properties were expressed using the same graphical language as for the formalization, and checked using FC2TOOLS. Other properties were expressed using temporal logics, either mu-calculus or ACTL, and checked using the EVALUATOR tool of CADP. These verifications raised some issues that needed to be clarified in the initial informal specification. For instance, the verification of the informal property "SII gives the right answers to invoice status requests" showed undesired behaviors, which could be removed by adding a property, namely "it is not possible to cancel an invoice which has not been emitted before", that was missing in the original informal specification.
Conclusions:	This case study shows that the formal specification and verification of a large system is realistic. Furthermore, using verification tools already in early stages of the specification process allowed to find errors in the specification and omissions in the informal description.
Publications:	[Attali-Barros-Madelaine-04] Isabelle Attali, Tomas Barros, and Eric Madelaine. "Parameterized Specification and Verification of the Chilean Electronic Invoices System". In Proceedings of the 24th International Conference of the Chilean Computer Science Society SCCC'04 (Arica, Chile), November 2004. Available on-line at: http://www-sop.inria.fr/oasis/Vercors/papers/jccc04.pdf or from the CADP Web site in PDF or PostScript [Barros-Madelaine-04] Tomas Barros and Eric Madelaine. "Formalization and Proofs of the Chilean Electronic Invoices System." INRIA Research Report RR-55217, INRIA, June 2004. Available on-line at: http://www-sop.inria.fr/oasis/Vercors/papers/RR-5217.pdf or from the CADP Web site in PDF or PostScript
Contact:	Tomas Barros INRIA Sophia-Antipolis / OASIS project 2004 route des Lucioles - B.P. 93, 06902 Sophia Antipolis FRANCE Tel: +33 (0) 4 92 38 75 54 Fax: +33 (0) 4 92 38 76 44
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page