University of Tehran and IPM (IRAN)
Eindhoven University of Technology TU/e (THE NETHERLANDS)
Reykjavík University (ICELAND)
CADP (Construction and Analysis of Distributed Processes)
This paper addresses the verification of actor-based programs
written in the reactive object language Rebeca, which has a
formal foundation and is designed in an effort to bridge the
gap between formal verification approaches and real
applications. A Rebeca model contains concurrent objects
(called rebecs) that modify their local state and send
asynchronous messages in reaction to received messages. Rebecs
dequeue received messages from infinite queues and execute the
corresponding methods atomically (i.e., without interleaving
statements of concurrent methods). When several rebecs can
dequeue a message, a nondeterministic scheduler chooses the
message to dequeue.
The verification approach consists in translating Rebeca models into the mCRL2 process algebra. Atomicity of message execution allows to replace concurrent behavior by nondeterministic sequential interleaving; moreover, at any time, only one instance from the rebecs and the scheduler processes needs to be present (in addition to a process for the state variables of the rebecs and one for their queues). This translation is automated by a tool, called Sarir.
Then, the state space is generated as a labeled transition system (LTS), where transitions correspond to message sending and to assignment to local state of rebecs.
In a third step, various reductions and minimizations can be applied to the LTS and properties are checked against the LTS using the EVALUATOR tool of CADP.
The approach is illustrated on four examples among which the tree identify phase of the IEEE 1394 firewire bus. When a component is removed or attached to a firewire bus, the resulting topology is checked to be a tree or not. To determine the root of the tree, nodes exchange parent request messages. The property checked with the EVALUATOR tool verifies that the root is always correctly determined.
This work illustrates the usefulness of the model checking
approach with CADP of actor-based programs. Despite conceptual
differences between source and target models, the tool chain
proved to be effective for the purpose of verification:
H. Hojjat, M. Sirjani, M. R. Mousavi and J. F. Groote.
"Sarir: A Rebeca to mCRL2 Translator".
In Proceedings of the 7th International Conference on Application
of Concurrency to System Design ACSD'07 (Bratislava, Slovak
IEEE Computer Society,
Available on-line from http://www.win.tue.nl/~mousavi/acsd07.htm
or from the CADP Web site in PDF or PostScript
School of Electrical and Computer Engineering
University of Tehran
Karegar Avenue, Pardiss 2
Tel: + 98 21 6111 4912
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies