Abstract:
Cyber-Physical Systems (CPSs) incorporate sets of controllers for managing sets of physical processes. Controllers are distributed, and interact with one another using appropriate networking protocols. Examples range from biomedical devices implanted in the human body in order to regulate the behaviour of certain organs to embedded controllers used in automotive applications. To safely control their real-world safety-critical applications, CPS must be verified to have reactive and real-time properties. Traditionally, controllers for CPS are designed using the Model-Based Design (MBD) approach. Here, high-level formal models are used for analysis and validation. Then validated models are passed through robust compilers to derive ‘correct-by-construction’ implementations. The MBD approach offers many benefits to ensure the safety and verification of safety critical systems. However, conventional MBD approaches are now being challenged due to the recent push for integration of Artificial Intelligence (AI) based controllers such as neural networks. These are instead developed using data-driven techniques. For example, in a modern autonomous vehicle, pedestrian detection will rely on machine learning techniques over data collected from sensors such as LiDARs or cameras. Controllers utilising these data-driven processing techniques are not well suited to MBD. However, safety critical systems such as autonomous vehicles still need to be validated. As such, how can we mix diverse conventional controllers which interact with the new type of data-driven controllers, while ensuring safety? This thesis tries to address this question within the setting of a one year research masters. The main focus area is within the compositional design of CPS controllers. We argue that these increase the predictability of systems featuring both data-driven and MBD-designed controllers. Advantages such as flexibility in the face of requirement changes are demonstrated, showing how AI based CPS may be deployed to complex and unpredictable environments. This thesis thus develops a framework for the compositional design of AI based CPS. In doing so, we propose techniques for the systematic composition of neural networks with conventional controllers. We develop automated code generators such that the generated code is correct by construction and amenable to Worst-Case Execution Time (WCET) analysis. To demonstrate the efficacy of the approach, we also show that the developed code is competitive relative to Tensorflow Lite, an industry standard for similar systems. We also show how we can add additional runtime elements for AI based controllers so that they may be able to deal with requirements changes without needing redesign or re-training of their controllers. Our results are presented through three major case studies: (1) a car following controller, (2) a pedestrian detection requirements change for a pre-trained neural network, and (3) an industrial load frequency controller where AI systems are composed with conventional PID commands.