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

Jingyi Wang, Jun Sun, Shengchao Qin, Cyrille Jegourel

Research output: Contribution to journalArticleResearchpeer-review

7 Downloads (Pure)

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.
Original languageEnglish
Number of pages15
JournalIEEE Transactions on Software Engineering
DOIs
Publication statusPublished - 14 Dec 2018

Fingerprint

Large scale systems
Model checking
Water treatment
Systems analysis
Sampling
Monitoring
Testing

Cite this

@article{be5bf4a44c4d4e81b2a08d01997912d7,
title = "Automatically ‘Verifying’ Discrete-Time Complex Systems through Learning, Abstraction and Refinement",
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.",
author = "Jingyi Wang and Jun Sun and Shengchao Qin and Cyrille Jegourel",
year = "2018",
month = "12",
day = "14",
doi = "10.1109/TSE.2018.2886898",
language = "English",
journal = "IEEE Transactions on Software Engineering",
issn = "0098-5589",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

Automatically ‘Verifying’ Discrete-Time Complex Systems through Learning, Abstraction and Refinement. / Wang, Jingyi; Sun, Jun; Qin, Shengchao; Jegourel, Cyrille.

In: IEEE Transactions on Software Engineering, 14.12.2018.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Automatically ‘Verifying’ Discrete-Time Complex Systems through Learning, Abstraction and Refinement

AU - Wang, Jingyi

AU - Sun, Jun

AU - Qin, Shengchao

AU - Jegourel, Cyrille

PY - 2018/12/14

Y1 - 2018/12/14

N2 - 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.

AB - 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.

U2 - 10.1109/TSE.2018.2886898

DO - 10.1109/TSE.2018.2886898

M3 - Article

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

SN - 0098-5589

ER -