计算机科学 ›› 2013, Vol. 40 ›› Issue (11): 181-186.
赵岭忠,翟仲毅,钱俊彦
ZHAO Ling-zhong,ZHAI Zhong-yi and QIAN Jun-yan
摘要： CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂；性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。
| [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,Syrjnen 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! |
|
||
首页