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.