Computer Science ›› 2013, Vol. 40 ›› Issue (11): 181-186.

Previous Articles     Next Articles

Framework for Model Checking CSP with Traces of Processes

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

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

Abstract: Communicating Sequential Processes is a classic method for describing concurrent systems and network security protocols.The verification for CSP is a complex conversion process,which translates processes into a label transition system and describes the properties to be verified with traces.The main problem of the method is in the description of liveness properties.This paper proposed a framework for model checking CSP with traces,in which properties are specified by LTL,a universal property specification language.Finally,a verification system for CSP was implemented with answer set programming.It is shown that the ability of the system for describing CSP processes is more powerful and the verification accuracy of the system is higher than the similar system developed previously.When a property is not qualified,the system returns counterexamples for the property.

Key words: Communicating sequential processes,Concurrent system,Trace model,Answer set programming

[1] Hoare C A R.Communicating Sequential Processes .http://www.usingcsp.com/cspbooks,2012
[2] Art K R.Ten years of Hoare’s logic,A survey—Part I[J].ACM TOPLAS,1981,3(4):431-483
[3] Roscoe A W,Gardiner P H B,Goldsmith M H,et al.Hierarchical compression for model-checking CSP or how to check10dining philosophers for deadlock[C]∥Proceedings of the 1st TACAS,BRICS Notes Series NS-95-2.Department of Computer Science,University of Aarhus,1995
[4] Roscoe A W.Model Checking CSP[M]∥A classical mind:essays in honour of C.A.R.Hoare.Prentice Hall,1994
[5] Armstrpng P,Lowe G,Ouaknine J,et al.Model checking timed CSP[C]∥To appear in proceedings of HOWARD,Easychair,2012
[6] Armstrpng P,Goldsmith M H,Lowe G,et al.Recent develop-ments in FDR2[C]∥Proceedings of CAV.2012:699-704
[7] 赵岭忠,张超,钱俊彦.基于ASP的CSP并发系统验证研究[J].计算机科学,2012,9(12):133-136
[8] Baier C,Katoen J-P.Principles of model checking[M].Cambridge,Massachusetts :The MIT Press,2007
[9] Hoare C A R.A model for communicating sequential processes [M]∥McKeag,MacNaughten,eds.On the construction of programs. Cambridge University Press,1980
[10] Roscoe A W.The Theory and Practice of Concurrency [M].Prentice Hall,1998
[11] Lifschitz V.What is answer set programming? [C]∥Procee-dings of the AAAI Conference on Artificial Intelligence.2008:1594-1597
[12] Niemel I,Simons P,Syrjnen T.Smodels:a system for answer set programming[C]∥Proceedings of the 8th International Workshop on Non-Monotonic Reasoning.Brenkenridge,Colorado,USA,2000
[13] Lin Fang-zhen,Zhao Yu-ting.ASSAT:computing answer sets of a logic program by SAT slover[J].Artificial Intelligence,2004,157(1/2):115-137
[14] Lifschitz V,Turner H.Splitting a logic program[C]∥Procee-dings of the Eleventh International Conference on Logic Programming.2008:23-37
[15] Baral C.Knowledge Representation,Reasoning,and Declarative Problem Solving [M].Cambridge Press,2003
[16] Heljanko K,Niemel I.Bounded LTL model checking with sta-ble models [J].Theory and Practice of Logic Programming,2003,4(3):519-550
[17] Leone N,Pfeifer G,Faber W,et al.The DLV system for knowledge representation and reasoning [J].ACM Transactions on Conputational Logic,2006,3(7):499-562
[18] 陆汝钤.计算机语言的形式语义[M].北京:科学出版社,1992
[19] Brookes S D,Hoare C A R,Roscoe A W.A theory of communicating sequential processes [J].Journal of the ACM,1984,31(3):560-599
[20] Palikareva H,Ouaknine J,Roscoe A W.SAT-solving in CSPtrace refinement [J].Science of Computer Programming.Special issue on Automated Verification of Critical Systems,2012,7(10/11):1178-1197
[21] Ranzato F.On the completeness of model checking[C]∥Proc.ESOP’01,LCNS 2028.Springer,1999:137-154
[22] Giacobazzi R,Ranzato F.States vs.traces in model checking[C]∥Proc.9th International Static Analysis Symposium(SAS’02).LNCS 2477,2002:461-476
[23] Howard Y,Gruner S,Gravell A,et al.Model-based trace checking [C]∥SoftTest:UK Software Testing Research Workshop II.2003

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!