基于常规工程模型的组合形式化分析
软件工程
2020-04-09 v1 系统与控制
系统与控制
摘要
形式化方法在状态空间探索中的应用已成功用于评估鲁棒关键软件系统。形式化方法能够发现常规测试可能遗漏的错误条件,并可辅助规划复杂系统操作。然而,形式化方法的广泛应用受限于为真实系统生成形式化规约所需的工作量。本文提出基于数据的状态链接接口合规引擎(SLICED),一种通过利用常规工程模型推导组合形式化状态模型并生成关于状态机的形式化断言的方法来应对形式化状态机规约生成的复杂性。我们使用 NASA 发布的 Virtual ADAPT 模型演示 SLICED,并通过 Simulink 复现结果以验证我们的工作。
引用
@article{arxiv.2004.03666,
title = {Compositional Formal Analysis Based on Conventional Engineering Models},
author = {Tyler D. Smith and Ryan Peroutka and Robert Edman},
journal= {arXiv preprint arXiv:2004.03666},
year = {2020}
}