基于迁移系统分析的线性混成系统安全性验证工具
混成自动机行为中既包含离散行为又包含连续行为，非常复杂。因此其安全性验证问题也难以解决，即使是线性混成自动机，它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集，复杂度高，可处理问题规模非常有限。本文中我们提出了一种新的工具，该工具将线性混成自动机表达为等价的迁移系统，并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明，方法有效可行，工具具有良好的性能。
线性混成自动机 迁移系统 安全性验证 不变式生成
蒋慧 卜磊 李宣东
南京大学计算机软件新技术国家重点实验室,江苏南京 210046;南京大学 计算机科学与技术系,江苏 南京 210046
国内会议
南京
中文
1-8
2012-10-20（万方平台首次上网日期，不代表论文的发表时间）