Formal Analysis of Cyber-physical Systems
Formally modelling and verifying a complex CPS is extremely challenging, can we automatically learn for verifying such systems without manual modelling?
Series of Works
- [ETAPS/FASE 2017, STTT 2018] Conducted an empirical study on learning probabilistic models (e.g., discrete-time Markov Chains) from system traces, and proposed a new learning framework based on genetic algorithms.
- [TSE 2018] Proposed a CEGAR-style predicate abstraction-based learning framework to push forward learning to be applicable for large-scale systems with even infinite state space.
- [ICFEM 2017] Proposed an active learning algorithm to sample the system so that a more acurate model can be learned.
- [FM 2018] Conducted a case study of the above learning algorithms on the verification of a real-world testbed, i.e., SWaT.
- [DSN 2018] Proposed an importance sampling algorithm of the learned approximate probabilistic model to obtain a more accurate verification result where rare events are potentially involved.
- [ICSE 2018, ACM SIGSOFT Distinguished Paper Award] Applied the idea of probabilistic learning to model program concolic testing, solved the optimal strategy and proposed a greedy algorithm to approximate the strategy.
Software Engineering for Dependable Artificial Intelligence Systems
AI is deeply interwined with software engineering. While AI systems can be intrinsically vulnerable/discriminative to be trusted, software engineering could help either by testing or formal verification.
Series of Works
- [ICSE 2019] Proposed a runtime detection system framework to filter adversarial samples of deep neural networks. Compared to prior detection algorithms, it is sufficiently efficient to be applicable at runtime.
- [ICSE 2020, ACM SIGSOFT Distinguished Paper Award] Proposed a scalable and efficient algorithm which utilized gradient to search for disciminative samples of deep neural networks, which could be used for data augmentation to improve the model fairness.
- [ASE 2020] Proposed to interprete recurrent neural networks by extracting more tracable, reasonable and transparent models, i.e., probabilistic finite automata. The extracted models can potentially bridge the gap between black-box neural networks and existing model-based analysis methods like testing/attack/adversary detection, predictive analysis and runtime monitoring.
[ICECCS 2020] Conducted an empirical study on the correlation between coverage and robustness for deep neural networks, which is surpringly limited.
- Several other works are in submission.