PASS
Property ASSistant
Developing correct concurrent software is challenging. Design errors can result in deadlocks, race conditions and livelocks, and discovering these is difficult. Approaches for automatically generating formal models from system designs have been proposed and successfully used in industry. A serious obstacle for an industrial uptake of rigorous analysis techniques such as model checking is the steep learning curve associated to the languages—typically temporal logics— used for specifying the application-specific properties to be checked. To bring the process of correctly eliciting functional properties closer to software engineers, we introduce PASS, a Property ASSistant wizard as part of a UML-based front-end to the mCRL2 toolset. PASS instantiates pattern templates using three notations: a natural language summary, a μ-calculus formula and a UML sequence diagram depicting the desired behavior. Most approaches to date have focused on LTL, which is a state-based formalism. Conversely, μ-calculus is event-based, making it a good match for sequence diagrams, where communication between components is depicted. Last but not least, we automatically generate monitors based on a μ-calculus formula, which can be used for property-driven on-the-fly model checking using the standard state-space exploration facilities of mCRL2.
PASS is developed as an Eclipse plug-in (only around 5k loc), so you can easily install it by adding the .jar file to your ECLIPSE_HOME/plugins directory.
Launching PASS is easy:
But before you do that, perhaps add the ProfilePropSpec.epx profile to your model:
Select the model, go to the Properties tab, and click on "Add Profile":
Just select the profile from a file (ProfilePropSpec.epx is in this repository), click OK, and you're done!
Screenshots
Click to view.
See also the mCRL2 site and the LTSmin toolset one. Our Property Pattern templates and extensions for μ-calculus are publicly available for the curious users.
Q: I don't care about UML. I already have the mCRL2 model and just want to get a formula and a monitor for my property.
A: OK, we have a solution: use PASS Web Start. It's work in progress. For now it should work with Linux and Windows, all you need is J2SE1.5+. Please report any problems or feedback.