Machine Learning for Cyber-Physical Systems Monitoring (available)

Starting Date: June 2020
Prerequisites: Good knowledge of Python, familiar with (or eager to learn about) neural networks and deep learning libraries like tensorflow, eager to learn about basics of hybrid systems verification.
Will results be assigned to University:

Hybrid automata (HA) are a formal model for cyber-physical systems, i.e., systems characterised by digital components (discrete) that control and interact with the physical environment (continuous). HAs have been applied to system designs in numerous domains including avionics, automotive, medical devices, and robotics. Formal verification of HAs can establish, with provable correctness guarantees, whether or not there exist a trajectory of the HA model that can reach some unsafe state. This kind of analysis is crucial for safety-critical applications, but computationally expensive, and thus, suitable only for offline design-time analysis.

In collaboration with the University of Trieste and Stony Brook University, we developed neural predictive monitoring (NPM), a method based on machine learning for predicting, at runtime, reachability of HA models. The method consists of three main components:

  1. A predictor, that is, a neural network model for reachability prediction, trained offline via supervision from a precise (expensive) reachability checker
  2. A rejection rule, which uses measures of prediction uncertainty to optimally decide whether or not a reachability prediction can be trusted
  3. An active learning procedure, which identifies the HA states for retraining that best improve the predictor and the rejection rule

In this project, you will consolidate existing code for NPM to produce a usable software tool, including interfacing with the main HA model checkers, evaluation on an extended benchmark of case studies, and efficient compilation into mobile and IoT devices.

Useful readings: