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

• 作者: 卜磊 李宣东 蒋慧
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 线性混成自动机 迁移系统 安全性验证 不变式生成
• 年，卷（期）: 2013,（4）
• 所属期刊栏目: 理论研究、研发设计
• 页码范围: 58-64,76
• 页数: 8页
• 分类号: TP311
• 字数: 4577字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1208-0548

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李宣东	南京大学计算机软件新技术国家重点实验室	72	1417	20.0	36.0
5	卜磊	南京大学计算机软件新技术国家重点实验室	6	47	3.0	6.0
9	蒋慧	南京大学计算机软件新技术国家重点实验室	1	5	1.0	1.0