IEICE TRANSACTIONS on Information
Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots
Summary :
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).
- Publication
- IEICE TRANSACTIONS on Information Vol.E104-D No.10 pp.1515-1532
- Publication Date
- 2021/10/01
- Publicized
- 2021/07/08
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2020FOP0002
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approaches)
- Category
Authors
Yoshinao ISOBE
National Institute of Advanced Industrial Science and Technology
Nobuhiko MIYAMOTO
National Institute of Advanced Industrial Science and Technology
Noriaki ANDO
National Institute of Advanced Industrial Science and Technology
Yutaka OIWA
National Institute of Advanced Industrial Science and Technology
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Yoshinao ISOBE, Nobuhiko MIYAMOTO, Noriaki ANDO, Yutaka OIWA, "Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots" in IEICE TRANSACTIONS on Information,
vol. E104-D, no. 10, pp. 1515-1532, October 2021, doi: 10.1587/transinf.2020FOP0002.
Abstract: 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).
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2020FOP0002/_p
Copy
@ARTICLE{e104-d_10_1515,
author={Yoshinao ISOBE, Nobuhiko MIYAMOTO, Noriaki ANDO, Yutaka OIWA, },
journal={IEICE TRANSACTIONS on Information},
title={Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots},
year={2021},
volume={E104-D},
number={10},
pages={1515-1532},
abstract={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).},
keywords={},
doi={10.1587/transinf.2020FOP0002},
ISSN={1745-1361},
month={October},}
Copy
TY - JOUR
TI - Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots
T2 - IEICE TRANSACTIONS on Information
SP - 1515
EP - 1532
AU - Yoshinao ISOBE
AU - Nobuhiko MIYAMOTO
AU - Noriaki ANDO
AU - Yutaka OIWA
PY - 2021
DO - 10.1587/transinf.2020FOP0002
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E104-D
IS - 10
JA - IEICE TRANSACTIONS on Information
Y1 - October 2021
AB - 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).
ER -
English
