Contracts for Multi-instance UML Activities

Abstract : We present a novel way of encapsulating UML activities using interface contracts, which allows to verify functional properties that depend on the synchronization of parallel instances of software components. Encapsulated UML activities can be reused together with their verification results in SPACE, a model-driven engineering method for reactive systems. Such compositional verification significantly improves the scalability of the method. Employing a small example of a load balancing system, we explain the semantics of the contracts using the temporal logic TLA. Thereafter, we propose a more easily comprehensible graphical notation and clarify that the contracts are able to express the variants of multiplicity that we can encounter using UML activities. Finally, we give the results of verifying some properties of the example system using the TLC model checker.
Type de document :
Communication dans un congrès
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.304-318, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_20〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01583314
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 septembre 2017 - 11:10:12
Dernière modification le : lundi 11 septembre 2017 - 10:47:03

Fichier

978-3-642-21461-5_20_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Vidar Slåtten, Peter Herrmann. Contracts for Multi-instance UML Activities. Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.304-318, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_20〉. 〈hal-01583314〉

Partager

Métriques

Consultations de la notice

45

Téléchargements de fichiers

7