Integration of robotics components and verification using petri net

被引:0
|
作者
Srivastava, Ratnesh Prasad [1 ]
Nandi, G. C. [2 ]
机构
[1] GBPUA&T, Coll Technol, Informat Technol, Pantnagar, Uttar Pradesh, India
[2] Indian Inst Informat Technol, Informat Technol, Allahabad, Uttar Pradesh, India
来源
2017 INTERNATIONAL CONFERENCE ON INNOVATIONS IN CONTROL, COMMUNICATION AND INFORMATION SYSTEMS (ICICCI-2017) | 2017年
关键词
SOA; CCU; DCU; BCU; Interface; Petri Net; Siphon; Deadlock; Concurrency component;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We advocate developing new components by using already developed components thus reduces time and effort of development. The issues of concurrency, compatibility, correctness, coordination arises during component composition while using synchronous or asynchronous communication. We were motivated with MARIE[17] an integration effort which has shortcomings of tight coupling and multithreaded request/response architecture produces non deterministic behavior of execution. We selected components Player/Stage [18] (A network server for robotics), Wall Follower Service, Wanderer available in field of robotics and tried to verify the component composition before developing an integration platform. For verification purpose we decided to use model checking instead of theorem proving. We used Petri net [19], a language of concurrent system and petri net tool PIPE for preparing the model of composition. Since the components communicate using their interfaces so we established theory of interface, component and their interface composition. Finally we came to a conclusion based on the composed petri net model that issues of deadlock can only be removed by using implicit synchronization in a concurrent system.
引用
收藏
页码:80 / 86
页数:7
相关论文
共 50 条
  • [31] Compositional verification of concurrent systems using Petri-net-based condensation rules
    Univ of Illinois at Chicago, Chicago, United States
    ACM Trans Program Lang Syst, 5 (917-979):
  • [32] Verification of the safety communication protocol in train control system using colored Petri net
    Chen Lijie
    Tang Tao
    Zhao Xianqiong
    Schnieder, Eckehard
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 2012, 100 : 8 - 18
  • [33] Verification and Validation of a Neural-Symbolic Hybrid System Using an Enhanced Petri Net
    Rodriguez Jorge, Ricardo
    Reyes Salgado, Gerardo
    Cruz Sanchez, Vianey Guadalupe
    PROCEEDINGS OF THE SEVENTH IEEE INTERNATIONAL CONFERENCE ON COGNITIVE INFORMATICS, 2008, : 160 - 167
  • [34] Compositional verification of concurrent systems using Petri-net-based condensation rules
    Juan, EYT
    Tsai, JJP
    Murata, T
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (05): : 917 - 979
  • [35] A compositional partial order semantics for Petri net components
    Kindler, E
    APPLICATION AND THEORY OF PETRI NETS 1997, 1997, 1248 : 235 - 252
  • [36] Verification and Analysis of Access Control Policy with Colored Petri Net
    Feng, Fujun
    Li, Junshan
    PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMMUNICATION SOFTWARE AND NETWORKS, 2009, : 610 - 614
  • [37] Decidability of opacity verification problems in labeled Petri net systems
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    AUTOMATICA, 2017, 80 : 48 - 53
  • [38] On the design and temporal Petri net verification of grid commerce architecture
    Yuyue, Du
    Changjun, Jiang
    CHINESE JOURNAL OF ELECTRONICS, 2008, 17 (02): : 247 - 251
  • [39] Hierarchical verification for web service composition based on petri net
    Wang, L.
    Wang, Z. G.
    BASIC & CLINICAL PHARMACOLOGY & TOXICOLOGY, 2018, 123 : 36 - 37
  • [40] On the design and temporal petri net verification of grid commerce architecture
    College of Information Science and Engineering, Shandong University of Science and Technology, Qingdao 266510, China
    不详
    不详
    Chin J Electron, 2008, 2 (247-251):