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.
Type de document :
Communication dans un congrès
Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.17-32, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_2〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01398006
Contributeur : Hal Ifip <>
Soumis le : mercredi 16 novembre 2016 - 15:33:54
Dernière modification le : dimanche 29 octobre 2017 - 20:26:01
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:21:52

Fichier

978-3-662-43613-4_2_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Daniela Remenska, Tim Willemse, Jeff Templon, Kees Verstoep, Henri Bal. Property Specification Made Easy: Harnessing the Power of Model Checking in UML Designs. Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.17-32, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_2〉. 〈hal-01398006〉

Partager

Métriques

Consultations de la notice

37

Téléchargements de fichiers

32