Component-based specification, design and verification of adaptive systems

Control systems are typically tightly embedded into their environment to enable adaptation to environmental effects. As the complexity of such adaptive systems is rapidly increasing, there is a strong need for coherent tool-centric approaches to aid their systematic development. This paper proposes an end-to-end component-based specification, design and verification approach for adaptive systems based on the integration of a high-level scenario language (sequence chart variant) and an adaptation definition language (statechart extension) in the open source Gamma tool. The scenario language supports high-level constructs for specifying contracts and the adaptation definition language supports the flexible activation and deactivation of static contracts and managed elements (state-based components) based on internal changes (e.g., faults), environmental changes (e.g., varying context) or interactions. The approach supports linking managed elements to static contracts to formally verify their adherence to the specified behavior at design time using integrated model checkers. Implementation can be derived from the adaptation model automatically, which can be tested using automated test generation and verified at runtime by contract-based monitors.