Abstract In many different areas of application, dynamic system models can be decomposed into smaller subsystems according to either their physical or logical nature. Such kind of decomposition is typically helpful for the design and analysis of cyber-physical systems, where logical components – comprising control and state estimation algorithms – alter the dynamics of physical subsystems in a purposeful manner. The structured synthesis and the verification of such cyber-physical systems can be guided by means of methods from the domain of contract-based design. This approach allows for verifying the dynamic behavior of each of the interconnected components independently. Afterwards, conclusions on the behavior of the interconnected system can be made on the basis of operations such as contract composition and contract refinement. In this paper, we present a methodology that employs set-based contract specifications, determined with the help of techniques for reachability analysis to verify the overall system. These contracts are the basis for further stages of controller tuning. Our approach is essentially based on a two-stage procedure. Firstly, a set-based reachability analysis is conduced for models which are subject to uncertain but bounded parameters. These parameter intervals are then restricted further in a contract strengthening stage, complementing the classical concepts of contract refinement and composition, which, among others, allows for selecting optimal constant controller parameters or for determining optimal switching sequences between multiple control laws. Analogously, reconfigurations of the controlled plant can be performed in a similar manner, for example, with the aim to prove the admissibility of reconfiguration approaches in the case of faults that can be mapped onto bounded parameter variations.
Rauh et al. (Mon,) studied this question.