Title :
An Eclipse-Based Editor to Support LOTOS Newcomers
Author :
De Ruvo, Giuseppe ; Santone, Antonella
Author_Institution :
Dept. of Eng., Univ. of Sannio, Benevento, Italy
Abstract :
We present ELOTON, an Eclipse-based Editor to help people who want to approach the Language of Temporal Ordering Specification (LOTOS). LOTOS is a Formal Description Technique standardized by ISO for the design of concurrent and distributed systems, and in particular for OSI services and protocols. LOTOS has been widely used for the specification of large data communication systems. It is mathematically well-defined and expressive: it allows concurrency, non-determinism, synchronous and asynchronous communications. CADP is a popular toolbox that supports high-level descriptions written in LOTOS, among others. Unluckily, there not exists an user interface suitable for newcomers in formal methods. Thus, many people encounter many obstacles in using formal methods and in particular model checking due to the lacking of user-friendly tools. We argue that ELOTON, thanks to its rich text editor and visualization features might involve a major number of users coming from various disciplines. Our tool serves as a graphical front-end for CADP.
Keywords :
data visualisation; formal specification; object-oriented methods; CADP toolbox; ELOTON Eclipse-based editor; LOTOS newcomers support; OSI protocols; OSI services; data communication systems; formal description technique; formal methods; language of temporal ordering specification; rich text editor; visualization features; Algebra; Automata; Mathematical model; Model checking; Software; Syntactics; Visualization; CADP; Eclipse RCP; Formal Verification Tools; LOTOS; Model Checking;
Conference_Titel :
WETICE Conference (WETICE), 2014 IEEE 23rd International
Conference_Location :
Parma
DOI :
10.1109/WETICE.2014.39