Please use this identifier to cite or link to this item:
Title: Taming hierarchical connectors
Author: Proença, José
Madeira, Alexandre
Keywords: Dynamic logic
Software connectors
Formal methods
Issue Date: 2019
Publisher: Springer
Abstract: Building and maintaining complex systems requires good software engineering practices, including code modularity and reuse. The same applies in the context of coordination of complex component-based systems. This paper investigates how to verify properties of complex coordination patterns built hierarchically, i.e., built from composing blocks that are in turn built from smaller blocks. Most existing approaches to verify properties flatten these hierarchical models before the verification process, losing the hierarchical structure. We propose an approach to verify hierarchical models using containers as actions; more concretely, containers interacting with their neighbours. We present a dynamic modal logic tailored for hierarchical connectors, using Reo and Petri Nets to illustrate our approach. We realise our approach via a prototype implementation available online to verify hierarchical Reo connectors, encoding connectors and formulas into mCRL2 specifications and formulas.
Peer review: yes
DOI: 10.1007/978-3-030-31517-7_13
ISBN: 978-3-030-31516-0
Publisher Version:
Appears in Collections:CIDMA - Capítulo de livro
AGG - Capítulo de livro

Files in This Item:
File Description SizeFormat 
paper_41.pdf509.92 kBAdobe PDFView/Open

Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.