计算机科学 ›› 2015, Vol. 42 ›› Issue (10): 244-250.

• 人工智能 • 上一篇    下一篇

基于Petri网的CSP并发系统验证技术研究

刘彦青,赵岭忠,钱俊彦   

  1. 桂林电子科技大学计算机科学与工程学院 桂林541004,桂林电子科技大学计算机科学与工程学院 桂林541004,桂林电子科技大学计算机科学与工程学院 桂林541004
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基金(61262008,61100186),广西自然科学基金(2013GXNSFBA019267),广西教育厅重点项目:高可信软件的安全性验证研究,广西高等学校高水平创新团队及卓越学者计划,广西可信软件重点实验室基金项目(kx201113),桂林电子科技大学创新团队资助

Verification of Concurrent CSP Systems Based on Petri Net

LIU Yan-qing, ZHAO Ling-zhong and QIAN Jun-yan   

  • Online:2018-11-14 Published:2018-11-14

摘要: 通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。

关键词: 通信顺序进程(CSP),并发系统,Petri网,性质验证,安全性

Abstract: Communicating sequential processes (CSP) and Petri net are two important formal methods for analyzing concurrent systems.The CSP language features high level abstraction which is useful to effectively describe the interactions between concurrent processes,but it has weaknesses in the description and analysis of the physical structure of systems.Petri net is a tool for modeling and analyzing concurrent systems in a formal and graphical form,focusing on the physical description of system structure and properties analysis.This paper combined the advantages of both CSP and Petri net.At first,we used CSP to describe concurrent systems and then translated them into Petri net to analyze the dynamic behavior of the system.Finally,we used the model checking tool TINA to analyze and verify the system properties.It is shown that the safety property of CSP processes cannot be verified with existing properties analysis tools like PAT,however,it can be analyzed when the CSP description is transformed into Petri net.This transformation effectively expands the scope of verifiable properties of concurrent systems described by CSP.

Key words: Communicating sequential processes (CSP),Concurrent systems,Petri net,Property verification,Safety

[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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!