Analysis and Synthesis of Interactive Component and Connector Systems

The development of distributed interactive systems is a challenging endeavor. Component and connector (C&C) architecture descriptions address complexity of systems by logical and physical decomposition of systems into subsystems. C&C descriptions model components with well-defined interfaces and component interaction via connectors.

Current modeling and specification mechanisms rely on the traditional, implementation-oriented hierarchical decomposition of systems into subsystems. We introduce modeling languages and methods that crosscut these boundaries. Usage scenarios include formalizing crosscutting knowledge available to different stakeholders about the C&C structure, behavior, and interaction of the system.

We present a language for design decisions on a system's decomposition and connectivity in partial C&C views. This language enriches C&C modeling with powerful abstraction mechanisms for hierarchical containment, connectedness, and interfaces. An analysis method verifies whether a C&C model satisfies a C&C view. A synthesis method computes a satisfying C&C model for valid, invalid, alternative, and dependent designs, if one exists.

We present a language for automata embedded in components that interact via messages over components' ports with various mechanisms for underspecification. Tool support verifies the implementation of C&C systems' behavior against underspecified models and generates executable code. The verification enables incremental development of component behavior based on stepwise refinement. Prototype implementations and evaluation in a user study, a case study, and over example systems show promising results towards a comprehensive model-based development environment for interactive C&C systems.