Property specification made easy: Harnessing the power of model checking in UML designs

Abstract

Developing correct concurrent software is challenging. Design errors can result in deadlocks, race conditions and livelocks, and discovering these is difficult. A serious obstacle for an industrial uptake of rigorous analysis techniques such as model checking is the 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. We revisit a case study from the Grid domain, using PASS to obtain the formula and monitor for checking the property. © 2014 IFIP International Federation for Information Processing.