迈向“验证”一个水处理系统
人工智能
2019-11-22 v2 软件工程
摘要
对真实世界的信息物理系统建模与验证颇具挑战，对于手动建模不可行的复杂系统尤为如此。本工作中，我们报告了结合模型学习与抽象精化来分析一个具挑战性系统（即真实世界的 Secure Water Treatment 系统（SWaT））的经验。给定一组安全性需求，目标是表明系统以高概率安全（从而因安全违例而触发的系统停机很少）或不安全。由于系统过于复杂而无法手动建模，我们应用最新的自动模型学习技术，基于两段长的系统执行日志（一段训练、一段测试）通过抽象与精化构建一组马尔可夫链。对每一条概率安全性质，我们要么以某一概率置信度报告其不成立，要么通过以抽象马尔可夫链形式展示证据来报告其成立。这些马尔可夫链随后可作为运行时监视器在 SWaT 中实现。
引用
@article{arxiv.1712.04155,
title = {Toward `verifying' a Water Treatment System},
author = {Jingyi Wang and Jun Sun and Yifan Jia and Shengchao Qin and Zhiwu Xu},
journal= {arXiv preprint arXiv:1712.04155},
year = {2019}
}
备注
Accepted by FM 2018