ELOTON Eclipse-based Editor to Support LOTOS Newcomers

Organisation:	University of Sannio (ITALY)
Functionality:	Language editor and graph viewer.
Tools used:	ELOTON CADP (Construction and Analysis of Distributed Processes)
Period:	2014
Description:	Writing and verifying a formal model of a system is not an easy task, particularly for newcomers in formal methods. There is a need for tools to assist users in these tasks. ELOTON (Eclipse-based editor for LOTOS Newcomers) is an Eclipse based tool designed for this purpose. It provides a graphical front-end to some elements of the CADP verification environment, among which its input language LOTOS. More precisely, ELOTON consists of three main components: (1) A LOTOS editor based on the Xtext component of Eclipse enables syntax highlighting, code templates, and code auto-completion. (2) A wrapper component allows the user to call the CADP compilers for LOTOS and to manage the resulting compiling errors. These errors are sorted in a specific view, and automatically linked to their code location, to facilitate source-code navigation and debugging. (3) A graph visualizer based on the Zest visualization toolkit of Eclipse allows the user to view, zoom and arrange the BCG graphs generated by CADP, according to his needs. A salient feature is the ability to expand the graph on-demand, node after node, so as to navigate within large graphs.
Conclusions:	ELOTON constitutes a front-end to CADP, which aims at facilitating access to the verification of LOTOS specifications. Being based on the popular Eclipse platform, it is aimed at contributing to the dissemination of formal methods, and in particular model checking. The tool is still to be complemented with editors for other languages of CADP, in particular the temporal logic description languages used to describe the system properties to be checked.
Publications:	[DeRuvo-Santone-14] Giuseppe de Ruvo and Antonella Santone. "An Eclipse-Based Editor to Support LOTOS Newcomers". Proceedings of the 23rd International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises WETICE'2014, pages 372-377. IEEE Computer Society Press, 2014. Available on-line at: http://www.deruvo.eu/preprints/VSC2014.pdf or from the CADP Web site in PDF or PostScript
Contact:	Prof. Antonella Santone Department of Engineering University of Sannio RCOST - Ex Post Office Building Via Traiano 1 I-82100 Benevento ITALY Tel: +39 (0)824 30 5552 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