Taming Hierarchical Connectors
Ref: CISTER-TR-200104 Publication Date: 1 to 3, May, 2019
Taming Hierarchical ConnectorsRef: CISTER-TR-200104 Publication Date: 1 to 3, May, 2019
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.
8th IPM International Conference on Fundamentals of Software Engineering (FSEN 2019), pp 186-193.
Notes: Part of the Lecture Notes in Computer Science book series (LNCS, volume 11761)