Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, November 16, 2016 - 3:33:54 PM
Last modification on : Friday, January 7, 2022 - 12:00:02 PM
Long-term archiving on: : Thursday, March 16, 2017 - 5:21:52 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Daniela Remenska, Tim C. Willemse, Jeff Templon, Kees Verstoep, Henri Bal. Property Specification Made Easy: Harnessing the Power of Model Checking in UML Designs. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. pp.17-32, ⟨10.1007/978-3-662-43613-4_2⟩. ⟨hal-01398006⟩



Record views


Files downloads