Correct Integration of Discrete and Continuous Models – DISCONT

Cyber-Physical Systems (CPSs) connect the real world to software systems through a network of sensors and actuators: physical and logical (computational) components interact in complex ways, depending on context, and involving different spatial and temporal scales. There is a diverse range of application domains, including: health, energy, autonomous vehicles and robotics; and many of these include safety critical requirements. One of the most common architectures found in CPSs is a discrete software controller which interacts with its physical environment in a closed-loop schema where input from sensors is processed and output is generated and communicated to actuators. We are concerned with the verification of the correctness of such discrete controllers, which requires correct integration of discrete and continuous models. Correctness should arise from a design process based on sound abstractions and models of the relevant physical laws. In general, such physical systems are characterized by differential equations involving solutions in continuous domains; thus further discretisation steps are required. Such discretisation can be achieved by finding approximate solutions to equations in the continuous domain model (typically through integration). Consequently, the correct operation of a controller must now be established within a specific error bound of approximation. Overall, we aim to bridge the gap between the discrete and continuous worlds of formal methods and control theory. We will lift the level of abstraction above that which is found in current bridging techniques. In order to achieve this, we propose to focus on 5 high-level objectives: (O1) develop a formal hybrid model; (O2) demonstrate refinement steps for different types of control requirements; (O3) propose a rational step-wise design method and support bf tools; (O4) validate the theory/models, based on classic problems from the discrete controller corpus; and (O5) validate the rational process, based on use cases from a range of application domains.