Verifying Component and Connector Models against Crosscutting Structural Views
This work addresses the verification of structural properties in software engineering models for engineers, but it is incremental as it builds on existing C&C view concepts.
The authors tackled the problem of verifying component and connector (C&C) models against structural views by developing efficient polynomial-time algorithms to decide satisfaction, and they demonstrated this with a prototype tool evaluated on four example systems, including performance tests and a user study on witness usefulness.
The structure of component and connector (C&C) models, which are used in many application domains of software engineering, consists of components at different containment levels, their typed input and output ports, and the connectors between them. C&C views, presented in [24], can be used to specify structural properties of C&C models in an expressive and intuitive way. In this work 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 naturallanguage 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.