ASP based property verification of communication protocols described by CSP

作者：Zhao Lingzhong; Zhang Liqin; Qian Junyan^*; Zhang Haitao; Zhu Ying

来源：Journal of Computational Information Systems, 2014, 10(11): 4929-4936.

DOI：0.12733/jcis10748

• ASP
• Concurrent systems
• Conversion process
• CSP
• Operational semantics
• Property verification
• Refinement checking
• Verification framework

Existing CSP model checkers are based on operational semantics, which need to translate processes into a label transition system. The conversion process is complex. Moreover, in most CSP model checkers, the properties to be verified are described by CSP, which is helpful for refinement checking, but leads to limited description power and weak generality. Therefore, ASP techniques have been proposed to verify CSP concurrent systems in our previous work. However, the methods are inadequate for verifying communication protocols, which may include assignment operator and an event contains channel and message. In this paper, a significant extension to the previous verification framework is proposed, which includes the ASP representation of prefix and assignment operator and concurrency rules. Practice with AB protocol shows the correctness and feasibility of the method for verifying communication protocols.

• 出版日期2014