Abstract:

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. We present C&C views, which specify structural properties of C&C 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.

We consider two applications of C&C views. First, 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. We present recent experiences from applying C&C view verification with Daimler AG on industrial size Simulink models.

Second, 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. 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. Recently, we have addressed the case where a C&C views specification is unsatisfiable. We have defined C&C views specification cores and show how to compute them as minimal explanations for unsatifiability.

Summarizing papers from FSE’13, ICSE’14, MoDELS’17 Practice & Innovation, and MoDELS’17 Foundations Track.