Static POR of Message-Passing Protocols.
MP-Basset is a model checker for message-passing systems. It extends the Basset model checker with quorum transitions, i.e., atomic events consuming multiple messages. MP-Basset supports Partial-Order Reduction (POR) for better scalability of model checking complex message-passing protocols.
News
Release of MP-Basset extension with new optimization called Decompasition-Based Stateful Search (DBBS). The optimization consists of the following features:
- Selective push-on-stack for time-efficient backtracking.
- Selective hashing for more efficient state matching.
- New JPF core version (6.0).
The source code of DBSS/MP-Basset is available for download.
Documentations
MP-Basset supports dynamic Partial-Order Reductions (POR) via Basset, and implements a new static POR algorithm called Local POR (LPOR) [2]. Die new version of MP-Basset also supports MP-State, which is an improvement of explicit-state software model checking of message passing programs.
A short user guide of MP-Basset can be found in [1].
[1]
Péter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri, “Efficient Model Checking of Fault-Tolerant Distributed Protocols”, Proc. of the IEEE Int’l Conf. on Dependable Systems and Networks (DSN-DCCS), 2011
[2]
Péter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri, “Supporting Domain-Specific State Space Reductions through Local Partial-Order Reduction”, Proc. of the 26th IEEE/ACM Int’l Conf. on Automated Software Engineering (ASE), pp. 113-122, 20111.
Download & Installation
The complete source code of MP-Basset is available here. The new version of MP-Basset is integrated with the latest JPF core and includes our new technique MP-State.
MP-Basset includes Java Pathfinder (the model checker engine utilized by Basset, and, in turn, MP-Basset) and a Java-based open library implementation of LPOR.
MP-Basset can be installed similar to Basset.
MP-Basset runs from the command line. You can run your first MP-Basset application using the following simple script (MPBasset).
For example, the following command starts MP-Basset with LPOR for the model of the Paxos consensus protocol with 3 acceptor processes.
./MPbasset +fw.mp=1 +fw.spor=1 paxos.actor.DriverMP 3
Examples
Example message-passing protocols written in MP, the input language of MP-Basset, can be found in the MP-Basset distribution (/jpf-actor/src/examples/).
The following examples are available:
- Paxos consensus: /jpf-actor/src/examples/paxos/
- Echo multicast: /jpf-actor/src/examples/multicast/
- Regular register: /jpf-actor/src/examples/register/
- Zab atomic broadcast: /jpf-actor/src/examples/zab/