Magnifier：一种用于自主交通控制的组合式分析方法
软件工程
2021-03-12 v3 形式语言与自动机理论
摘要
自主交通控制系统是具有关键目标的大规模系统。由于这些系统所处外部世界的动态性，确保其在运行时以及发生变化时满足自身属性十分重要。保证这些系统正确行为的一种突出方法是在运行时验证，该方法具有严格的时间和内存限制。为应对这些限制，我们提出 Magnifier，一种基于组件模型运行的迭代、增量且组合式的验证方法。Magnifier 的思想是聚焦于受变更影响的组件，在将组件适配于变更后验证系统相关属性的正确性，随后放大视野并在变更传播时追踪之。若变更传播，则所有受影响的组件均被适配并组合以形成一个新组件。Magnifier 对新组件重复相同过程。该迭代过程在变更传播停止时终止。在 Magnifier 中，我们使用交通控制系统的协调自适应参与者模型（CoodAA）。我们给出 CoodAA 作为定时输入输出自动机（TIOAs）网络的形式化语义。若适配组件的 TIOAs 与其环境兼容，则变更不会传播。我们在 Ptolemy II 中实现了我们的方法。实验结果表明，与非组合式方法相比，所提方法改善了验证时间与内存消耗。
引用
@article{arxiv.1905.06732,
title = {Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control},
author = {Maryam Bagheri and Marjan Sirjani and Ehsan Khamespanah and Christel Baier and Ali Movaghar},
journal= {arXiv preprint arXiv:1905.06732},
year = {2021}
}