Open AccessLanguage-Oriented Formal Analysis: a Case Study on Protocols and Distributed Systems
Author(s) -
Carlos Bazílio,
Edward Hermann Hæusler,
Markus Endler
Publication year - 2007
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2007.03.022
Subject(s) - computer science , programming language , language of temporal ordering specification , model checking , specification language , formal specification , formal methods , programming language specification , architecture , protocol (science) , formal verification , process (computing) , medicine , art , inductive programming , programming domain , alternative medicine , pathology , programming paradigm , visual arts
The main motivation of this paper is to describe an architecture that intends to ease the verification of distributed algorithms and protocols (possibly mobile) through model checking. The core of the architecture is the protocol specification language (LEP), which has constructions, called pronouns, that allows for high-level specification. This means a much less verbose specification, when compared with the general-purpose specification language of the model checker used in our experiments. Through a two-step process, LEP specifications are translated into the language of a model checker and the result is translated back to LEP. A formal communication model is used in the translation process in order to allow the use of different model checkers. Currently the prototype of the architecture uses the model checkers Spin and SMV
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom