Contracts for Multi-instance UML Activities

International audience 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 verific...

Full description

Bibliographic Details
Main Authors: Slåtten, Vidar, Herrmann, Peter
Other Authors: Norwegian University of Science and Technology Trondheim (NTNU), Norwegian University of Science and Technology (NTNU), Roberto Bruni, Juergen Dingel, TC 6, WG 6.1
Format: Conference Object
Language:English
Published: HAL CCSD 2011
Subjects:
[INFO]Computer Science [cs]
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI]
Iceland
Online Access:https://hal.inria.fr/hal-01583314
https://hal.inria.fr/hal-01583314/document
https://hal.inria.fr/hal-01583314/file/978-3-642-21461-5_20_Chapter.pdf
https://doi.org/10.1007/978-3-642-21461-5_20
Description
Summary:International audience 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.

Similar Items