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...
Main Authors: | , |
---|---|
Other Authors: | , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2011
|
Subjects: | |
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 |
id |
ftccsdartic:oai:HAL:hal-01583314v1 |
---|---|
record_format |
openpolar |
spelling |
ftccsdartic:oai:HAL:hal-01583314v1 2023-05-15T16:49:27+02:00 Contracts for Multi-instance UML Activities Slåtten, Vidar Herrmann, Peter Norwegian University of Science and Technology Trondheim (NTNU) Norwegian University of Science and Technology (NTNU) Roberto Bruni Juergen Dingel TC 6 WG 6.1 Reykjavik,, Iceland 2011-06-06 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 en eng HAL CCSD Springer info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_20 hal-01583314 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 doi:10.1007/978-3-642-21461-5_20 http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://hal.inria.fr/hal-01583314 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. pp.304-318, ⟨10.1007/978-3-642-21461-5_20⟩ [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] info:eu-repo/semantics/conferenceObject Conference papers 2011 ftccsdartic https://doi.org/10.1007/978-3-642-21461-5_20 2021-02-28T01:25:54Z 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. Conference Object Iceland Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) 304 318 |
institution |
Open Polar |
collection |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
op_collection_id |
ftccsdartic |
language |
English |
topic |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
spellingShingle |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Slåtten, Vidar Herrmann, Peter Contracts for Multi-instance UML Activities |
topic_facet |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
description |
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. |
author2 |
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 |
author |
Slåtten, Vidar Herrmann, Peter |
author_facet |
Slåtten, Vidar Herrmann, Peter |
author_sort |
Slåtten, Vidar |
title |
Contracts for Multi-instance UML Activities |
title_short |
Contracts for Multi-instance UML Activities |
title_full |
Contracts for Multi-instance UML Activities |
title_fullStr |
Contracts for Multi-instance UML Activities |
title_full_unstemmed |
Contracts for Multi-instance UML Activities |
title_sort |
contracts for multi-instance uml activities |
publisher |
HAL CCSD |
publishDate |
2011 |
url |
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 |
op_coverage |
Reykjavik,, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://hal.inria.fr/hal-01583314 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. pp.304-318, ⟨10.1007/978-3-642-21461-5_20⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_20 hal-01583314 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 doi:10.1007/978-3-642-21461-5_20 |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-642-21461-5_20 |
container_start_page |
304 |
op_container_end_page |
318 |
_version_ |
1766039592658534400 |