Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots

被引：1
|
作者：
Isobe, Yoshinao [1 ]
Miyamoto, Nobuhiko [1 ]
Ando, Noriaki [1 ]
Oiwa, Yutaka [1 ]
机构：
[1] Natl Inst Adv Ind Sci & Technol, Ikeda, Osaka 5638577, Japan
来源：
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS | 2021年 / E104D卷 / 10期
关键词：
formal approach; concurrent finite state machines; process algebra; model check; cooperative robots; robotic technology middleware;
D O I：
10.1587/transinf.2020FOP0002
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper, we demonstrate that a formal approach is effective for improving reliability of cooperative robot designs, where the control logics are expressed in concurrent FSMs (Finite State Machines), especially in accordance with the standard FSM4RTC (FSM for Robotic Technology Components), by a case study of cooperative transport robots. In the case study, FSMs are modeled in the formal specification language CSP (Communicating Sequential Processes) and checked by the model-checking tool FDR, where we show techniques for modeling and verification of cooperative robots implemented with the help of the RTM (Robotic Technology Middleware).
引用
收藏
页码：1515 / 1532
页数：18
相关论文
共 50 条
  • [1] Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification
    Inès Mouakher
    Fatma Dhaou
    J. Christian Attiogbé
    Journal of Computer Science and Technology, 2022, 37 : 4 - 28
  • [2] Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification
    Mouakher, Ines
    Dhaou, Fatma
    Attiogbe, J. Christian
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2022, 37 (01) : 4 - 28
  • [3] Formal construction and verification of home service robots: A case study
    Kim, M
    Kang, KC
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 429 - 443
  • [4] Modeling, analysis and testing of safety issues an event-based approach and case study
    Belli, Fevzi
    Hollmann, Axel
    Nissanke, Nimal
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, PROCEEDINGS, 2007, 4680 : 276 - +
  • [5] Fall Detection with Event-Based Data: A Case Study
    Wang, Xueyi
    Risi, Nicoletta
    Talavera, Estefania
    Chicca, Elisabetta
    Karastoyanova, Dimka
    Azzopardi, George
    COMPUTER ANALYSIS OF IMAGES AND PATTERNS, CAIP 2023, PT II, 2023, 14185 : 33 - 42
  • [6] EVENT-BASED PERFORMANCE PERTURBATION - A CASE-STUDY
    MALONY, AD
    SIGPLAN NOTICES, 1991, 26 (07): : 201 - 212
  • [7] Research on Event-B based formal modeling and verification of automatic production line
    Fu, Kaiming
    Fang, Bin
    Li, Yafen
    Li, Huijie
    PROCEEDINGS OF THE 28TH CHINESE CONTROL AND DECISION CONFERENCE (2016 CCDC), 2016, : 3690 - 3695
  • [8] Formal development method of control systems using the event-based B approach - Case study: A parcel sorting device
    Mosbahi, Olfa
    Jaray, Jacques
    Jemni Ben Ayed, Leila
    2006 IEEE INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS, VOLS 1-3, 2006, : 833 - +
  • [9] Stepwise Formal Modeling and Verification of Self-Adaptive systems with Event-B. The Automatic Rover Protection case study
    Singh, Neeraj Kumar
    Ait-Ameur, Yamine
    Pantel, Marc
    Dieumegard, Arnaud
    Jenn, Eric
    2016 21ST INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2016), 2016, : 43 - 52
  • [10] Dissemination of information in event-based surveillance, a case study of Avian Influenza
    Valentin, Sarah
    Boudoua, Bahdja
    Sewalk, Kara
    Arinik, Nejat
    Roche, Mathieu
    Lancelot, Renaud
    Arsevska, Elena
    PLOS ONE, 2023, 18 (09):
12345