关键词: CSP,ASP,模型检测

Abstract: In the previous work,an ASP based framework,which is used to verify the model described by CSP,was proposed to solve the problem of verifying multiple properties in one run of a model checker．However,some problems still exit,which include the inability to describe some forms of concurrent process and the scale limitation of the concurrent systems that can be described．In this paper,a new description system for concurrent systems was constructed,which allows loop structure in prefix process,and therefore can be used to describe various forms of concurrent processes．It allows several processes to be combined automatically to generate a new process,which not only fulfills all behavioral characteristics but also keeps the structural consistency with the original processes．In this way,the process description within the verification framework follows a uniform style,which is helpful for the abstraction and validation of concurrent processes．The effectiveness of the ASP description system and the combination process generation technique,and the feasibility of the verification based on the description system were illustrated by examples.

Key words: CSP,ASP,Model checking