Tools
Tools
Webster, M, Dixon, C, Fisher, M, Salem, M, Saunders, J, Koay, KL, Dautenhahn, K and Saez-Pons, J (2015) Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study. IEEE Transactions on Human-Machine Systems, 46 (2). pp. 186-196. ISSN 2168-2291
|
Text
Toward Reliable Autonomous Robotic Assistants Through Formal Verification A Case Study.pdf - Published Version Available under License Creative Commons Attribution. Download (553kB) | Preview |
Abstract
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.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | Science & Technology; Technology; Computer Science, Artificial Intelligence; Computer Science, Cybernetics; Computer Science; Autonomous systems; formal verification; human-robot teams; model checking; robotics |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science Q Science > QA Mathematics > QA76 Computer software |
| Divisions: | Computer Science & Mathematics |
| Publisher: | IEEE |
| Related URLs: | |
| Date Deposited: | 21 Apr 2021 08:26 |
| Last Modified: | 04 Sep 2021 06:14 |
| DOI or ID number: | 10.1109/THMS.2015.2425139 |
| URI: | https://researchonline.ljmu.ac.uk/id/eprint/14161 |
 |
View Item |