[00044133]一种基于ASP的CSP并发系统调试方法
技术详细介绍
本发明为一种基于ASP的CSP并发系统调试方法，包括以下步骤：步骤1、根据描述CSP并发系统行为特征的ASP规则集，得到实例化性质规则集；步骤2、生成性质成立或不成立的原因；步骤3、生成反例迹并利用反例迹调试系统错误；步骤4、通过性质成立的原因生成ASP规则L，表示系统中使该性质成立的部分系统结构，分析系统修改后对已验证性质的影响，如果新系统满足规则L，性质依然成立，否则性质需要重新验证。本方法采用基于ASP的CSP并发系统的性质验证框架仅需两层模型即可完成性质验证，且两层模型间的差异较小；利用性质不成立时的反例迹实现针对CSP并发系统错误的调试，避免系统部分改变后，对仍成立的性质重复验证。
