BACH:线性混成系统有界可达性模型检验工具

• 作者: 卜磊 李宣东 李游 王林章
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 线性混成系统 线性混成自动机 有界可达性检验 线性规划
• 年，卷（期）: 2011,（4）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 640-658
• 分类号: TP311
• 字数: 13068字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.03766

摘要

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reachability checker),该工具能够沿指定路径(组)对单个线性混成自动机、多个线性混成自动机的组合进行可达性检验,并且在此基础上结合路径遍历技术完成对所有路径的有界可达性检验.实验数据显示,BACH不仅在面向路径可达性检验方面性能优异,可以适用于足够长度的路径,而且在针对所有路径的有界可达性检验时,BACH可以解决的问题规模也远远超过同类工具,已接近工业界应用的要求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王林章	南京大学计算机软件新技术国家重点实验室	23	610	12.0	23.0
5	卜磊	南京大学计算机软件新技术国家重点实验室	6	47	3.0	6.0
9	李游	南京大学计算机软件新技术国家重点实验室	1	23	1.0	1.0