BMC4UML

is a (prototype) module of the verification system VerICS, aimed at verification of concurrent systems specified in a subset of UML 2.1, using the bounded model checking method. It is still in a preliminary stage and needs some improvements. However, some encouraging experimental results have been obtained (see publications list).

Download & Run

To proceed with BMC4UML one should download the current version of VerICS.
Choose the "full version" if you are using linux, or the "client version" otherwise.

If you choose the full version make sure that all files in the folder WEB-INF/apps are executable. You need also to add one of SAT-solvers: zChaff or MiniSAT (minisat_static) to your PATH variable.

 Run VerICS via "run.sh" or "run.bat" and launch UML2SAT plugin from Modules menu.

 Using the "Load" button load one of examples provided. Each of the examples consists of 2 files. *T.xml contains a description of a property to be tested and a file name with UML specification. You can see it as a tree or as text. In the next release we plan to introduce an advanced property editor here. At the moment you should prepare T.xml files using an external editor, if you want to test other properties.
The second file contains UML 2.1system in XMI 2.1 format exported from Enterprise Architect tool. You can visualize the state machines by using a corresponding button. Click "Next" to proceed to the next step of verification.

The options available here are:
initial state - checked (or unchecked) automatically, according to the input (property) file *T.xml: if there is no "<state depth="0">" tag, the first state of the symbolic path will be encoded as the default initial state (i.e. for all the state machines the initial state of the Top region will be encoded as active and completed). Otherwise the first symbolic state will be encoded in accordance with *T.xml file.
queue size - the maximal number of events allowed in event queues.
integer size - the number of bits used to encode the integer variables (e.g. 6 bits allow to encode values between -32 and 31).
depth of the path - the depth of unwinding of the transition relation. Typically one starts with the depth 1 and checks the option "search until SAT".
search until SAT - if checked, then the depth of the path is automatically increased, and the search is repeated until a counterexample is found.
simulate witness - if checked, then a witness (counterexample) file is generated (if one is found) and in the next step its simulation is enabled.
SAT-solver - one can choose between MiniSAT and zChaff solver. At the moment MiniSAT gives better results..

After setting the options proceed with "Run verification" button.

During the verification process you can see some statistics, e.g. time and memory consumed by BMC and SAT-solver. You can also cancel the verification using the corresponding button.

Finally, if a counterexample has been found, you can visualize it, optionally after setting some options:
global view - presents global states of the system,
local view - shows the state machines of all the objects,
active view - a view presenting a state machine of the object that fires a transition during the current step.
Using "Filter" buttons you can display only the objects interesting for you (usefull in the case of big number of objects).
Next proceed with "Simulate witness" button.

At the witness visualization stage you can navigate the path using "Prev" and "Next" buttons, or by clicking at the global view. In the left part of the window you can see variables and clocks valuations, and the contents of the event queues.

Known problems and final remarks

The parametric verification mode is available at the moment only from the command line. Please type bmc4uml -h for more information.
BMC4UML is also highly sensitive to incorrect property files (*T.xml). In the case of errors, the advise is to check them first (e.g. if a state that is not "completion sensitive" has an attribute "compl" the program crashes after producing a nasty error description). The property files editor will be included in the next release.

Finally I want to thank to a lot of people which helped me with BMC4UML, and especially:
Wojciech Penczek - my supervisor - for motivation and support,
Maciej Szreter for great introduction in the world of satisfiability,
Andrzej Zbrzezny for access to his C++ library that allows easy encoding of propositional formulae,
Agata Półrola for additional help and support,
and Łukasz Gadomski for developing the witness visualization.