Computer Science ›› 2013, Vol. 40 ›› Issue (12): 133-140.

Previous Articles     Next Articles

Description and Combination of CSP Process Based on ASP

ZHAO Ling-zhong,SITU Ling-yun,ZHAI Zhong-yi and QIAN Jun-yan   

  • Online:2018-11-16 Published:2018-11-16

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

[1] Hoare C A R.Communicating Sequential Processes [M].ht-tp://www.usingcsp.com/cspbooks,2004
[2] Roscoe A W.The Theory and Practice of Concurrency [M].Prentice Hall,1998
[3] Clarke E M,Grumberg O,Peled D.Model Checking [M].Cambridge:MIT Press,2001:35-49
[4] Baral C.Knowledge Representation,Reasoning,and Declarative Problem Solving [M].Cambridge Press,2003
[5] 赵岭忠,张超,钱俊彦.基于ASP的CSP并发系统验证研究[J].计算机科学,2012,9(12):133-136
[6] Durobvin J.Efficient Symbolic Model Checking of Concurrent System [D].Aalto University School of Science Department of Information of Computer Science,Doctoral Dissertation,2011
[7] D’Silva V,Kroening D,Weissenbacher G.A Survey of Automated Techniques for Formal Software Verification [J].IEEE Trans.on CAD of Integrated Circuits and Systems,2008,27(7):1165-1178
[8] Heljanko K,Niemel I.Bounded LTL model checking with stable models [J].TPLP,2003(4/5):519-550
[9] Armstrong P J,Goldsmith M,Lowe G,et al.Recent Developments in FDR [J].CAV,2012,7358:699-704
[10] Palikareva H,Ouaknine J,Roscoe B.Faster FDR Counterexample Generation Using SAT-Solving [C]∥ECEASST.2009
[11] Leone N,Pfeifer G,Faber W,et al.The DLV system for know-ledge representation and reasoning [J].ACM TOCL,2006,7(3):499-562
[12] Lierler Y,Maratea M.Cmodels-2:SAT-Based Answer Set Solver Enhanced to Non-tight Programs [J].Proc.LPNMR,2004,2923:346-350
[13] Ilik D,Lee G,Herbelin H.Kripke models for classical logic [J].Ann.Pure Appl.Logic,2010,1(11):1367-1378
[14] De Angelis E,Pettorossi A,Proietti M.Synthesizing Concurrent Programs Using Answer Set Programming [J].Fundam.Inform,2012,0(3/4):205-229
[15] 蒋屹新,林闯,曲扬,等.基于Petri网的模型检测研究[J].软件学报,2004,15(9):1265-1276
[16] Niemel I,Simons P,Syrjnen T.Smodels:A System for Answer Set Programming [C]∥Proceeding of the 8th International Workshop on Non-Monotonic Reasoning.2000

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!