中文摘要：

针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。

英文摘要：

Aiming at lack of activity description and the complexity of models transition of CSP model checkers,CSP model checking based on ASP and stable failure semantics is proposed.In this method,the properties are specified by linear temporal logic（LTL）,the description of CSP system and LTL properties are implemented with answer set programming（ASP）,then multiple properties are verified in one execution of ASP solvers.The experimental result shows that the method expands the scope of liveness properties based on stable failure model,and prevents transition from different models.