Show simple item record

dc.contributor.authorWebster, Matt
dc.contributor.authorDixon, Clare
dc.contributor.authorFisher, Michael
dc.contributor.authorSalem, Maha
dc.contributor.authorSaunders, Joe
dc.contributor.authorKoay, Kheng Lee
dc.contributor.authorDautenhahn, K.
dc.contributor.authorSaez-Pons, Joan
dc.date.accessioned2017-07-13T16:58:13Z
dc.date.available2017-07-13T16:58:13Z
dc.date.issued2016-04-02
dc.identifier.citationWebster , M , Dixon , C , Fisher , M , Salem , M , Saunders , J , Koay , K L , Dautenhahn , K & Saez-Pons , J 2016 , ' Toward Reliable Autonomous Robotic Assistants Through Formal Verification : A Case Study ' , IEEE Transactions on Human-Machine Systems , vol. 46 , no. 2 , pp. 186-196 . https://doi.org/10.1109/THMS.2015.2425139
dc.identifier.issn2168-2305
dc.identifier.otherPURE: 8650184
dc.identifier.otherPURE UUID: 1c9a8c26-4291-4527-87cb-65cbf0b82118
dc.identifier.otherScopus: 84929208278
dc.identifier.urihttp://hdl.handle.net/2299/18912
dc.descriptionThis is an Open Access article distributed in accordance with the terms of the Creative Commons Attribution (CC BY 3.0) license, which permits others to copy, distribute, remix, adapt and build upon this work, for commercial use, provided the original work is properly cited. See: https://creativecommons.org/licenses/by/3.0/
dc.description.abstractIt 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.en
dc.format.extent11
dc.language.isoeng
dc.relation.ispartofIEEE Transactions on Human-Machine Systems
dc.subjectArtificial Intelligence
dc.subjectSignal Processing
dc.subjectHuman Factors and Ergonomics
dc.subjectComputer Networks and Communications
dc.subjectComputer Science Applications
dc.subjectHuman-Computer Interaction
dc.subjectControl and Systems Engineering
dc.titleToward Reliable Autonomous Robotic Assistants Through Formal Verification : A Case Studyen
dc.contributor.institutionSchool of Computer Science
dc.contributor.institutionAdaptive Systems
dc.contributor.institutionCentre for Computer Science and Informatics Research
dc.description.statusPeer reviewed
rioxxterms.versionVoR
rioxxterms.versionofrecordhttps://doi.org/10.1109/THMS.2015.2425139
rioxxterms.typeJournal Article/Review
herts.preservation.rarelyaccessedtrue


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record