计算机科学 ›› 2015, Vol. 42 ›› Issue (10): 244-250.
刘彦青,赵岭忠,钱俊彦
LIU Yan-qing, ZHAO Ling-zhong and QIAN Jun-yan
摘要: 通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。
[1] Hoare C A R.Communicating Sequential Processes [M].Prentice Hall International,2004:45-108 [2] 袁崇义.Petri网应用[M].北京:科学出版社,2013:31-55Yuan Chong-yi.The Application of Petri Nets [M].Beijing:Science Press,2013:31-55 [3] 蒋昌俊.Petri网的行为理论及其应用[M].北京:高等教育出版社,2003:8-9 Jiang Chang-jun.The Behavior Theory of Petri Nets and its Application [M].Beijing:Higher Education Press,2003:8-9 [4] Girault C,Valk R.系统工程Petri网—建模、验证与应用指南[M].王生原,余鹏,霍金健,译.北京:电子工业出版社,2005:60-130 [5] Cindio F,Michelis G,Pomello L,et al.A Petri net model of CSP[C]∥Proceedings of Convención Informática Latina (CIL’81).Barcelona,1981:392-406 [6] Goltz U,Reisig W.CSP-programs as nets with individual tokens [M]∥Advances in Petri Nets 1984.Springer,1985:169-196 [7] Mazzeo A,Mazzocca N,Russo S,et al.Formal specification of concurrent systems:a structured approach [J].The Computer Journal,1998,1(3):145-162 [8] Mazzeo A,Mazzocca N,Russo S,et al.A Systematic Approach to the Petri Net Based Specification of Concurrent Systems[C]∥Proceedings of the Safety-Critical Real-Time Systems.Napoli,Italy,1997:3-20 [9] Mazzocca N,Russo S,Vittorini V.Integrating trace logic andPetri nets specifications [C]∥ Proceedings of the 30th Hawaii International Conference on System Sciences:Software Techno-logy and Architecture.1997:443-451 [10] Llorens M,Oliver J,Silva J,et al.Transforming communicating sequential processes to Petri nets[C]∥Proceedings of the 7th International Conference on Engineering Computational Technology(ECT 2010).Val-encia,Spain,2010:1-16 [11] Llorens M,Oliver J,Silva J,et al.Generating a Petri net from a CSP specification:A semantics-based method[J].Advances in Engineering Software,2012,0(1):110-130 [12] Baldan P,Bonchi F,Gadducci F.Encoding Asynchronous Interactions Using Open Petri Nets[C]∥Proceedings of the 20th International Conference,CONCUR 2009.Bologna,Italy,2009:99-114 [13] Baldan P,Bonchi F,Gadducci F.Encoding Synchronous Interactions Using Labelled Petri Nets[C]∥Proceedings of the 16th IFIP WG 6.1 International Conference,COORDINATION 2014.Berlin,Germany,2014:1-16 [14] Magott J.Performance evaluation of communicating sequential processes(CSP) using Petri nets[J].IEE Proceedings E:Computers and Digital Techniques,1992,9(3):237-241 [15] Sheldon F T,Kavi K M,Ka-mangar F A.Reliability Analysis of CSP Specifications:a New Method Using Petri Nets[C]∥Proceedings of the AIAA Computing in Aerospace Conference.USA,1995:317-326 [16] Berthomieu B,Ribet P O,Vernadat F.The tool TINA——Construction of Abstract State Spaces for Petri Nets and Time Petri Nets[J].International Journal of Production Research,2004,2(14):2741-2756 [17] Berthomieu B,Vernadat F.Time Petri Nets Analysis with TINA[C]∥Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QEST 2006).Riverside,CA,2006:123-124 [18] Louazani A,Sekhri L,Kechar B.A time Petri net model forwormhole attack detection in wireless sensor networks[C]∥Proceedings of the 2013 International Conference on Smart Communications in Network Technologies (SaCoNeT).Paris,France,2013:1-6 [19] Adjir N,de Saqui-Sannes P,Rahmouni K M.Conformance Testing of Preemptive Real-Time Systems[J].International Journal of Embedded and Real-Time Communication Systems,2013,4(4):1-26 [20] Liu Y,Sun J,Dong J S.Pat 3:An extensible architecture for building multi-domain model checkers[C]∥2011 IEEE 22nd International Symposium on Proceedings of the Software Reliabi-lity Engineering (ISSRE).Hiroshima,Japan,2011:190-199 |
No related articles found! |
|