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 metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01398006
Contributor : Hal Ifip <>
Submitted on : Wednesday, November 16, 2016 - 3:33:54 PM
Last modification on : Sunday, October 29, 2017 - 8:26:01 PM
Long-term archiving on : Thursday, March 16, 2017 - 5:21:52 PM

File

978-3-662-43613-4_2_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Daniela Remenska, Tim 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⟩

Share

Metrics

Record views

58

Files downloads

125