Automatically 'Verifying' Discrete-Time Complex Systems through Learning, Abstraction and Refinement
This addresses the problem of verifying complex systems for engineers and researchers, but it appears incremental as it builds on existing verification techniques with a learning-based approach.
The authors tackled the challenge of verifying complex systems like cyber-physical systems by proposing LAR, a method that uses learning, abstraction, and refinement from system logs to produce probabilistic models and counterexamples, with evaluation on benchmarks and a real-world water treatment system showing promising results.
Precisely modeling complex systems like cyber-physical systems is challenging, which often render model-based system verification techniques like model checking infeasible. To overcome this challenge, we propose a method called LAR to automatically `verify' such complex systems through a combination of learning, abstraction and refinement from a set of system log traces. We assume that log traces and sampling frequency are adequate to capture `enough' behaviour of the system. Given a safety property and the concrete system log traces as input, LAR automatically learns and refines system models, and produces two kinds of outputs. One is a counterexample with a bounded probability of being spurious. The other is a probabilistic model based on which the given property is `verified'. The model can be viewed as a proof obligation, i.e., the property is verified if the model is correct. It can also be used for subsequent system analysis activities like runtime monitoring or model-based testing. Our method has been implemented as a self-contained software toolkit. The evaluation on multiple benchmark systems as well as a real-world water treatment system shows promising results.