We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

Title: Towards Compositional Verification for Modular Robotic Systems

Authors: Rafael C. Cardoso (The University of Manchester), Louise A. Dennis (The University of Manchester), Marie Farrell (The University of Manchester), Michael Fisher (The University of Manchester), Matt Luckcuck (The University of Manchester)
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.
Comments: In Proceedings FMAS 2020, arXiv:2012.01176
Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO); Robotics (cs.RO)
Journal reference: EPTCS 329, 2020, pp. 15-22
DOI: 10.4204/EPTCS.329.2
Cite as: arXiv:2012.01648 [cs.SE]
  (or arXiv:2012.01648v1 [cs.SE] for this version)

Submission history

From: EPTCS [view email]
[v1] Thu, 3 Dec 2020 02:21:51 GMT (27kb)

Link back to: arXiv, form interface, contact.