Language-Oriented Formal Analysis: a Case Study on Protocols and Distributed Systems

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.