Structural Views for Component and Connector Models
S. Maoz, J.O. Ringert, and B. RumpeComponent and connector views
We present component and connector (C&C) views, which specify structural properties of component and connector models in an expressive and intuitive way. C&C views provide means to abstract away direct hierarchy, direct connectivity, port names and types, and thus can crosscut the traditional boundaries of the implementation-oriented hierarchical decomposition of systems and sub-systems, and reflect the partial knowledge available to different stakeholders involved in a system's design.
C&C views resources- C&C views synthesis and verification plug-in prototype implementation (download as Eclipse feature, compatible with version 3.6.2 or later (tested with Eclipse 4.2 Juno), for Windows only), installation instructions in the readme below.
- C&C views language definition, syntax of MontiArcView explained with simple examples
Verification
We address the verification of a C&C model
against a C&C view and present efficient (polynomial) algorithms to decide satisfaction.
A unique feature of our work, not present in existing approaches to
checking structural properties of C&C models, is the generation of
witnesses for satisfaction/non-satisfaction and of short natural-language
texts, which serve to explain and formally justify
the verification results and point the engineer to its causes.
A prototype tool and an evaluation over four example
systems with multiple views, performance and scalability
experiments, as well as a user study of the usefulness of
the witnesses for engineers, demonstrate the contribution of
our work to the state-of-the-art in component and connector
modeling and analysis.
S. Maoz, J. O. Ringert, B. Rumpe: Verifying Component and Connector Models against Crosscutting Structural Views. In: 36th International Conference on Software Engineering (ICSE 2014). Pages 95-105. Hyderabad, India, ACM New York, June 2014.
Supporting materials for verification- Verification algorithm report, includes the verification algorithm, correctness and completeness proofs, and witness generation algorithms.
- C&C views verification plug-in readme, includes screen captures and installation instructions for the plug-in.
- Evaluation project, includes C&C views and C&C views specifications, for use after the plug-in is installed.
- C&C views exercise (pdf) of a user study and the raw data of 22 entries.
Synthesis
As one application for C&C views we investigate the synthesis problem:
given a C&C views specification, consisting of mandatory, alternative, and
negative views, construct a concrete satisfying C&C model, if one exists. We
show that the problem is NP-hard and solve it, in a bounded scope, using a
reduction to SAT, via Alloy. We further extend the basic problem with support
for library components, specification patterns, and architectural styles. The
result of synthesis can be used for further exploration, simulation, and
refinement of the C&C model or, as the complete, final model itself, for
direct code generation.
A prototype tool and an
evaluation over three case studies show promising results and suggest
interesting future research directions towards a comprehensive design
environment for architecture synthesis.
S. Maoz, J. O. Ringert, B. Rumpe: Synthesis of Component and Connector Models from Crosscutting Structural Views. Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'13), Eds.: B. Meyer, L. Baresi, M. Mezini, pages 444-454, ACM New York, 2013.
Supporting materials for synthesis- C&C views synthesis plug-in readme, includes screen captures and installation instructions for the plug-in.
- Evaluation project, includes C&C views and C&C views specifications, for use after the plug-in is installed.
- Case studies details document, includes all C&C views, C&C views specifications, and synthesized C&C models referenced in the paper.