The Circus model checker is a tool implemented over Microsoft FORMULA that is able to analyse properties of Circus specifications. It has been implemented following the Structured Operational Semantics of Circus, where formal rules are the mais elements used to derive FORMULA instructions to generate the model (a Labelled Transtion System) and the properties (deadlock, livelock and nondeterminism) are translated as queries over models.
Software Installation
The Circus model checker runs only in Windows platform and requires auxiliary software. The following steps show how to install the required software:
Install Visual Studio 2010. The current version of FORMULA requires this specific version of Visual Studio. Please do not install any other version.
Install FORMULA. It is available at http://research.microsoft.com/en-us/um/redmond/projects/formula/. It automatically installs Z3. As our embedding considered version 1.3.15450.0, we strongly recommend it for questions of compatibility.
Screenshots
There are two modes of running FORMULA: command line and inside Visual Studio. Both modes have similar features but in Visual Studio the user interaction is much more friendly.
On the other hand, the command line mode is a fewer fast but requires the use of excplicit commands and it does not allow to observe calls to Z3.
The screeshots presented here provide a way to make the use of the Circus model checker clear. Each step is intuitive and easy to be executed.
Open Visual Studio. This action opens the Visual Studio main window.
Create a new FORMULA project. This can be doen by using the menu bar and then by choosing a Formula project. Enter the name of the project and confirm. This will create an empty project. Maybe the panel Formula Explorer is not active, but you can make it visible by using the menu View of Visual Studio.
Replace the content of an empty project with that of the one example provided here.
Compile the project by using the menu Build -> Rebuild solution. This compiles the project and fills the Formula Explorer with all sections in the script.
The elements to be checked in Visual studio are partial models. Use the right click on the partial model and select Get Model. This makes FORMULA to generate the LTS (base of facts according to the semantics) and generate one item representing the model validating the property, or "unsatisfiable" if the model does not satisfy the property.
Check the model. Once there the property is satisfied we already know that there is a solution. But it is not still complete untill it has been checked. This can be done by using right click in the generated solution and by choosing the Check option.
Examples
Some examples are provided:
A process without state and that simply performs the Stop action. FORMULA detects a deadlock.
A process without state and that simply performs the Skip action. FORMULA does not detect deadlocks.
A process without state and that behaves as "a.1 -> Stop". FORMULA does not detect deadlocks
A complex process describing the Emergency Response System (ERS) proposed in [1,2]. The process ERSystem_0 has deadlock, while ERSystem_2 has not. This is an improvement made towards fault tolerance.
Complete demonstration
This video shows how to use the Circus Model Checker using some of the above examples. We recommend that you try all the examples.
References
[1] Andrews, Z., Didier, A., Payne, R., Ingram, C., Holt, J., Perry, S., Oliveira, M., Woodcock, J., Mota, A., and Romanovsky, A. (2013a). Report on timed fault tree analysis—fault modelling. Technical Report D24.2, COMPASS.
[2] Andrews, Z., Payne, R., Romanovsky, A., Didier, A., and Mota, A. (2013b). Model-based development of fault tolerant systems of systems. In Systems Conference (SysCon), 2013 IEEE International, pages 356–363.