Towards Compositional Verification for Modular Robotic Systems

Rafael Cardoso, Louise Dennis, Marie Farrell, Michael Fisher, Matt Luckcuck

Research output: Contribution to conferencePaperpeer-review


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.
Original languageEnglish
Publication statusPublished - 2020
EventSecond International Workshop on Formal Methods for Autonomous Systems -
Duration: 7 Dec 2020 → …


WorkshopSecond International Workshop on Formal Methods for Autonomous Systems
Abbreviated titleFMAS 2020
Period7/12/20 → …
Internet address


Dive into the research topics of 'Towards Compositional Verification for Modular Robotic Systems'. Together they form a unique fingerprint.

Cite this