论文研究-基于迁移系统分析的线性混成系统安全验证.pdf

混成自动机行为中既包含离散行为又包含连续行为，非常复杂。其安全性验证问题难以解决，即使是线性混成自动机，它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集，复杂度高，可处理问题规模非常有限。为了避免这类问题，实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统，并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明，方法有效可行，工具具有良好的性能。