Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study

被引：44

作者：

Webster, Matt ^{[1
]}

Dixon, Clare ^{[1
]}

Fisher, Michael ^{[1
]}

Salem, Maha ^{[2
]}

Saunders, Joe ^{[2
]}

Koay, Kheng Lee ^{[2
]}

Dautenhahn, Kerstin ^{[2
]}

Saez-Pons, Joan ^{[2
]}

机构：

[1] Univ Liverpool, Dept Comp Sci, Liverpool L69 3BX, Merseyside, England

[2] Univ Hertfordshire, Sch Comp Sci, Hatfield AL10 9AB, Herts, England

来源：

IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS | 2016年 / 46卷 / 02期

基金：

英国工程与自然科学研究理事会;

关键词：

Autonomous systems; formal verification; human-robot teams; model checking; robotics;

D O I：

10.1109/THMS.2015.2425139

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

It is essential for robots working in close proximity to people to be both safe and trustworthy. We present a case study on formal verification for a high-level planner/scheduler for the Care-O-bot, an autonomous personal robotic assistant. We describe how a model of the Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by automatically translating this model to the input language of an existing model checker. Four sample properties based on system requirements were verified. We then refined the environment model three times to increase its accuracy and the persuasiveness of the formal verification results. The first refinement uses a user activity log based on real-life experiments, but is deterministic. The second refinement uses the activities from the user activity log nondeterministically. The third refinement uses "conjoined activities" based on an observation that many user activities can overlap. The four samples properties were verified for each refinement of the environment model. Finally, we discuss the approach of environment model refinement with respect to this case study.

引用

页码：186 / 196

页数：11

共 18 条

[1]

Acquisti A., 2011, BRAHMS TUTORIAL TM01

[2]

Clancey W. J., 2002, P HUM ROB INT AAAI F

[3]

Clarke EM, 1999, MODEL CHECKING, P1

[4]

Cowley A., 2011, 2011 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2011), P4776, DOI 10.1109/IROS.2011.6048677

[5]

Duque I., 2013, PROC 6 INT C ADV COM, P141

[6]

Fisher M., 2011, An Introduction to Practical Formal Methods Using Temporal Logic

[7]

Holzmann G., 2013, INSPIRING APPL SPIN

[8]

Holzmann G. J., 2003, The SPIN Model Checker: Primer and Reference Manual

[9]

Kouskoulas Y., Belta and Ivancic, V137, P263, DOI [10.1145/2461328.2461369, DOI 10.1145/2461328.2461369]

[10]

Mohammed A, 2010, MULTIROBOT SYSTEMS M, V01, DOI [10.5772/7349, DOI 10.5772/7349]

← 1 2 →