Machine Learning for Cyber-Physical Systems Verification (available)

Starting Date: June 2019
Duration: 10 weeks
Time commitment: Full time
Prerequisites: desirable experience with machine learning/neural net library; eager to learn about formal verification of hybrid systems

Hybrid automata (HA) [1] 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 is crucial for such safety-critical applications, as it provides mathematically rigorous proofs of correctness (whether or not the system satisfy the desired specification). HA verification often boils down to reachability checking, that is, verifying whether an unsafe HA state can be reached from an initial set of states. However, state-of-the-art reachability techniques [2,3,4] are computationally expensive, and thus, can only be applied offline at design-time.

To make reachability analysis efficient and suitable for online/runtime analysis, in [5] we presented Neural State Classification (NSC), a method based on machine learning and neural networks where reachability checking is reduced to a supervised binary classification problem, i.e., given an HA state, classify whether or not that state can reach an unsafe configuration. Up to now, NSC has been successfully applied to a relatively small benchmark of seven HA models.

The goal of this project is to evaluate NSC on a larger benchmark of cyber-physical system models [6]. For this purpose, you will generate training and test data for all the HA models in the benchmark by executing adequate reachability checkers and use the data to train the NSC neural networks and evaluate their accuracy. Where the accuracy is not satisfactory, you will experiment with different architectures and sample sizes. If time permits, you will extend NSC with methods for graph embedding like [7], to account for the graph-like structure of the HA (neglected in the current NSC implementation).

 

[1] Henzinger, Thomas A. “The theory of hybrid automata.” Verification of Digital and Hybrid Systems. Springer, Berlin, Heidelberg, 2000. 265-292.
[2] Kong, Soonho, et al. “dReach: δ-reachability analysis for hybrid systems.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2015.
[3] Frehse, Goran, et al. “SpaceEx: Scalable verification of hybrid systems.” International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2011.
[4] Chen, Xin, Erika Ábrahám, and Sriram Sankaranarayanan. “Flow*: An analyzer for non-linear hybrid systems.” International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2013.
[5] Phan, Dung, et al. “Neural state classification for hybrid systems.” International Symposium on Automated Technology for Verification and Analysis. Springer, Cham, 2018.
[6] X. Chen, S. Schupp, I. B. Makhlouf, E. Ábrahám, G. Frehse, and S. Kowalewski. A benchmark suite for hybrid systems reachability analysis. In NASA Formal Methods Symposium, pages 408–414. Springer, 2015
[7] Belkin, Mikhail, and Partha Niyogi. “Laplacian eigenmaps for dimensionality reduction and data representation.” Neural Computation 15.6 (2003): 1373-1396.