.png){kind=icon}
.png){kind=icon}
Return
Automatically 'Verifying' Discrete-Time Complex Systems through Learning, Abstraction and Refinement
.png){kind=icon}
OA
AI
DOI：10.1109/TSE.2018.2886898.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Precisely modeling complex systems like cyber-physical systems is challenging, which often renders 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 ormodel-based testing. Our method has been implemented as a self-contained software toolkit. The evaluation on multiple benchmark systems as well as a real-worldwater treatment system shows promising results.
Keywords:
Verification
model learning
abstraction refinement
cyber-physical system
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
5.6
Papers:
2.8K
Citations:
1.1W