Model Checking CSP Based on ASP and Critical-Trace Model of CSP
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [54]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    Model checking is a mainstream method for formal verification of communicating sequential processes (CSP). Existing CSP model checkers are based on operational semantics, which need to translate processes into a label transition system, and to extract the semantic model based on the 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 at the same time leads to limited description power and weak generality. To address these issues, a new denotational semantic model of CSP, critical-trace model, is proposed and proved to be reliable for model checking CSP. Based on this model, a framework for model checking CSP is established to allow critical-trace model to be constructed inductively from the traces of its components, and properties to be specified by linear temporal logic (LTL), a universal property specification language. In addition, automatic mechanisms for generating critical-trace model and verifying LTL formulas are implemented with answer set programming (ASP). Finally, the two mechanisms are integrated into a CSP model checker T_ASP. Compared with the similar systems developed previously, experimental results indicate a higher ability of the proposed system to describe CSP processes and higher verification accuracy. Furthermore, T_ASP checks multiple properties in one execution of the system. When a property is not satisfied, the system also returns counterexamples for the property.

    Reference
    [1] Hoare CAR. Communicating Sequential Processes. Electronic Version, London: Prentice Hall, 2004. 1-122.
    [2] Isobe Y, Roggenbach M. A complete axiomatic semantics for the CSP stable failures model. In: Proc. of the CONCUR 2006. LNCS, 2006. 158-172. [doi: 10.1007/11817949_11]
    [3] Isobe Y, Roggenbach M. Proof principles of CSP—CSP-Prover in practice. In: Proc. of the LDIC 2007. Springer-Verlag, 2008. 425-442. [doi: 10.1007/978-3-540-76862-3_42]
    [4] O'Reilly L, Roggenbach M, Isobe Y. CSP-CASL-Prover: A generic tool for process and data refinement. Electronic Notes in Theoretical Compututer Science, 2009,250(2):69-84. [doi: 10.1016/j.entcs.2009.08.018]
    [5] Baier C, Katoen JP. Principles of Model Checking. Cambridge: MIT Press, 2007. 1-18.
    [6] Winskel G. Topics in concurrency lecture notes. 2009. 20-24. http://www.cl.cam.ac.uk/~gw104/TIC.pdf
    [7] McMillan KL. Interpolation and SAT-based model checking. In: Proc. of the CAV. 2003. 1-13. [doi: 10.1007/978-3-540-45069- 6_1]
    [8] Een N, Sorensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Compututer Science, 2003, 89(4):543-560. [doi: 10.1016/S1571-0661(05)82542-3]
    [9] Garavel H, Lang F. NTIF: A general symbolic model for communicating sequential processes with data. In: Proc. of the FORTE 2002. 2002. 276-291. [doi: 10.1007/3-540-36135-9_18]
    [10] Holzmann G. The model checker SPIN. IEEE Trans. on Software Engineering, 1997,23(5):279-295. [doi: 10.1109/32.588521]
    [11] Milner R. A Calculus of Communicating Systems. Springer-Verlag, 1980. [doi: 10.1007/978-1-4615-4020-5_2]
    [12] Reisig W. Petri nets and algebraic specifications. Theoretical Computer Science, 1991,80(1):1-34. [doi: 10.1016/0304-3975(91) 90203-E]
    [13] Hoare CAR. A model for communicating sequential processes. In: Mc Keag RM, Mc Naghton AM, eds. On the Construction of Programs. Cambridge University Press, 1980. 33-44.
    [14] SMV System. 2001. http://www.cs.cmu.edu/~modelcheck/smv.html
    [15] Kronos. 1999. http://www-verimag.imag.fr/DIST-TOOLS/TEMPO/kronos/index-english.html
    [16] Truth. 2002. http://www-i2.informatik.rwth-aachen.de/Forschung/MCS/Truth/index.html
    [17] Armstrpng P, Goldsmith MH, Lowe G, Ouaknine J, Palikareva H, Roscoe A W, Worrell J. Recent developments in FDR2. In: Proc. of the CAV. 2012. 699-704. [doi: 10.1007/978-3-642-31424-7_52]
    [18] Failures-Divergence Refinement: FDR2 User Manual. 2010. http://web.comlab.ox.ac.uk/projects/concurrency-tools/
    [19] Parashkevov A, Yantchev J. ARC—A tool for efficient refinement and equivalence checking for CSP. In: Proc. of the IEEE Int'l Conf. on Algorithms and Architectures for Parallel Processing. 1996. 68-75. [doi: 10.1109/ICAPP.1996.562859]
    [20] Sun J, Liu Y, Dong JS, Sun J. Bounded model checking of compositional processes. In: Proc. of the TASE. IEEE, 2008. 23-30. [doi: 10.1109/TASE.2008.12]
    [21] Zhou CH, Liu ZF, Wang CD. Bounded model checking for probabilistic computation tree logic. Ruan Jian Xue Bao/Journal of Software, 2012,23(7):1656-1668 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4089.htm [doi: 10.3724/SP.J. 1001.2012.04089]
    [22] Xia W, Yao YP, Mu XD. Model checking for event graphs and event temporal logic. Ruan Jian Xue Bao/Journal of Software, 2013, 24(3):421-432 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4162.htm [doi: 10.3724/SP.J.1001.2013. 04162]
    [23] Clarke EM, Emerson EA, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009,52:74-84. [doi: 10.1145/1592761.1592781]
    [24] Meulen JV, Pecheur C. Combining partial order reduction with bounded model checking. In: Proc. of the Communicating Process Architectures 2009-WoTUG-32 on Concurrent Systems Engineering Series, Vol.67. 2009. 29-48. [doi: 10.3233/978-1-60750-065- 0-29]
    [25] Peled D. Ten years of partial order reduction. In: Proc. of the 10th Int'l Conf. on Computer Aided Verification (CAV'98). 1998. 17-28. [doi: 10.1007/BFb0028727]
    [26] Biere A. Bounded model checking. In: Frontiers in Artificial Intelligence and Applications. 2003,Chapter 14:457-481. [doi: 10. 3233/978-1-58603-929-5-457]
    [27] Grumberg O, Long DE. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 1994(16): 843-871. [doi: 10.1145/177492.177725]
    [28] Palikareva H, Ouaknine J, Roscoe AW. SAT-Solving in CSP trace refinement. Science of Computer Programming, 2012,77(10-11): 1178-1197. [doi: 10.1016/j.scico.2011.07.008]
    [29] Zhao LZ, Zhang C, Qian JY. ASP-Based verification of concurrent systems described by CSP. Computer Science, 2012,39(12): 133-136 (in Chinese with English abstract).
    [30] Zhao LZ, Zhai ZY, Qian JY. The framework for model checking CSP with traces of processes. Computer Science, 2013,40(11): 181-186 (in Chinese with English abstract).
    [31] Baral C. Knowledge Representation, Reasoning, and Declarative Problem Solving. Cambridge Press, 2003. 1-60.
    [32] Gelfond M, Lifschitz V. The stable model semantics for logic programming. In: Proc. of the Int'l Logic Programming Conf. and Symp. 1988. 1070-1080. [doi: 10.2307/2275201]
    [33] Anger C, Konczak K, Linke T. A glimpse of answer set programming. Kunstliche Intelligenz, 2005,19(1):12-17.
    [34] Smith AM, Mateas M. Answer set programming for procedural content generation: A design space approach. IEEE Trans. on Computational Intelligence and AI in Games, 2011,3(3):187-200. [doi: 10.1109/TCIAIG.2011.2158545]
    [35] Lifschitz V. What is answer set programming? In: Proc. of the AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 2008. 1594-1597.
    [36] Leone N, Pfeifer G, Faber W, Eiter T, Gottlob G, Perri S, Scarcello F. The DLV system for knowledge representation and reasoning. ACM Trans. on Computational Logic, 2006,3(7):499-562. [doi: 10.1145/1149114.1149117]
    [37] Roscoe AW. The Theory and Practice of Concurrency. London: Prentice Hall (Pearson), 1998. 183-218.
    [38] Roscoe AW. Understanding Concurrent Systems. Heidelberg: Springer-Verlag, 2011. 191-317. [doi: 10.1007/978-1-84882-258-0]
    [39] Apt KR. Ten years of Hoare's logic, A survey—Part I. ACM TOPLAS, 1981,3(4):431-483. [doi: 10.1145/357146.357150]
    [40] Heljanko K, Niemelä I. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming, 2003,4(3): 519-550. [doi: 10.1017/S1471068403001790]
    [41] Tang CKF, Ternovska E. Model checking abstract state machines with answer set programming. In: Proc. of the LPAR. 2005. 443-458. [doi: 10.1007/11591191_31]
    [42] Heymans S, Van Nieuwenborgh D, Vermeir D. Synthesis from temporal specications using preferred answer set programming. Lecture Note in Computer Sciences, 2005,3701:280-294. [doi: 10.1007/11560586_23]
    [43] Syrjänen T. Debugging inconsistent answer set programs. In: Dix J, Hunter A, eds. Proc. of the NMR 2006. 2006. 77-83.
    [44] Pontelli E, Son T. Justifications for logic programs under answer set semantics. In: Proc. of the ICLP 2006. Springer-Verlag, 2006. 196-210. [doi: 10.1007/11799573_16]
    [45] Brain M, Gebser M, Puhrer J, Schaub T, Tompits H, Woltran S. Debugging ASP programs by means of ASP. In: Proc. of the LPNMR 2007. Springer-Verlag, 2007. 31-43. [doi: 10.1007/978-3-540-72200-7_5]
    [46] Gebser M, Pührer J, Schaub T, Tompits H. A meta-programming technique for debugging answer-set programs. In: Fox D, Gomes CP, eds. Proc. of the 23rd AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 2008. 13-17.
    [47] Oetsch J, Puhrer J, Tompits H. Catching the ouroboros: Towards debugging non-ground answer-set programs. Theory and Practice of Logic Programming, 2010,10(4-6):513-529.
    [48] Clarke E, Kröning D, Ouaknine J, Strichman O. Completeness and complexity of bounded model checking. In: Proc. of the VMCAI. 2004. 85-96. [doi: 10.1007/978-3-540-24622-0_9]
    [49] Babb J, Lee JY. Module theorem for the general theory of stable models. Theory and Practice of Logic Programming, 2012,12(4-5): 719-735.
    附中文参考文献:
    [21] 周从华,刘志峰,王昌达.概率计算逻辑的限界模型检测.软件学报,2012,23(7):1656-1668. http://www.jos.org.cn/1000-9825/4089. htm [doi: 10.3724/SP.J.1001.2012.04089]
    [22] 夏薇,姚益平,慕晓冬.面向事件图和事件时态逻辑的模型检验方法.软件学报,2013,24(3):421-432. http://www.jos.org.cn/1000- 9825/4162.htm [doi: 10.3724/SP.J.1001.2013.04162]
    [29] 赵岭忠,张超,钱俊彦.基于ASP的CSP并发系统验证研究.计算机科学,2012,39(12):133-136.
    [30] 赵岭忠,翟仲毅,钱俊彦.基于进程迹的CSP模型验证框架.计算机科学,2013,40(11):181-186.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

赵岭忠,翟仲毅,钱俊彦,郭云川.基于关键迹和ASP的CSP模型检测.软件学报,2015,26(10):2521-2544

Copy
Share
Article Metrics
  • Abstract:3665
  • PDF: 5646
  • HTML: 1564
  • Cited by: 0
History
  • Received:September 10,2013
  • Revised:September 29,2014
  • Online: October 10,2015
You are the first2032465Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063