面向不确定信息物理系统的验证
软件工程
2017-05-02 v1 系统与控制
摘要
信息物理系统(CPS)对验证与确认提出了超越基于高层模型的功能正确性证明的新挑战。特别是对于形式化方法而言，其特殊挑战在于异构性和可扩展性。对于数值仿真，不确定行为很难被全面覆盖，这促使了符号方法的使用。本文描述了一种基于符号仿真的不确定CPS验证方法。我们定义了不确定计算的符号模型与表示：仿射算术决策图(Affine Arithmetic Decision Diagrams)。然后我们将该方法集成到支持不同计算模型仿真的SystemC AMS仿真器中。我们通过分析一个具有不确定性、自诊断和错误反应的水位监测器来演示该方法。
引用
@article{arxiv.1705.00519,
title = {Towards Verification of Uncertain Cyber-Physical Systems},
author = {Carna Radojicic and Christoph Grimm and Axel Jantsch and Michael Rathmair},
journal= {arXiv preprint arXiv:1705.00519},
year = {2017}
}
备注
In Proceedings SNR 2017, arXiv:1704.02421