基于迁移系统分析的线性混成系统安全验证

摘要：

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

关键词：线性混成自动机、迁移系统、安全性验证、不变式生成

所属期刊栏目：49

分类号：TP311(计算技术、计算机技术)

资助基金：江苏省自然科学基金BK2011558

在线出版日期：2013-04-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：58-64,76