EB32LNT Translator from the EB3 Language to LNT

Organisation:	LACL, Université Paris-Est, Paris (FRANCE) Inria Grenoble Rhône-Alpes and LIG, Grenoble (FRANCE)
Functionality:	Translator from the EB3 language to LNT
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2013
Description:	EB3 is a specification language for information systems. The core of the EB3 language consists of process algebraic specifications describing the behaviour of the entities in a system, and attribute function definitions describing the entity attributes. The verification of EB3 specifications against temporal properties is of great interest to users of EB3. A translation from EB3 to LNT is proposed, which ensures a one-to-one correspondence between states and transitions of the labelled transition systems corresponding to EB3 and the LNT specification. This translation is automated with the EB32LNT tool, which makes it possible to verify EB3 specifications with the use of the CADP toolbox.
Conclusions:	The EB32LNT translator provides a direct connection to all the state-of-the-art verification features of the CADP toolbox. The translator was validated on several examples of typical information systems, and MCL temporal properties were successfully model checked using CADP on these examples. The translator also opens the way to equivalence checking and compositional LTS construction applied to EB3 specifications.
Publications:	[Vekris-Dima-13] Dimitrios Vekris and Catalin Dima. "Efficient Operational Semantics for EB3 for Verification of Temporal Properties". Proceedings of the 5th International Conference on Fundamentals of Software Engineering (Tehran, Iran), volume 8161 of Lecture Notes in Computer Science, pages 133-149, Springer-Verlag, April 2013. Available on-line from: http://doi.org/10.1007/978-3-642-40213-5_9 or from the CADP Web site in PDF and PostScript [Vekris-Lang-Dima-Mateescu-13] Dimitrios Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu. "Translating EB3 to LNT for Verification with CADP". Proceedings of the 10th International Conference on integrated Formal Methods iFM'2013 (Turku, Finland), volume 7940 of Lecture Notes in Computer Science, pages 61-76, Springer-Verlag, June 2013. Available on-line from: http://cadp.inria.fr/publications/Vekris-Lang-Dima-Mateescu-13.html or from: http://hal.inria.fr/hal-00768310/en [Vekris-14] Dimitrios Vekris. "Vérification de spécifications EB3 à l'aide de model checking". PhD thesis, Université Paris-Est, December 2014. Available on-line from: http://www.theses.fr/2014PEST1117.pdf or from the CADP Web site in PDF or PostScript [Vekris-Lang-Dima-Mateescu-16] Dimitris Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu. "Verification of EB3 Specifications using CADP". Formal Aspects of Computing, 28(1):145-178, 2016. Available on-line from: http://cadp.inria.fr/publications/Vekris-Lang-Dima-Mateescu-16.html or from: http://hal.inria.fr/hal-01290460/en
Contact:	Dimitrios Vekris LACL, Université Paris-Est 61, avenue du Général de Gaulle 94010 Créteil FRANCE Email: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page