Automatically 'Verifying' Discrete-Time Complex Systems through Learning, Abstraction and Refinement

TL;DR

This paper introduces LAR, an automated method combining learning, abstraction, and refinement to verify complex discrete-time systems using log traces, enabling probabilistic verification and system analysis.

Contribution

The paper presents a novel LAR approach that automatically learns and refines models from logs for verifying complex systems without full model knowledge.

Findings

Effective on benchmark systems and real-world water treatment system

Produces probabilistic models with bounded spurious counterexamples

Enables verification, runtime monitoring, and testing

Abstract

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.