基于ASP的CSP进程描述与组合研究

作     者：赵岭忠 司徒凌云 翟仲毅 钱俊彦 ZHAO Ling-zhong;SITU Ling-yun;ZHAI Zhong-yi;QIAN Jun-yan

作者机构：桂林电子科技大学计算机科学与工程学院桂林541004 广西可信软件重点实验室桂林541004 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2013年第40卷第12期

页      面：133-140页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金(61262008 61100186 61063002) 广西自然基金(2011GXNS FA018166 2011GXNSFA018164) 广西可信软件重点实验室基金项目(kx201113)资助 

主　　题：CSP ASP 模型检测 

摘      要：前期工作中,为解决CSP模型检测不支持一次运行验证多条性质的问题,构建了基于ASP的CSP模型检测框架,但其存在着可描述并发进程形态不完善与可验证并发系统规模受限的问题。构建了全新的并发系统ASP描述体系,其解决了前期工作中前缀描述不允许出现类环状结构的问题,可完整描述各种形态的CSP进程。研究了并发组合进程生成技术,它可使多个进程自动化并发组合,并生成一个满足所有行为特性、具有一致结构特性的新进程,保持了验证框架内进程描述的一致性,有利于并发进程的抽象与验证。实验表明了基于ASP的CSP进程描述与组合进程生成技术的有效性,以及基于该ASP描述体系的系统性质验证的可行性。