Towards Compositional Verification for Modular Robotic Systems

Cardoso, Rafael C ORCID: 0000-0001-6666-6954, Dennis, Louise A ORCID: 0000-0003-1426-1896, Farrell, Marie ORCID: 0000-0001-7708-3877, Fisher, Michael and Luckcuck, Matt ORCID: 0000-0002-6444-9312 (2020) Towards Compositional Verification for Modular Robotic Systems. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 329 (329). pp. 15-22.

Access the full-text of this item by clicking on the Open Access link.

Text
2012.01648v1.pdf - Submitted version
Download (138kB) | Preview

Official URL: http://dx.doi.org/10.4204/EPTCS.329.2

Abstract

Software engineering of modular robotic systems is a challenging task, however, verifying that the developed components all behave as they should individually and as a whole presents its own unique set of challenges. In particular, distinct components in a modular robotic system often require different verification techniques to ensure that they behave as expected. Ensuring whole system consistency when individual components are verified using a variety of techniques and formalisms is difficult. This paper discusses how to use compositional verification to integrate the various verification techniques that are applied to modular robotic software, using a First-Order Logic (FOL) contract that captures each component's assumptions and guarantees. These contracts can then be used to guide the verification of the individual components, be it by testing or the use of a formal method. We provide an illustrative example of an autonomous robot used in remote inspection. We also discuss a way of defining confidence for the verification associated with each component.

Item Type:	Article
Additional Information:	In Proceedings FMAS 2020, arXiv:2012.01176
Uncontrolled Keywords:	cs.SE, cs.SE, cs.LO, cs.RO
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	16 Aug 2021 14:05
Last Modified:	20 Sep 2023 22:12
DOI:	10.4204/EPTCS.329.2
Open Access URL:	http://eptcs.web.cse.unsw.edu.au/paper.cgi?FMAS202...
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3115859