Information Technology Reference
In-Depth Information
-
the implementation of an alternative small-step Erlang semantics which is
able to detect more program errors, but which may yield substantially larger
state spaces,
-
initial support for using multiple processors (SMP) for model checking,
-
improved handling of Linear Temporal Logic claims through the integration
of a new translator from Linear Temporal Logic to Buchi automata (see
discussion below),
-
support for combining simulation and model checking algorithms to reduce
the state space needed to verify a program. This is used to reduce the cost
of using OTP behaviours such as e.g. the supervisor behaviour,
-
providing user documentation, including a tutorial, a user manual, and a
web page.
This has resulted in the production of the McErlang model checker which has
been released as open source under the agreed project license (a BSD variant);
more documentation and the option to download it is available at the tool web
site:
https://babel.ls.fi.upm.es/trac/McErlang/
.
A sign of the increasing maturity of the tool is that we were able to analyse a
RoboCup simulation league team programmed in Erlang (comprising some 8500
lines of Erlang code) using the McErlang tool, see [EFIL08]. A number of recent
improvements to the McErlang tool realised in the ProTest project are described
in [EF09].
LTL-to-Buchi Translation.
One of the additions made to McErlang during the
ProTest project was to add the possibility of expressing and checking correctness
properties expressed in Linear Temporal Logic (LTL). This is fairly straightfor-
ward, since LTL expressions can be automatically translated into Buchi automata.
However, for model checking to be ecient it is important to produce as small
an automaton as possible, thus a good translator was needed. The obvious solu-
tion was to use an existing implementation. However, this was not done for two
reasons: by developing an in-house translator we avoided licensing problems (our
in-house translator is licensed under the same BSD license as McErlang unlike,
e.g., the LTL2Buchi translator used in the JavaPathfinder project), and secondly
its proper integration into the McErlang verification framework enabled a better
end-user experience (e.g., with regards to formula parsing/deparsing, conversion
to an executable Erlang module, and so on).
The LTL-to-Buchi translator we have developed [Sve09] consists of the follow-
ing three parts: - A rewrite engine, which aims to simplify the LTL formula. It
uses a fixed set of (heuristically chosen) rewrite rules. - A core translation algo-
rithm Construction of the Buchi automaton from the re-written LTL formula.
We use a tableau-based algorithm. - A reduction step, where optimizations such
as simulation reductions and removal of non-reachable and non-accepting states,
are applied to the Buchi automaton.
The eciency of the LTL-to-Buchi translator was evaluated against two refer-
ence implementations; the LTL2Buchi translator in the JavaPathfinder and the
Wring tool. Our translator clearly outperforms Wring; moreover the evaluation
