%0 Conference Proceedings
%T Property Specification Made Easy: Harnessing the Power of Model Checking in UML Designs
%+ Vrije Universiteit Amsterdam [Amsterdam] (VU)
%+ National Institute for Subatomic Physics [Amsterdam] (NIKHEF)
%+ Eindhoven University of Technology [Eindhoven] (TU/e)
%A Remenska, Daniela
%A Willemse, Tim, C.
%A Templon, Jeff
%A Verstoep, Kees
%A Bal, Henri
%Z Part 1: Specification Languages and Type Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 34th Formal Techniques for Networked and Distributed Systems (FORTE)
%C Berlin, Germany
%Y Erika Ábrahám
%Y Catuscia Palamidessi
%I Springer
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-8461
%P 17-32
%8 2014-06-03
%D 2014
%R 10.1007/978-3-662-43613-4_2
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01398006/document
%2 https://inria.hal.science/hal-01398006/file/978-3-662-43613-4_2_Chapter.pdf
%L hal-01398006
%U https://inria.hal.science/hal-01398006
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-8461