# A Compositional Approach
to
Verifying Modular Robotic Systems

Matt Luckcuck This work is supported by UK Research and Innovation, and EPSRC
Hubs for Robotics and AI in Hazardous Environments: EP/R026092 (FAIR-SPACE),
EP/R026173 (ORCA), and EP/R026084 (RAIN); and through grant EP/V026801 (TAS
Verifiability Node). Cardoso’s and Fisher’s work is supported by the Royal
Academy of Engineering under the Chairs in Emerging Technologies scheme. Some
of Luckcuck’s work was performed while employed by Maynooth University,
Ireland. For the purpose of open access, the authors have applied a Creative
Commons Attribution (CC BY) licence to any Author Accepted Manuscript version
arising. The formal models, data, and source code supporting the findings
reported in this paper are openly available from the Zenodo repository at:
https://doi.org/10.5281/zenodo.6941344. School of Computer Science, University
of Nottingham, United Kingdom  0000-0002-6444-9312 Marie Farrell  Department
of Computer Science, University of Manchester, United Kingdom
0000-0001-7708-3877 Angelo Ferrando  Department of Computer Science,
University of Genova, Italy  0000-0002-8711-4670 Rafael C. Cardoso  Department
of Computing Science, University of Aberdeen, United Kingdom
0000-0001-6666-6954 Louise A. Dennis  Department of Computer Science,
University of Manchester, United Kingdom  0000-0003-1426-1896 Michael Fisher
Department of Computer Science, University of Manchester, United Kingdom
0000-0002-0875-3862

###### Abstract

Robotic systems used in safety-critical scenarios often rely on modular
software architectures, and increasingly include autonomous components.
Verifying that these modular robotic systems behave as expected requires
approaches that can cope with, and preferably take advantage of, this inherent
modularity. This paper describes a compositional approach to specifying the
nodes in robotic systems built using the Robot Operating System (ROS), where
each node is specified using First-Order Logic (FOL) assume-guarantee
contracts that link the specification to the ROS implementation. We introduce
inference rules that facilitate the composition of these node-level contracts
to derive system-level properties. We also present a novel Domain-Specific
Language, the ROS Contract Language (RCL), which captures a node’s FOL
specification and links this contract to its implementation. RCL contracts can
be automatically translated, by our tool Vanda, into executable monitors;
which we use to verify the contracts at runtime. We illustrate our approach
through the specification and verification of an autonomous rover engaged in
the remote inspection of a nuclear site, and finish with smaller examples that
illustrate other useful features of our framework.

##  1 Introduction

Robotic systems are increasingly deployed in industrial, often safety-
critical, scenarios such as monitoring offshore structures [1], nuclear
inspection and decommissioning [2, 3], and space exploration [4, 5].
Engineering the software to control a robotic system is a complex task, often
supported by modular software frameworks, such as the Robot Operating System
(ROS) [6] or GenoM [7, 8]. It is crucial to ensure that the software
controlling a robot behaves correctly, particularly as modern robotic systems
become more autonomous, more complex, and are used in dynamic environments
that they share with humans. The generality and flexibility of robotic
software frameworks also means that guaranteeing their correct behaviour is
challenging [9].

The state-of-the-art for verification of autonomous and robotic systems
includes a variety of formal methods that can be used for specification and
verification [10] – non-formal methods such as field tests and simulation-
based testing are also common. Formal methods that we see being used include:
model-checking [11], which exhaustively explores the state space to establish
that a property holds; runtime verification [12], which monitors system
behaviour at runtime; and theorem-provers [13], demonstrating by mathematical
proof that the system behaves correctly. Different components of a robotic
system may be better suited to different verification techniques, but linking
the outputs of multiple techniques remains a challenge. Previously, we have
argued that robotics is a domain in which integrating (formal and non-formal)
verification methods is both a necessity to be dealt with and an opportunity
to be grasped [14].

_Assume-Guarantee_ reasoning [15] (or the specification of _pre-_ and _post-_
conditions) is a well established compositional verification technique. A pair
of pre- and post-conditions form a contract [16]. Specifying a system using
Assume-Guarantee or _pre-_ and _post-_ conditions enables it to be decomposed
into modules, so that each module can be verified separately against its
associated contract. However, care must be taken when specifying the
contracts, because they still require validation against the actual
requirements of the system.

This paper presents our approach to verifying robotic systems that are
developed using ROS. This particular robotic software framework was chosen
because of its prevalence in the literature. A ROS system is composed of nodes
that communicate using message passing via buffered communication channels.
The nodes coordinate to control the robot’s overall behaviour. Typically, each
node will be specialised to perform a different function, with different nodes
(or collections of nodes) often requiring distinct verification techniques.
For example, machine learning components will likely be verified via testing,
whereas a planner might be mathematically modelled and reasoned about using
formal verification. Our approach uses the encapsulation provided by ROS nodes
to provide compositionality. Fundamentally, we address the research question:

> Can we use a compositional and heterogeneous approach to verify ROS-based
> systems?

Our approach begins by (manually) abstracting the graph of nodes in the ROS
program (generated by ROS Graph or similar) into a more manageable model of
the system, a model that focusses on the system’s most critical components.
Although some nodes maintain a one-to-one correspondence with the ROS
software, abstraction can involve dropping some nodes from the system model or
combining related nodes into, what we call, a compound node.

Once the ROS software is abstracted to a manageable system model, we specify
each of the nodes in this model using Assume-Guarantee contracts, written in
our contract specification language that is based on First-Order Logic (FOL).
FOL was chosen for contract specifications because it is both expressive and
widely understood, flattening our approach’s learning curve.

We also provide a calculus that can be used to combine the module contracts
and to derive system-level properties that correspond to the system’s
requirements. The calculus uses temporal operators from First-Order Temporal
Logic (FOTL) [17] to represent the connections between the contracts.

Once the contracts are verified against the system’s requirements, we can take
two further steps in parallel. The contracts are used to guide the
verification of each node, using heterogeneous (formal or non-formal)
verification approaches chosen to suit each node. Providing a formal link
between FOL and every verification approach is no in scope for this paper.
Using the contracts as a guide enables the use of formal and informal links
between the contracts and verification. We leave the verifiers to choose the
most suitable verification method for each nodes, because they are best placed
o make this choice. Meanwhile, our tool, Vanda, automatically synthesises
runtime monitors from the contracts. The overall approach builds on two pieces
of previous work:

  * •

the initial presentation of the contract calculus in [18], which we
significantly update in this paper; and,

  * •

our application of heterogeneous verification approaches to a simulation of
the Mars Curiosity rover [19], which we also update with additional steps.

Our work provides four contributions:

  1. 1.

A compositional approach to specifying the pre- and post-conditions of robotic
systems constructed using ROS, which is supported by;

  2. 2.

a Domain Specific Language (DSL), called the ROS Contract Language (RCL), that
links a contract to the ROS implementation;

  3. 3.

a calculus containing inference rules for combining the contracts so that we
can derive system-level (safety and mission) properties; and,

  4. 4.

a tool-chain that synthesises runtime monitors from the system’s RCL
contracts.

Our approach enables the introduction of a formal specification to an existing
ROS system. As such, we use the intended behaviour of the nodes in a system as
the starting point for specifying its contracts, and combine them using the
calculus. Our DSL and prototype parsing and monitor-generation tool (Vanda)
support users in writing grammatically correct contracts.

In summary, the contracts: are structured using RCL; are reasoned about using
our calculus; guide the heterogeneous verification of the nodes; and are then
used to generate runtime monitors that provide a safety net, ensuring that the
contracts have been verified correctly and the system is obeying its
requirements. We validate our approach by applying it to a rover robot
performing a remote inspection task inside a nuclear storage facility (§4).
This example system was developed independently of our work, and we use our
approach to introduce contracts and formal verification. We also describe the
specification and verification of individual nodes, showing how our approach
can guide verification using a variety of different formalisms.

The remainder of this paper is structured as follows. In §2, we discuss
related work. §3 describes our compositional approach to verifying modular
robotic systems using FOL contracts, including: the calculus for combining
node specifications, a description of how RCL supports contract specification,
and the automatic synthesis of runtime monitors from RCL. §4 presents the
specification and verification of our Case Study, a remote inspection rover.
In §5 we discuss some interesting characteristics of our framework, such as
the use of a system’s modularity, how our approach fits into the robotic
software development process and, in §5.3, we describe how our approach can be
applied to non-ROS systems. Finally, §6 concludes the paper and presents
avenues for future work.

##  2 Related Work

This section discusses approaches in the literature that are related to our
work. We have grouped these into Compositional Verification and Reliable
Software Engineering (§2.1) and Robotics (§2.2). Some of the cited work could
fit into both of these categories, we added them to the most relevant category
based on their main contributions and publication venue.

###  2.1 Compositional Verification and Reliable Software Engineering

Our approach encourages the development of systems as a composition of sub-
systems, as does the work on the Pacti [20] tool for assume-guarantee
contracts. In Pacti, constraints are expressed as linear inequalities and
refinement is used to reason about the relationship between contracts. In
contrast to the language used by Pacti, we use FOL which is more expressive
and actually capable of expressing Pacti contracts.

Compositional verification is applied to the SIENA event-notification
middleware [21] where a global system property is decomposed into local
properties that only hold on sub-parts of the system. They use compositional
model-checking and the system models (labelled transition systems) are
translated to Promela, using SPIN for verification. The various properties are
related using simulation, a notion that in [21] seems similar to formal
refinement. Our work provides a broader approach; we are not restricted to
model-checking and we enable heterogeneous verification. That said, their way
of relating global and sub-properties is interesting and will likely inspire
future directions for our work.

Compositional Assume-Guarantee reasoning has been used to define contracts for
system modules [22], with rule-defined contract composition. Their rules share
the same aim as our work, but our inference rules (§3) are simpler because we
make assumptions about the robotic system being modelled, making our contracts
easier to mechanise as runtime monitors. Their rules are extended by [23],
using a variant of Signal Temporal Logic (STL) to describe behaviour and
contracts. They used the rules in [22] to produce whole system assumptions and
guarantees. They target closed-loop control systems, whereas our approach
targets robotic systems that are written in general-purpose programming
languages. Related compositional approaches include OCRA [24] and AGREE [25],
though neither explicitly incorporates heterogeneous verification.

CoCoSpec [26] is a language that provides assume/guarantee contracts for
reactive systems. CoCoSpec extends the Lustre specification language and uses
the Kind2 model-checker for compositional verification [27]. This approach is
specialised for synchronous communications, which differ from the event-based
communications that we target, and their contract semantics is more
restrictive than ours. Further, it is not clear how their support for
compositional verification can be extended to support heterogeneous components
such as those in our example. In our previous work, an inspection rover
example combined NASA’s Formal Requirements Elicitation Tool (FRET), CoCoSpec,
and Event-B for verification [28]. This work used a Simulink model of the
robot’s architecture to define individual components. In contrast, our work
focusses on systems developed in ROS and use FOL contracts to reason about
system-level properties.

We take inspiration from Broy’s approach to systems engineering [29] which
presents three kinds of artefacts: (1) system-level requirements, (2)
functional system specification, and (3) logical subsystem architecture. These
are represented as logical predicates in the form of assertions, with
relationships defined between them that extend to assume/commitment contracts.
The treatment of these contracts is purely logical, and we present a similar
technique that, instead of assertions, uses Assume-Guarantee contracts and is
specialised to the software engineering of robotic systems.

The Integration Property Language (IPL) [30] is designed to improve
expressiveness in the verification of integrated heterogeneous models in
cyber-physical systems. IPL combines FOL reasoning across architectural views
that correspond to behaviourless component models, annotated with types and
properties. IPL provides modular verification of properties that come from
different models and static, system-wide reasoning using Satisfiability Modulo
Theories (SMT) solvers and model checkers. They focus on verifying the result
of the integration, rather than individually verifying each model and then
generating system-level properties. The latter approach is more appropriate
for robotic systems, since integration will often result in poor scalability.

Publish-subscribe architectures, like ROS, are popular in many domains. Recent
work presents the Loupe model-checker for publish-subscribe architectures
[31]. They essentially embed the communications infrastructure within the
verification checker to reduce the state space for verification. Such
approaches are certainly relevant for our work, but, they do not explicitly
focus on ROS or support a compositional approach to verification of individual
system modules.

###  2.2 Robotics

Many approaches for building safe robotic systems focus on ROS, which is a
well established middleware that supports interoperability and modularity in
the development of robotic software. A safety-critical working
group111https://github.com/ros-safety Accessed: 03/11/2023 for ROS 2 have been
developing tools, libraries, and documentation to support the safe engineering
of safety-critical ROS systems. For example, they provide a _contracts_
package222https://github.com/ros-safety/contracts_lite Accessed: 03/17/2023,
where a contract is a combination of pre-/post-conditions and assertions over
the implementation of C++ functions. The advantage of this approach is that
the contracts work directly in the implementation’s source code. However,
limiting the library to C++ is a disadvantage because ROS nodes may also be
written in Python, Java, etc. In comparison, our approach is more general and
not limited to the verification of individual functions, but also allows the
verification of the system as a whole through the use of our inference rules.
Further, their ad-hoc contract language is less expressive than FOL. An
interesting line of future work may include updating Vanda, our prototype
tool, to produce contracts compatible with the ROS2 contracts package for
applications fully implemented in C++.

A similar approach is shown in [32] for GenoM instead of ROS, which uses the
Behaviour-Interaction-Priority (BIP) framework for incremental composition of
heterogeneous components. They offer synthesis of functional-level controllers
by synchronising dependencies between controllers. They verify safety
properties and detect deadlock conditions using model checking and “observers”
(runtime monitors). Another compositional approach in [33] uses Assume-
Guarantee contracts to decompose the control software of multi-robot systems
and targets ROS. The individual components or robots are decomposed into sub-
problems and then recomposed using contracts to provide system-level
validation. Finally, the resulting synthesised controller is integrated into
ROS.

Drona [34] is a toolchain for programming safety-critical robots, with support
for ROS. Their DSL, called $P$, is based on state machines. It offers
compositional Assume-Guarantee testing and a runtime assurance system to check
that the assumptions made at design-time hold at runtime. In contrast, our DSL
is used purely to specify contracts for verification, we do not directly
interfere with the system’s implementation. Additionally, our runtime monitors
are automatically synthesised from the contracts, while theirs require
additional specification.

The Declarative Robot Safety (DeRoS) [35] is a DSL with a declarative syntax
for specifying safety-related constraints in ROS, which lowers the barrier to
using this approach – similarly to our use of a textual version of FOL. In
DeRoS, each contract is a refinement of the system-level contract; it is not
clear if they use a similar technique to our inference rules to ensure that
the contracts are composed correctly at design time. Unfortunately, DeRoS is
not publicly available, or it could have been an alternative way to synthesise
our monitors.

Another DSL, PROMISE [36], is designed to describe mission specifications for
multi-robot systems. PROMISE has been integrated in Eclipse as a plugin to
provide a graphical interface for users which allows the automatic generation
of behaviour from the mission specification, sending missions to the robots,
and runtime management of missions.

Other related work provides automatic static verification of system-wide
properties for message-passing in ROS applications [37]. The specification of
the safety properties is written in a DSL. This is then translated into FOTL
to be used in Electrum [38] which provides an automatic _Analyser_. Their
approach is embedded in HAROS [39], a framework for quality assessment of ROS
software that offers a visualisation interface for safety issues. Instead, our
work focuses on compositional verification of nodes/modules in ROS, which are
supported by inference rules to automatically generate system-wide properties.
Further, we are not limited to static verification, our approach also provides
runtime verification by synthesising monitors from the contracts.

SOTER [40] is a programming framework to support the development of robotic
systems by capturing runtime safety assurance principles. Their high-level DSL
can be used to implement reactive systems, make use of systematic testing
techniques, and support runtime assurances. The case study and experiments
presented use ROS. Our approach differs in that we are not limited to runtime
assurances, we also encourage a variety of offline verification techniques.

RoboSC is a DSL, and accompanying tool, that enables the specification of ROS
nodes as Finite-State Automata (FSA) and then synthesises supervisory
controller nodes [41]. The events in the FSA are the ROS communication topics
that trigger state changes in the automaton. The supervisory controller nodes
aim to enforce a node’s (user-described) requirements. RoboSC always adds the
overhead of communication to the ROS middleware, which increases the average
time of a controller cycle by approx. 957% (adding an average of 33.5
microseconds). Our approach can be used to enforce requirements, or to simply
observe and log deviations from the specification; the latter option avoids
some of the overheads of the additional nodes needed for Runtime Verification
(RV).

RoboChart [42] is a DSL based on the Unified Modelling Language (UML), which
supports verification and automated reasoning of robotic systems using model
checking and theorem proving. Its notation is based on state-machines, with a
restricted set of constructs. Integrated Development Environment (IDE) support
is available through an Eclipse plugin called RoboTool that automatically
generates C++ code for state machines and controllers, but does not yet offer
automatic code deployment in ROS.

As robotic systems become more complex, supporting heterogeneous verification
becomes even more important [14]. Crucially, the modular structure of ROS
systems facilitates the use of heterogeneous verification methods. For
example, recent work used various verification techniques on an autonomous
space debris removal grasping system that was developed in ROS [43]. Another
example is Antlab [44], a multi-robot task server for declarative multi-robot
programming based on ROS. Our calculus could be used to derive system-level
contracts for systems like these.

###  2.3 Summary

Many approach partially address the challenge that we tackle, and there are
various foundational approaches to compositional verification that are not
restricted to any particular domain. We take inspiration from some of these,
but devise a calculus that is specifically tailored for ROS systems. Other
approaches are limited to specific tools and so neither support nor harness
the power of incorporating a suite of heterogeneous verification approaches in
the way that our approach does. To ensure traceability and consistency, we
also provide a way of automatically generating runtime monitors so that we can
support both static and dynamic verification for systems that operate in the
real world.

##  3 Specifying Verifiable Robotic Systems

As mentioned in §1, our work enables the introduction of a formal
specification to existing ROS programs. Recall that a ROS system is composed
of nodes. Each node may subscribe to receive messages from, or publish
messages to, a topic (a buffered communication channel). Each topic is
described by the message type(s) that it can accept. ROS contains several
built-in message types such as string, bool, and int8; and custom types can
also be added.

Our verification approach begins with a manual analysis of the ROS program, to
abstract it into a more manageable system model. We then specify a contract
for each of the system’s nodes in typed FOL, which was chosen to lower the
barrier to learning to write contracts. The contracts are then combined and
reasoned about using our calculus, which uses the $\bigcirc$ (“next”) and
$\lozenge$ (“eventually”) temporal operators from FOTL. We use the contracts
to guide the modelling and verification of individual nodes, while our tool,
Vanda, automatically synthesises monitors from the contracts to provide a
safety-net that checks that their guarantees are obeyed at runtime.

Figure 1: A flowchart of the steps in our approach. The trapezium-shaped steps
are manual processes, the rectangle with rounded corners (Step 4a) is a
process that may be manual or automatic (depending on the verification tools
available), and the rectangle with right-angled corners (Step 4b) is an
automatic process. Note that Steps 4a and 4b can happen in parallel. If
needed, previous steps may be revisited.

Our approach is split into the following five steps (shown in Fig. 1):

  * Step 1:

Abstract the ROS program into a more manageable system model, containing the
nodes that are critical to the program’s correct behaviour. Depending on the
ROS program, this step may involve some form of abstraction, for example by
combining multiple nodes into a compound node, or omitting nodes that are
known to be reliable.

  * Step 2:

Write the RCL contract for each node. The contract contains the FOL _assume_
and _guarantee_ conditions, and describes the ROS topics that the node uses
(the node’s inputs and outputs). Our RCL tool, Vanda, parses the contracts,
identifying where the format of the language has not been adhered to, and can
synthesis runtime monitors (see Step 4b).

  * Step 3:

Use our calculus to reason about the combination of the node contracts. This
generates a list of system-level properties that can be used to verify the
system’s requirements. The calculus also identifies malformed contracts, which
we debug until the inference rules are valid.

  * Step 4a:

Verify the nodes, using a suite of heterogeneous verification approaches. This
step uses the contracts to guide the verification, which is especially
important where there is not a formal link between the verification approach
and FOL.

  * Step 4b:

Automatically synthesise runtime monitors for nodes from their RCL contracts.
The monitors act as a safety net to ensure that nodes adhere to their
contracts while the system is operating.

This paper focuses on ROS systems, but Steps 1 and 2 above could be applied to
a system where the nodes/modules are classes or methods. We discuss how this
might work in §5.3.

The steps are numbered sequentially, but they are not intended to be only
followed linearly; Steps 4a and 4b can also be performed in parallel.
Additionally, previous steps may be revisited, if needed. For example, as
identified above, Step 3 could highlight a malformed contract that would be
debugged and potentially rewritten, which revisits Step 2. Similarly, Step 4a
could reveal that a specification is too restrictive to be verified (for
example), which could trigger a re-write (revisiting Step 2) or the
restrictive part of the specification could be left to be monitored in Step
4b. Step 1 can also be revisited if we later find that an abstraction in the
system model is troublesome, for example we may need to split a compound node
back into its constituent parts.

It is important to note the difference in purpose between Steps 3 and 4a/4b.
In Step 3, the calculus is used to combine the contracts and reveal the
system-level property (or properties) that is produced by the combination of
their guarantees. The verification in Step 4a statically verifies that the
nodes implement their contracts, which then implies the system-level property
holds. And the monitors in Step 4b check the guarantees hold at runtime; if
all the monitors do not conclude $false$333Because our runtime monitors are
checking for violation of a property, they return $false$ when no violation is
detected., then the system-level property holds. If one monitor concludes
$false$, then we know (a) that the system-level property does not hold, and
(b) which node has violated its guarantee.

In the remainder of this section we describe: the process of abstracting a ROS
system into a system model, §3.1; how our contracts are described and
composed, §3.2; our approach to writing the contracts, §3.3; our calculus for
combining the contracts, §3.4; how the contracts can guide heterogeneous
verification, §3.5; and our runtime monitoring approach, §3.6.

###  3.1 System Model

To start writing the contracts we need a description of system’s nodes.
Because we are using ROS, we can make use of the _rqt_graph_ library444
_rqt_graph_ library: http://wiki.ros.org/rqt_graph Accessed: 03/11/2023, which
automatically generates a graph (called a ROS graph) for the system that
contains all of its nodes and the communication links between them. ROS graphs
can also display topics and actions (used to execute long-running tasks), but
using only the nodes and communication links is enough for our purposes. If
the graph is simple enough, then we can use it as the system model. However,
the graph is ofent very large, with many nodes from well-tested libraries, so
we might choose to abstract the ROS graph into a more manageable system model.

This section describes a heuristic approach to generating a more compact
system model based on the ROS graph.

  1. 1.

_Generate the ROS graph:_ use the _rqt_graph_ library to generate a graph of
the system. This can be used “as is” (skip to Step 3 in this methodology) or
can be further abstracted as detailed in the next steps.

  2. 2.

_Remove nodes:_ remove nodes that match the following conditions:

     * •

nodes from libraries that have been demonstrated to be reliable in most cases
(e.g., the _move base_ library555Move Base ROS Library:
http://wiki.ros.org/move_base Accessed: 03/11/2023 for path planning in ROS)
through community experimentation and testing;

     * •

and nodes that are simple or have no impact on the nodes or properties that
are being verified.

  3. 3.

_Combine related nodes into compound nodes:_ some nodes may be simple parts of
a larger group or sub-system. These nodes can be merged into a _compound_
node, making sure that it retains all the information needed for verification
and that it matches the implementation of the original nodes.

  4. 4.

_Add external nodes:_ some nodes may be external to ROS, such as autonomous
components (e.g., rational agents) and image processing (e.g., machine
learning), and therefore do not appear on a ROS graph. These nodes are added
to the system diagram, alongside a description of how they interact and
communicate with the other nodes.

This heuristic approach indicates how a more tractable system model can be
distilled from a complicated ROS graph. The most important aspect is that the
abstracted system model must still resemble the implementation of the ROS
nodes. We provide an example application of this heuristic in §4.1.

###  3.2 Background Concepts for the First-Order Logic Contracts

Our contracts use the standard definition of FOL with quantifiers ($\forall$,
$\exists$) and logical connectives ($\land$, $\lor$, $\lnot$, $\Rightarrow$,
$\iff$) over logical propositions including basic set theory [45]. For a given
component/node, $C$, its contract comprises
$\mathcal{A}_{C}(\overline{i_{C}})$ (assumption/pre-condition) and
$\mathcal{G}_{C}(\overline{o_{C}})$ (guarantee/post-condition), where
$\overline{i_{C}}$ and $\overline{o_{C}}$ are each a vector of variables
representing the node’s inputs/outputs, respectively. (Note that, when
discussing one specific component, we often omit the $C$ subscript.)

Complex robotic systems often produce and consume streams of data. Our
approach to stream semantics is based on well-established work in the area of
stream logic programming [46, 47]. In our approach, a stream is a list of
data: $[e|Tail]$, where $e$ is the first element in the list and $Tail$ is the
remaining elements. When receiving data, a component taks $e$ from the stream,
processes is, and recurses with $Tail$.

Each contract states that if a node consumes input data $\overline{i}$ from
its input stream ($\mathsf{InStream}([\overline{i}\mid S])$) and
$\mathcal{A}(\overline{i})$ holds (i.e., $\overline{i}$ satisfies the
assumption/pre-condition for correct operation of the node) then eventually
the node will place some data, $\overline{o}$ on its output stream that
satisfies the node’s guarantee. So if its current output stream was $T$, i.e.
$\mathsf{OutStream}(T)$,

before the execution of the node666$T$ is the sequence of outputs so far.
functionality on $\overline{i}$, then afterwards the output stream will be
$\mathsf{OutStream}([\overline{o}\mid T])$ and $\mathcal{G}(\overline{o})$
will hold. While our contract assumptions and guarantees are expressed using
FOL. We represent the meaning of the contract by a small extension using the
“eventually” operator, ‘$\lozenge$’ from Linear-time Temporal Logic (LTL)
[48]. Thus, a contract guarantees:

$\small{\begin{array}[]{c}(\mathsf{InStream}([\overline{i}\mid
S])\,\land\,\mathcal{A}(\overline{i})\,\land\,\mathsf{OutStream}(T))\\\
\Rightarrow\\\
\lozenge(\mathsf{InStream}(S)\,\land\,\mathcal{G}(\overline{o})\,\land\,\mathsf{OutStream}([\overline{o}\mid
T]))\end{array}}$

for any streams $S$ and $T$.

The temporal logic element is used to abstract from internal
computation/activity. As this is never instantaneous, nor do we have precise
timing constraints, the execution of one component is described as
_eventually_ completing. Hence the use of the “sometime in the future”
temporal operator ‘$\lozenge$’. Later in the development process, this very
general temporal constraint might be refined to more precise real-time
computational properties.

As in Stream Logic Programming, we will have rules to deal with end cases,
such as when the remaining input list/vector is empty. Note that in such cases
we might choose to terminate the processing, to suspend and wait until the
list or vector is non-empty, to perform some exception handling, or undertake
any other required computation.

Also, a component can consume, or produce, multiple streams. For example, we
might have a component consuming items from several streams to generate a
combined output (on one stream). Whether we take an item from each stream
simultaneously or just take an item from one of the streams (or any
combination of these approaches) will depend on the component, and the
component verification should account for this where appropriate. Note that we
deliberately say nothing about the global behaviour of concurrent streams, for
example whether one is generated more quickly than another, instead focusing
on the first element on each relevant stream. These concurrency aspects might
well be explored in future work but, for this initial investigation, we
concentrate on the straightforward case for clarity of explanation.

Although we use FOL to specify contracts, we require a machine-readable syntax
for capturing and generating monitors for contracts. For this, we introduce
RCL in the next subsection.

Figure 2: A flow chart showing Vanda’s monitor synthesis workflow. The rectangles represent steps in the workflow, and the solid lines show the flow of control between the steps. The parallelograms represent input or output files, and the dotted lines show the file being input to or output from a step.  start : |  contract_clause+
---|---
contract_clause : |  node_clause | context_clause
context_clause : |  “context” “{” (type_declaration
|  | constant_declaration)+ “}”
type_declaration : |  STRING “:” type_declaration_part “;"
constant_declaration : |  STRING “=” type_declaration_part “;”
type_declaration_part : |  ? a function declaration, set, sequence, or tuple ?
node_clause : |  “node” STRING “{” inputs outputs topic_list (assume)* (guarantee)+ “}”
inputs : |  “inputs” “(” (io_var (“,” io_var)*)? “)”
outputs : |  “outputs” “(” (io_var (“,” io_var)*)? “)”
io_var : |  STRING “:” STRING
topic_list : |  “topics” “(” (topic (“,” topic)*)? “)”
topic : |  TYPE STRING
|  (“matches” “(” topic_match_name “)” )?
topic_match_name : |  io_pointer? STRING
io_pointer : |  “in.” | “out.”
assume : |  (“assume”) “(” formula “)”
guarantee : |  (“guarantee”) “(” formula “)”
formula : |  ? Textual Definition of FOL?
TYPE : |  ? Types from ROS or custom type ?
STRING : |  ? Character String?
Table 1: A simplified description of RCL’s syntax in Extended Backus-Naur form
(EBNF). A “|” shows alternatives, quotation marks shows literals, a “?” shows
zero or one instances, a “*” shows zero or more instances, a “+” shows one or
more instances. Textual descriptions of a rule are enclosed in “?”.

###  3.3 Specifying Nodes in the ROS Contract Language

RCL captures a node’s FOL contract; plus a description of the node’s inputs
and outputs, and the ROS topics to which they correspond. This ties the node’s
contract to its ROS implementation, in a way that enables monitor synthesis.

RCL contracts describe the behaviour of a node, at a higher level than a
mission/task specification. An RCL contract describe the behaviour of a node
regardless of if that node is an autonomous decision-maker, a planning system,
or a simple deterministic program or hardware component.

Each assumption and guarantee is declared separately, in a plain-text version
of FOL, which uses keywords such as forall and in to represent logical
operators. Table 1 shows a simplified Extended Backus-Naur form (EBNF) grammar
for an RCL contract. The “TYPE” rule defines the builtin ROS message types and
allows custom types to be defined. Listing LABEL:list:CS1AgentRCL (§4.2) shows
one of the RCL contracts we used during this work.

Vanda777Vanda, which means ‘Oath’ in Quenya, is available at:
https://github.com/autonomy-and-verification/ros-contract-
language/tree/v0.3.1-ras Accessed: 03/11/2023 parses RCL files, synthesises
executable monitors (§3.6), and can produce LaTeX versions of the contracts.
It is written in Python3 and uses the Lark parsing library888Lark parsing
library: https://github.com/lark-parser/lark Accessed: 03/11/2023. Fig. 2
shows the steps taken (and files involved) in the synthesis of a monitor from
an RCL contract. This process comprises the following three steps. (1) parse:
parse a contract file and, if the contract is well-formed, produce a parse
tree. (2) extract: pre-process the parse tree from Step 1 to extract the node
name, topics and, guarantees into a Contract object. (3) translate: a contract
translator uses the Contract object from Step 2 to produce the configuration
file and monitor structure. The guarantees are translated by a FOL translator
class, which is a Lark Interpreter that converts the FOL parse tree into the
monitoring language (§3.6).

Vanda is built so as to make it easy to change the input and output formats.
The input language is defined in a Lark grammar, so that we can update RCL if
needed. The translation is implemented by two files (the contract translator
and FOL translator mentioned previously), so updating Vanda to produce
monitors in a different formalism should be relatively straightforward.

So far, we have described how contracts for individual nodes are expressed in
FOL and discussed how these are encoded in RCL. Next we present our calculus
for reasoning about how specifications for individual nodes are combined.

###  3.4 Calculus for Combining Node Specifications

Nodes in a (modular) system can be linked as long as their input types and
requirements match. The basic way to describe these structures is to first
have the contract capture all input and output variables and then describe how
they are combined using suitable inference rules. We compose the contracts of
individual nodes in a number of ways, the simplest being sequential
composition:

R1:

$\small{\begin{array}[]{l}\forall\overline{i_{1}},\overline{o_{1}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\
\Rightarrow\ \lozenge\mathcal{G}_{1}(\overline{o_{1}})\\\ \hskip
70.0pt\vdots\\\
\forall\overline{i_{n}},\overline{o_{n}}\cdot\mathcal{A}_{n}(\overline{i_{n}})\
\Rightarrow\ \lozenge\mathcal{G}_{n}(\overline{o_{n}})\\\
\overline{o_{1}}=\overline{i_{2}}\land\ldots\land\overline{o_{n-1}}=\overline{i_{n}}\\\
\vdash\
\bigg{(}\forall\overline{o_{1}},\overline{i_{2}}\cdot\mathcal{G}_{1}(\overline{o_{1}})\
\Rightarrow\ \mathcal{A}_{2}(\overline{i_{2}})\\\ \hskip 68.0pt\land\\\ \hskip
70.0pt\vdots\\\ \hskip 68.0pt\land\\\ \ \ \ \ \
\forall\overline{o_{n-1}},\overline{i_{n}}\cdot\mathcal{G}_{n-1}(\overline{o_{n-1}})\
\Rightarrow\ \mathcal{A}_{n}(\overline{i_{n}})\bigg{)}\\\
\hline\cr\bigg{(}\forall\overline{i_{1}},\overline{o_{n}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\
\Rightarrow\ \lozenge\mathcal{G}_{n}(\overline{o_{n}})\bigg{)}\end{array}}$

$1$ $\mathcal{A}_{1}(\overline{i_{1}})$$\mathcal{G}_{1}(\overline{o_{1}})$
$\bullet$ $\bullet$$\bullet$ $n$
$\mathcal{A}_{n}(\overline{i_{n}})$$\mathcal{G}_{n}(\overline{o_{n}})$

Rule R1 applies to nodes that are connected in a linear sequence, where the
output of one is the input of the next, etc. If the guarantee of the first
implies the assumption of the second etc. then, if the assumption of the first
node holds, we can conclude that the guarantees of the final node in the
sequence will eventually hold. This rule provides a basic starting point,
however, robotic systems are generally more complex than this, often including
multiple, branching outputs.

R2:

$\small{\begin{array}[]{l}\forall\overline{i_{1}},\overline{o_{1}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\
\Rightarrow\ \lozenge\mathcal{G}_{1}(\overline{o_{1}})\\\ \hskip
70.0pt\vdots\\\ \forall\overline{i_{n}},\overline{o_{n}}\cdot\
\mathcal{A}_{n}(\overline{i_{n}})\ \Rightarrow\
\lozenge\mathcal{G}_{n}(\overline{o_{n}})\\\
\overline{o}_{1}=\overline{i_{2}}\cup\ldots\cup\overline{i_{n}}\\\ \vdash\
\bigg{(}\forall\overline{o_{1}},\overline{i_{2}},\ldots,\overline{i_{n}}\cdot\
\mathcal{G}_{1}(\overline{o_{1}})\Rightarrow\
\mathcal{A}_{2}(\overline{i_{2}})\\\ \hskip 68.0pt\land\\\ \hskip
70.0pt\vdots\\\ \hskip 68.0pt\land\hskip
40.0pt\mathcal{A}_{n}(\overline{i_{n}})\bigg{)}\\\
\hline\cr\bigg{(}\forall\overline{i_{1}},\overline{o_{2}},\ldots,\overline{o_{n}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\\\
\ \ \ \ \Rightarrow\
\lozenge\mathcal{G}_{2}(\overline{o_{2}})\land\ldots\land\lozenge\mathcal{G}_{n}(\overline{o_{n}})\bigg{)}\end{array}}$

$1$ $\mathcal{A}_{1}(\overline{i_{1}})$$\mathcal{G}_{1}(\overline{o_{1}})$ $2$
$\mathcal{A}_{2}(\overline{i_{2}})$$\mathcal{G}_{2}(\overline{o_{2}})$
$\bullet\bullet\bullet$ $n$
$\mathcal{A}_{n}(\overline{i_{n}})$$\mathcal{G}_{n}(\overline{o_{n}})$

Rule R2 is used when a node has branching outputs. Here, the combined inputs
of all of the ‘leaf’ nodes is equal to the output of the ‘root’ node, while
the guarantee of the ‘root’ node implies the assumptions of each ‘leaf’ node,
as shown above (where we assume that the union operator, $\cup$, can takes
vectors as parameters and merge them in the same way as with sets).

Rule R3 deals with the converse architecture, where a node’s input is the
union of several outputs from other nodes. As expected, this rule is
essentially the dual of R2. Note that there is a simplifying assumption here:
that the outputs persist once generated, according to the $\lozenge$
constraint. Under this assumption, all the required inputs (from nodes $1$ to
$n-1$) will be available at the same time. In future work, we will consider
weakening this assumption, thus adding further timing constraints.

R3:

$\small{\begin{array}[]{l}\forall\overline{i_{1}},\overline{o_{1}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\
\Rightarrow\ \lozenge\mathcal{G}_{1}(\overline{o_{1}})\\\ \hskip
70.0pt\vdots\\\
\forall\overline{i_{n}},\overline{o_{n}}\cdot\mathcal{A}_{n}(\overline{i_{n}})\
\Rightarrow\ \lozenge\mathcal{G}_{n}(\overline{o_{n}})\\\
\overline{i_{n}}=\overline{o_{1}}\cup\ldots\cup\overline{o_{n-1}}\\\ \vdash\
\bigg{(}\forall\overline{i_{n}},\overline{o_{1}},\ldots,\overline{o_{n-1}}\cdot\mathcal{G}_{1}(\overline{o_{1}})\\\
\hskip 68.0pt\land\\\ \hskip 70.0pt\vdots\\\ \hskip 68.0pt\land\\\ \hskip
40.0pt\mathcal{G}_{n-1}(\overline{o_{n-1}})\
\Rightarrow\mathcal{A}_{n}(\overline{i_{n}})\bigg{)}\\\
\hline\cr\bigg{(}\forall\overline{i_{1}},\ldots\
\overline{i_{n-1}},\overline{o_{n}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\land\ldots\land\mathcal{A}_{n-1}(\overline{i_{n-1}})\Rightarrow\lozenge\mathcal{G}_{n}(\overline{o_{n}})\bigg{)}\end{array}}$

$n$ $\mathcal{A}_{n}(\overline{i_{n}})$$\mathcal{G}_{n}(\overline{o_{n}})$ $1$
$\mathcal{A}_{1}(\overline{i_{1}})$$\mathcal{G}_{1}(\overline{o_{1}})$
$\bullet\bullet\bullet$ $n-1$
$\mathcal{A}_{n-1}(\overline{i_{n-1}})$$\mathcal{G}_{n-1}(\overline{o_{n-1}})$

These three simple inference rules (R1, R2 and R3) constitute our basic
calculus for reasoning about node-level FOL contracts in a robotic system. We
do _not_ specify the fine-grained concurrency/streaming of processes/data but
are just specifying the interface expectations of nodes in a robotic system.

We use the $\lozenge$ operator from FOTL to represent that some arbitrary time
has passed. Using the $\lozenge$ operator gives us the flexibility to describe
and refine a range of temporal aspects. We assume that contracts are neither
mutually dependent, nor circularly dependant. However, we intend to
investigate this in future work and potentially leverage existing techniques
like [49].

We can extend R1-3 with rule R4, below, which captures looping behaviour. We
consider this rule to be an extension to our core calculus because it is
directly derived from the first three rules.

R4:

$\small{\begin{array}[]{l}\forall\overline{i_{1}},\overline{o_{1}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\
\Rightarrow\ \lozenge\mathcal{G}_{1}(\overline{o_{1}})\\\
\forall\overline{i_{2}},\overline{o_{2}}\cdot\mathcal{A}_{2}(\overline{i_{2}})\
\Rightarrow\ \lozenge\mathcal{G}_{2}(\overline{o_{2}})\\\
\forall\overline{i_{3}},\overline{o_{3}}\cdot\
\mathcal{A}_{3}(\overline{i_{3}})\ \Rightarrow\
\lozenge\mathcal{G}_{3}(\overline{o_{3}})\\\
\forall\overline{i_{4}},\overline{o_{4}}\cdot\
\mathcal{A}_{4}(\overline{i_{4}})\ \Rightarrow\
\lozenge\mathcal{G}_{4}(\overline{o_{4}})\\\
\overline{i_{2}}=\overline{o_{1}}\cup\overline{o_{3}}\land\overline{i_{3}}=\overline{o_{2}}\land\overline{o_{3}}\subseteq\overline{i_{4}}\\\
\vdash\forall\overline{i_{2}},\overline{o_{3}}\cdot\mathcal{A}_{2}(\overline{i_{2}})\Rightarrow\lozenge\mathcal{G}_{3}(\overline{o_{3}})\\\
\vdash\forall\overline{i_{3}},\overline{o_{2}},\overline{o_{4}}\cdot\mathcal{A}_{3}(\overline{i_{3}})\
\Rightarrow\
\lozenge\mathcal{G}_{2}(\overline{o_{2}})\land\lozenge\mathcal{G}_{4}(\overline{o_{4}})\\\
\vdash\forall\overline{i_{1}},\overline{i_{3}},\overline{o_{2}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\land\mathcal{A}_{3}(\overline{i_{3}})\
\Rightarrow\ \lozenge\mathcal{G}_{2}(\overline{o_{2}})\\\
\hline\cr\bigg{(}\forall\overline{i_{1}},\overline{o_{4}}\cdot\mathcal{A}_{1}(\overline{i_{1}})\
\Rightarrow\ \lozenge\mathcal{G}_{4}(\overline{o_{4}})\bigg{)}\end{array}}$

$1$ $\mathcal{A}_{1}(\overline{i_{1}})$$\mathcal{G}_{1}(\overline{o_{1}})$ $2$
$\mathcal{A}_{2}(\overline{i_{2}})$$\mathcal{G}_{2}(\overline{o_{2}})$ $3$
$\mathcal{A}_{3}(\overline{i_{3}})$$\mathcal{G}_{3}(\overline{o_{3}})$ $4$
$\mathcal{A}_{4}(\overline{i_{4}})$$\mathcal{G}_{4}(\overline{o_{4}})$

Observe that the three lines with the $\vdash$ symbol are a direct result of
applying R1, R2 and R3, respectively, to the nodes in the loop illustration
above. The conclusion below the line is drawn from their combination and
simplification. Although not part of our core calculus, we list R4 here to
explicitly capture the behaviour of loops and it can easily be extended to
incorporate an arbitrary number of nodes between nodes 2 and 3 in the loop
illustration above. Alternatively, we could augment R4 to include fixed-point
reasoning in first-order temporal logic [50].

Our inference rules describe how node contracts should be interpreted when
multiple nodes are combined in various ways. These rules are simple and
therefore transparently sound. For brevity, we omit the soundness proofs here
because they don’t add to the novelty of this paper. It is a separate
verification step to demonstrate that the individual node itself obeys its own
contract and we discuss this in more detail in the next subsection.

###  3.5 Guiding Heterogeneous Verification

Our RCL contracts provide a high-level specification of the system’s
requirements. These node-level contracts are used to guide the verification of
individual nodes, because a formal link is often difficult or impossible.
However, the FOL specification, and other information in the contract, can be
used to inform the (formal or non-formal) verification process.

Each node can present its own challenges when verifying that it obeys its FOL
contract, so the most suitable verification method should be chosen for each
node. Some nodes may be amenable to formal verification, such as an agent that
can be model checked for correctness properties (as in our previous work
[19]). Other nodes may be based on neural networks, e.g. a vision classifier
that might need a specific testing approach [51]. Some nodes might be more
critical to the system’s safety requirements than others, these nodes are
likely to be the focus of the most robust formal verification (as we suggest
in [52, 53]). Our approach leaves whoever is verifying the node to choose the
most suitable verification method(s), since they are best placed to make this
decision.

We use the contract’s high-level specification as a guide, or a target for
what properties a particular node should obey, supporting developing the
system from abstract specifications. Specifying what a system should do is
often the most time-consuming part of formal verification [54]. so reusing a
specification throughout the development process makes that initial effort
more worthwhile.

When developing a system from an abstract specification, a developer can start
by specifying a high-level contract for a node’s basic behaviour, and then
verify more concrete properties about the node’s functionality using their
chosen verification method. For example, as in [28], a high-level contract for
a planner might require that all the plans it produces are obstacle-free, but
the detailed planner verification might also verify that all points in the
plan are valid (e.g. within the map), that the planner does not deadlock, or
that the plan conforms to some measure of optimality.

Crucially, our approach enables a system to be verified using a range of
verification techniques without needing to decide beforehand which techniques
will be used. As mentioned in §1, using a variety of heterogeneous
verification techniques on one system can be beneficial, particularly in the
robotics domain [10, 14, 19, 28, 43].

The path from an RCL contract to formal verification is fairly clear, as we
describe in §4. Some formal methods are also based on FOL and sets, so the
guarantees in the contracts can be checked directly. Whereas, for other
methods, more effort may be needed to capture the contract’s properties in its
specification language. In either case, the contract describes the properties
that the chosen formal method must check.

The path from an RCL contract to non-formal verification is made easier
because each contract provides an unambiguous specification of a node’s
requirements. A suitably skilled test engineer should be able to, for example,
create software tests, simulation scenarios, etc.; that check the node for the
properties described in the guarantee. Having a formal specification provides
validation that the ‘right’ properties are being verified.

###  3.6 A Runtime Verification Safety-Net

The final part of our approach is to introduce a _safety net_ of RV monitors,
one for each RCL contract. Each monitor compares a trace of events produced by
the system, with a formal model of the intended behaviour. This RV safety net
ensures that the nodes conform to their contracts and, consequently, support
the inferred system-level properties.

We use the formalism-agnostic general-purpose framework, ROSMonitoring [55],
which is built for RV of ROS systems. The monitors used by ROSMonitoring
follow a standard publish/subscribe pattern. Each monitor is a ROS node that
subscribes to the topics needed to observe the behaviour that is relevant to
its property, and publishes a message to inform the system that a violation
was observed. We chose ROSMonitoring because its monitors can be easily
distributed through the system to check the contracts for each node, and it
can be used with various versions of ROS/ROS2.

instrumentconfig.yamlnodesmonitor.pyROSlog.txtoraclespeconlineoffline

Figure 3: High-level overview of ROSMonitoring [55].

#### From RCL topics to ROSMonitoring configuration file

ROSMonitoring takes a configuration file as input (‘config.yaml’ in Fig. 3)
where the user specifies the nodes and the topics that will be analysed by the
monitors. Our tool, Vanda, automatically generates a configuration file from
an RCL specification. Generating the configuration file only requires the name
of the topics to monitor and their message types. An example of a
configuration file is shown later when we describe the case study (§4.5).

Given a configuration file, ROSMonitoring generates one (or multiple) runtime
monitor(s) and changes the ROS system nodes to allow the monitors to intercept
the message exchanges needed for the verification. The remaining step is to
produce the _Oracle_ , the component that performs the formal verification.

#### From RCL guarantees to an RML Oracle

The Oracle (shown in Fig. 3) verifies that a system’s trace obeys the formal
specification, producing a verdict as output. In ROSMonitoring, the Orcale is
decoupled and can be specified with any formalism, here we have chosen the
Runtime Monitoring Language (RML) [56] because the translation from RCL to RML
was the most intuitive and direct.

An RML property is a tuple $\langle t,ETs\rangle$, with a term $t$ , and a set
of event types $ETs=\\{ET_{1},\ldots,ET_{n}\\}$. An event type $ET$ is
represented as a set of pairs $\\{k_{1}:v_{1},\ldots,k_{n}:v_{n}\\}$, where
each pair identifies a specific piece of information ($k_{i}$) and its value
($v_{i}$). Given an event type $ET$, an event $Ev$, denoted as a set of pairs
$\\{k_{1}^{\prime}:v_{1}^{\prime},\ldots,k_{m}^{\prime}:v_{m}^{\prime}\\}$ as
well, matches $ET$ if $ET\subseteq Ev$, which means $\forall(k_{i}:v_{i})\in
ET\cdot\exists(k_{j}:v_{j})\in Ev\cdot k_{i}=k_{j}\land v_{i}=v_{j}$. In
practice, an event type $ET$ specifies the requirements an event $Ev$ has to
satisfy to be considered valid. For instance, an event type $ET$ could be
$\\{pos:(waypoint1)\\}$, meaning that all events containing $pos$ with value
$(waypoint1)$ are valid. An event $Ev$ generated by a moving robot could be
$\\{speed:1.6,pos:(waypoint1)\\}$, meaning that the robot is moving at speed
$1.6$ [m/s], and is currently at position $(waypoint1)$.

An RML term $t$ can be:

  * •

$ET$, denoting a singleton set containing the events $Ev$ s.t. $ET\subseteq
Ev$

  * •

$t_{1}\;t_{2}$, denoting the concatenation of two sets of traces

  * •

$t_{1}\land t_{2}$, denoting the intersection of two sets of traces

  * •

$t_{1}\lor t_{2}$, denoting the union of two sets of traces

  * •

$\\{let\;x;t^{\prime}\\}$, denoting the set of traces $t^{\prime}$ where the
variable $x$ can be used

  * •

$t^{\prime}*$, denoting a chain of concatenations of trace $t^{\prime}$

where $t_{1}$, $t_{2}$ and $t^{\prime}$ are RML terms.

Event types can be negated. Given an event type $ET$, the term $\lnot ET$
denotes its negation. Specifically, $\forall_{Ev}.ET\subseteq Ev\iff\lnot
ET\nsubseteq Ev$. In the rest of the paper, we also apply the notion of
negation to the other RML terms. For instance, if the term is $ET_{1}\land
ET_{2}$, its negation is $\lnot ET_{1}\lor\lnot ET_{2}$; and the same
reasoning is applied for the other operators.

Event types can contain variables. Considering the previous event type, we
could have its parametric version as $ET(x)=\\{pos:(x)\\}$, where we do not
force any value for the waypoint. This event type matches all events
containing $pos$ with any $x$ value. When an event matches an event type with
variables, the variables get the values from the event.

An example of using RML to define contracts, consider the term
$ET_{1}ET_{2}\lor ET_{3}ET_{4}$, with $ET_{i}$ being some event type
describing a certain kind of event (as before). However, differently from
before, here, we have a union of two concatenations; which means the language
recognised by this term is

$\\{Ev\;Ev^{\prime}\;|\;ET_{1}\subseteq Ev,ET_{2}\subseteq
Ev^{\prime}\\}\cup\\{Ev\;Ev^{\prime}\;|\;ET_{3}\subseteq Ev,ET_{4}\subseteq
Ev^{\prime}\\}$

Naturally, the same reasoning can be applied to the $\land$ operator; the only
difference would be in using $\cap$ instead of $\cup$.

$\begin{array}[]{c}\scriptstyle{\textrm{({atom})}}{\displaystyle\frac{}{atom\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
atom,\\{\\}\rangle}}\
\qquad\scriptstyle{\textrm{({and/or})}}{\displaystyle\frac{g_{1}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{1},ET_{1}\rangle\land
g_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{2},ET_{2}\rangle}{g_{1}op\>g_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{1}op\>t_{2},ET_{1}\cup ET_{2}\rangle}}\
op\in\\{\land,\lor\\}\\\\[11.62495pt]
\scriptstyle{\textrm{({iff})}}{\displaystyle\frac{g_{1}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{1},ET_{1}\rangle\land
g_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{2},ET_{2}\rangle}{g_{1}\iff
g_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle(t_{1}\land
t_{2})\lor(\lnot t_{1}\land\lnot t_{2}),ET_{1}\cup
ET_{2}\rangle}}\\\\[11.62495pt]
\scriptstyle{\textrm{({implies})}}{\displaystyle\frac{g_{1}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{1},ET_{1}\rangle\land
g_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{2},ET_{2}\rangle}{g_{1}\implies
g_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle(\lnot t_{1}\land
t_{2})\lor(\lnot t_{1}\land\lnot t_{2})\lor(t_{1}\land t_{2}),ET_{1}\cup
ET_{2}\rangle}}\\\\[11.62495pt]
\scriptstyle{\textrm{({equals})}}{\displaystyle\frac{}{a_{1}==a_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
ET,\\{\langle ET,(a_{1}:a_{2})\rangle\\}\rangle}}\\\
\scriptstyle{\textrm{({not-
equals})}}{\displaystyle\frac{}{a_{1}!=a_{2}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle\lnot
ET,\\{\langle ET,(a_{1}:a_{2})\rangle\\}\rangle}}\\\\[11.62495pt]
\scriptstyle{\textrm{({exists})}}{\displaystyle\frac{g\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t,ET\rangle}{\exists x\cdot
g\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle\\{let\>x;t\\},ET\rangle}}\
\scriptstyle{\textrm{({guarantee})}}{\displaystyle\frac{g\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t,ET\rangle}{G(g)\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle(t)*,ET\rangle}}\\\\[11.62495pt]
\scriptstyle{\textrm{({guarantees})}}{\displaystyle\frac{g_{1}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{1},ET_{1}\rangle\land\ldots\land
g_{n}\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{n},ET_{n}\rangle}{G(g_{1}),\ldots,G(g_{n})\stackrel{{\scriptstyle{}}}{{\rightarrow}}\langle
t_{1}\land\ldots\land t_{n},ET_{1}\cup\ldots\cup ET_{n}\rangle}}\end{array}$

Figure 4: RML partial translation.

As previously mentioned, Vanda can translate contracts into RML
specifications; Fig. 4 shows the operational semantics of the translation
function from RCL descriptions to RML specifications that it implements. Here,
each rule formalises a single-step translation. For instance, the (and/or)
rule denotes how to translate the conjunction/disjunction of two RCL
guarantees. This can be done first by translating the two guarantees $g_{1}$
and $g_{2}$ into RML; then, by combining the results obtained using the
corresponding RML operator. For the (equals) rule, at the guarantee level we
require that a certain variable in a topic has a specific value. This is
mapped into an event type that requires the event to have the same value.
Recall that an event matches an event type if the latter is included in the
former. Since we want to guarantee that the information identified by $a_{1}$
has value $a_{2}$, the resulting event type has to check that this holds,
which can be done by adding the pair $a_{1}:a_{2}$ in the event type.

The (exists) rule tackles the use of variables. In RCL, the contract says that
there exists an $x$ for which the guarantee $g$ holds. This can be
straightforwardly mapped into a parametric term in RML, where the variable $x$
is used inside the term $t$ (the one derived by $g$). As usual, the (forall)
rule can be obtained by negating the (exists) rule. Finally, the (guarantee)
and (guarantees) rules denote the translation step for single and multiple
guarantees, respectively. To translate multiple guarantees, each guarantee
$g_{i}$ is translated separately, and the resulting RML terms $t_{i}$ are
combined using the $\land$ RML operator. In this way, all guarantees are
required to be satisfied. To translate a guarantee $G(g)$, first $g$ is
translated into the RML term $t$. A $*$ post-fix operator is then added to
$t$, meaning that $t$ can be repeated as many times as necessary. We need this
operator because the guarantees need to be checked continuously, and not only
once.

#### From RCL to ROSMonitoring monitors

The generation of monitors in ROSMonitoring from RCL guarantees requires one
more additional step. The RCL specifications are based on an abstraction of
the system, while the monitors in ROSMonitoring are deployed in the real
system under execution. Therefore, to ensure the monitors will be able to
capture all the necessary events (execution traces) produced by the system, it
is necessary to instrument the system with any missing events. For example,
these missing events can be a mismatch of names used in the contracts versus
what is used in the implemented system, different representations of data
types, implicit information that is not directly being published in a ROS
topic, etc.

##  4 Case Study: Remote Inspection

Our case study is a _Jackal_ 999Jackal: https://clearpathrobotics.com/jackal-
small-unmanned-ground-vehicle/ Accessed: 03/11/2023 rover performing remote
inspection in a nuclear waste store, in a 3D Gazebo101010Gazebo Simulator:
http://gazebosim.org/ Accessed: 03/11/2023 simulation. The Jackal uses a
(simulated) sensor to take radiation measurements at given waypoints. We
adapted this case study from the simulation described in [57], adding an
autonomous agent that makes the high-level decisions that control the Jackal.

The rover’s goal is to inspect 12 waypoints that are located inside the
simulated nuclear waste store (see Fig. 5). The autonomous agent decides which
waypoint to inspect next, depending on the current radiation readings. It
should always be aware of high radiation values, since this could put the
robot in danger, as well as indicating a problem in the waste store that
requires further investigation. The rover’s battery is not simulated, so we
assume that the rover has enough power for the duration of the scenario. We
use the ROS _move base_ package for low-level path planning.

Figure 5: Simulation environment of the remote inspection case study. On the
left-hand side is the Gazebo 3D simulation window. On the top right-hand side
is the RViz window, a visualisation interface containing the map that the
rover uses for path planning, a visual representation of radiation levels
(green, orange, red) around the robot, and the waypoints from 0 to 12 that the
robot must inspect. On the bottom right-hand side is the autonomous agent
console with the log of its execution.

At a high level the system should obey the following requirements.

REQ1:

The robot should inspect each waypoint as long as the radiation level at a
waypoint is not high (“red").

REQ2:

Each waypoint only needs to be inspected at least once.

REQ3:

If the radiation level at a waypoint is too high, then the robot will abandon
the mission and return to the entry point.

REQ4:

Eventually, all waypoints will have been inspected; or the mission will have
terminated in failure, due to high level of radiation.

In the rest of this section, we describe how to apply our approach to the
remote inspection case study, from the manual specification of the contracts
to the automatic generation of runtime monitors. The simulation environment,
contracts, and verification assets for this chapter are available from the
Zenodo repository that accompanies this paper:
https://doi.org/10.5281/zenodo.6941344.

###  4.1 Step 1: Creating a System Model

In this section we describe how we generated the system model for the remote
inspection case study. Fig. 6 shows the ROS graph of the remote inspection
robotic system (minus the autonomous agent, because it is not programmed using
ROS). As described in §3, we often find it helpful to adapt the ROS graph to
produce a system model that is more amenable to analysis and verification.

Figure 6: ROS graph automatically generated for the remote inspection case
study. The ovals represent ROS nodes and the rectangles represent topics. The
arrows connecting nodes and topics show the direction of messages.

Here, most of the nodes are well-tested off-the-shelf libraries, such as the
Jackal _velocity controller_ and the _move base_ library. The former relates
to the Jackal’s internal velocity controllers, while the latter provides a
suite of path planners. Both relate to the robot’s navigation, and thus we
abstract them into a _compound_ node called Navigation. Similarly, we merge
the nodes _imu_ and _odometry_ ,into the Localisation _compound_ node. We
obtain the Radiation Sensor node in a similar way. Finally, because the
autonomous agent is external to the ROS system, we create the Agent node as an
abstraction of its implementation. Thus, the system model is composed of these
four abstracted nodes, shown in Fig. 7 and described below.

Localisation $\overline{i_{L}}$: sensors : SensorsType
---
$\overline{o_{L}}$: position : PositionType
Navigation $\overline{i_{N}}$: position : PositionType,
---
command : CommandSet
$\overline{o_{N}}$: at : AtType
Agent $\overline{i_{A}}$: wayP : WayP, at : AtType,
---
radiationStatus : RadStat,
inspected : InspectedType
$\overline{o_{A}}$: command : CommandSet
Radiation Sensor $\overline{i_{R}}$: r : REAL,
---
command : CommandSet
$\overline{o_{R}}$: radiationStatus : RadStat,
inspected : InspectedType
Context $WayP:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{N}$
$RadStat:\\{red,orange,green\\}$
$CommandSet:\\{move(\mathbb{R},\mathbb{R}),inspect(\mathbb{N})\\}$
$PositionType:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{B}$
$AtType:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{B}$
$InspectedType:\mathbb{N}\rightarrow\mathbb{B}$ $SensorsType:\emptyset$

Figure 7: System model for the remote inspection case study. Arrows indicate
data flow between the nodes.

Localisation: abstracts the Adaptive Monte Carlo Localisation (AMCL) ROS
package111111Adaptive Monte Carlo Localisation package:
http://wiki.ros.org/amcl Accessed: 03/11/2023, which uses sensor input to
perform localisation. This is a well established package, so we do not define
a contract for its specifics. Instead, it is enough (for our purposes) to know
that the node will output what it believes to be the robot’s position. The
Localisation node takes input from hardware (a variety of sensors), but our
contracts focus on the links between the software nodes; so it is enough for
our contracts to specify its input as $\emptyset$ (defined as $SensorsType$ in
the specification’s context clause, because the inputs and outputs are name-
type pairs), knowing that the node will be able to access the sensor
information.

Navigation: abstracts the well known _move base_ package, which performs low-
level path planning. Its inputs are the estimated position from the
Localisation node, and the command from the Agent node to move to a particular
position. It outputs a function mapping coordinates to a boolean, which is
true if the Robot is at that position.

Agent: the most critical node to verify; because it makes the high-level
decisions for the robot, and its implementation is not based on preexisting
ROS packages. The agent is implemented in the agent programming language
Gwendolen [58]. Its inputs are the output of the Navigation and Radiation
Sensor nodes. It outputs a high-level command (either move or inspect).

Radiation Sensor: takes as input a radiation measurement $r$ from its internal
sensor and the command from the Agent to inspect a particular waypoint $i$. It
outputs a confirmation that a particular waypoint has been inspected.

Once the model has been distilled, the next step is to define contracts for
the individual nodes.

###  4.2 Step 2: Specifying Node Contracts

This step builds the contracts used to guide the heterogeneous verification
and to enable synthesis of the runtime monitors. Each contract is written in
RCL (described in §3.3), and consists of a node’s inputs, outputs,
assumptions, and guarantees (which are all written in a plain-text encoding of
FOL). A contract also links the inputs and outputs to the topics in the
underlying ROS program.

As an example, Listing LABEL:list:contextRCL shows the context clause that
defines the types and constants used in the specification of our case study
and Listing LABEL:list:CS1AgentRCL shows the RCL contract for the Agent node.
In the Agent’s contract, Listing LABEL:list:CS1AgentRCL, lines 3 and 5
identify the node’s inputs and outputs, respectively.

Lines 7–11 show the ROS topics that the Agent uses and which input or output
they correspond to (in the matches statement), using both built-in types (e.g.
Int16) and custom types that were defined in the underlying ROS system. On
line 14, the assume statement contains the assumption of the Agent’s contract.
From line 16 onward, the guarantee statements contain a plain-text encoding of
the Agent’s FOL guarantees. The overall links between the four nodes, and the
inputs and outputs that link them, are shown in Fig. 7.

⬇

1context{

2 WayP : REAL x REAL –> NATURAL ;

3 RadStat : {red, orange, green} ;

4 CommandSet : { move(REAL, REAL), inspect(NATURAL) };

5 PositionType : REAL x REAL –> BOOL ;

6 AtType: REAL x REAL –> BOOL;

7 InspectedType : NATURAL –> BOOL;

8 SensorsType : {}; }

⬇

1node agent{

2

3inputs( wayP : WayP, at : AtType, radiationStatus : RadStat, inspected :
InspectedType )

4

5outputs( command : CommandSet )

6

7topics( gazebo_radiation_plugins/Command command matches(out.command),

8gazebo_radiation_plugins/Inspection inspected matches(in.inspected),

9gazebo_radiation_plugins/At at matches(in.at),

10int16 wayP matches(in.wayP),

11string radiationStatus matches(in.radiationStatus) )

12

13assume( in.radiationStatus in {red, orange, green} )

14

15guarantee(forall(x’, y’ in REAL, i in NATURAL |

16 in.at(x’, y’) == TRUE and in.wayP(x’, y’) == i and in.inspected(i) == TRUE
and in.radiationStatus !in {red, orange} ->

17 exists(x, y in REAL | (in.wayP(x, y) == i + 1 or

18 (forall( x”, y” in REAL | in.wayP(x”, y”) != i+1 and in.wayP(x, y) == 0))) and out.command == move(x, y) )) )

19

20guarantee(forall(x’, y’ in REAL, i in NATURAL |

21 in.at(x’, y’) == TRUE and in.wayP(x’, y’) == i and in.inspected(i) == FALSE
-> out.command == inspect(i) ) )

22

23guarantee(forall(x’, y’ in REAL, i in NATURAL |

24 in.radiationStatus in {red, orange} or not exists( x, y in REAL | in.wayP(x, y) == i + 1 )

25 -> exists (x”, y” in REAL | in.wayP(x”, y”) == 0 and out.command == move(x”, y”) ) ) )

26}

Localisation
---
Input | Text |  Input from hardware (a variety of sensors)
FOL |  $sensors:SensorsType$
Output | Text |  The robot’s estimated position
FOL |  $position:PositionType$
Assume | Text |  N/A
FOL |  $TRUE$
Guarantees | Text |  The node outputs a unique $(x,y)$ coordinate that is the robot’s estimated position
FOL |  $\exists!x,y\in\mathbb{R}\bullet out.position(x,y)$
Table 2: A summary of the Localisation node’s inputs, outputs, assumptions,
and guarantees.

Tables 2, 3, 4, and 5 summarise the inputs, outputs, assumptions, and
guarantees of each contract. The tables describe the statements in the
contract in English, and then shows the relevant part of the contract. The FOL
has been rendered with mathematical symbols for the convenience of the reader.
The full contracts, in RCL, are shown in A.

The information contained in the contracts is useful for guiding both formal
and non-formal verification of the nodes, as we describe later in §4.4. Vanda,
the RCL tool, can also automatically synthesise runtime monitors from the
contracts, which we describe in §4.5.

In the next step, we use our calculus to derive system-level properties from
the individual node contracts.

###  4.3 Step 3: Deriving System-Level Properties

In this section, we give an example of how our calculus (§3.4) works by
presenting the manual derivation of one of the system-level properties from
the contracts.

We start with the Agent node, which takes input from the Navigation and
Radiation Sensor. Because Agent takes several inputs, we instantiate R3, the
input union rule, to get D1:

$\small{\begin{array}[]{l}\forall\overline{i_{N}},\overline{o_{N}}\cdot\mathcal{A}_{N}(\overline{i_{N}})\
\Rightarrow\ \lozenge\mathcal{G}_{N}(\overline{o_{N}})\\\
\forall\overline{i_{R}},\overline{o_{R}}\cdot\
\mathcal{A}_{R}(\overline{i_{R}})\ \Rightarrow\
\lozenge\mathcal{G}_{R}(\overline{o_{R}})\hskip 100.0pt\text{(D1)}\\\
\forall\overline{i_{A}},\overline{o_{A}}\cdot\
\mathcal{A}_{A}(\overline{i_{A}})\ \Rightarrow\
\lozenge\mathcal{G}_{A}(\overline{o_{A}})\\\
\overline{i_{A}}=\overline{o_{N}}\cup\overline{o_{R}}\\\ \vdash\
\bigg{(}\forall\overline{i_{A}},\overline{o_{N}},\overline{o_{R}}\cdot\mathcal{G}_{N}(\overline{o_{N}})\land\mathcal{G}_{R}(\overline{o_{R}})\Rightarrow\mathcal{A}_{A}(\overline{i_{A}})\bigg{)}\\\
\hline\cr\bigg{(}\forall\overline{i_{N}},\overline{i_{R}},\overline{o_{A}}\cdot\mathcal{A}_{N}(\overline{i_{N}})\land\mathcal{A}_{R}(\overline{i_{R}})\Rightarrow\lozenge\mathcal{G}_{A}(\overline{o_{A}})\bigg{)}\end{array}}$

Navigation
---
Input | Text |  Robot’s estimated position from the Localisation node, and the command from the Agent node
FOL |  $position:PositionType,\quad command:CommandSet$
Output | Text |  Robot’s position
FOL |  $at:AtType$
Assume | Text |  There is a unique $(x,y)$ coordinate position that represents the Robot’s estimated position
FOL |  $\exists!x,y\in\mathbb{R}\bullet in.position(x,y)=TRUE$
Guarantees | Text |  If the Robot is told to move to $(x,y)$ and the Localisation node says that the Robot is at $(x,y)$; then Navigation will conclude that it is at $(x,y)$
FOL |  $\begin{array}[]{l}\forall x,y\in\mathbb{R}\bullet(\ (in.command=move(x,y))\land\\\ \hskip 2.84544pt(in.position(x,y)=TRUE))\iff out.at(x,y)=TRUE\end{array}$
Table 3: A summary of the Navigation node’s inputs, outputs, assumptions, and
guarantees.

To apply rule R3, we must show that we can deduce that the guarantees of the
Navigation and Radiation Sensor nodes imply the assumption of the Agent node:
$\forall\overline{i_{A}},\overline{o_{N}},\overline{o_{R}}\cdot\mathcal{G}_{N}(\overline{o_{N}})\land\mathcal{G}_{R}(\overline{o_{R}})\Rightarrow\mathcal{A}_{A}(\overline{i_{A}})$.
For these three nodes, this is instantiated as:

$\small{\begin{array}[]{l}\forall\overline{i_{A}},\overline{o_{N}},\overline{o_{R}}\cdot[\forall
x,y\in\mathbb{R}\cdot\\\ \quad in.command=move(x,y)\land
in.position(x,y)=true\Leftrightarrow out.at(x,y)=true]\\\ \t{1}\land[\forall
i\in\mathbb{N}\cdot
in.command=inspect(i)\Rightarrow(out.inspected(i)=true\land\\\
\quad\land(0\leq in.r<120\Rightarrow out.radiationStatus=green)\\\
\quad\land(120\leq in.r<250\Rightarrow out.radiationStatus=orange)\\\
\quad\land(250\leq in.r\Rightarrow out.radiationStatus=red))]\\\
\quad\Rightarrow out.radiationStatus\in\\{red,orange,green\\}\end{array}}$

which is true by virtue of our definition of $radiationStatus$.

Applying R3 here here allows us to conclude that if the nodes are correctly
linked (by showing that the property after the $\vdash$ in D1 holds) then we
can say that the correct input to the Navigation and Radiation Sensor nodes
will result in the guarantee of the Agent being preserved. Thus, the system-
level property that we derive is:

$\forall\overline{i_{N}},\overline{i_{R}},\overline{o_{A}}\cdot(\exists!x,y\in\mathbb{R}\cdot
position(x,y)=true)\land(0\leq
r)\Rightarrow\lozenge\mathcal{G}_{A}(\overline{o_{A}})$

which tells us that when the robot is in a valid, unique position; and the
observed radiation level is valid; then eventually the guarantee of the Agent
will hold. This demonstrates that the Agent’s guarantee is dependent on the
correct input and functioning of the Navigation and Radiation Sensor nodes.

The Agent’s guarantees (see Table 4) support the four requirements described
in the introduction to this section. The Agent guarantees that that each
waypoint will be inspected, unless dangerous levels of radiation are detected
by the Radiation Sensor (REQ1 and REQ4); that a waypoint is only inspected if
it hasn’t been inspected yet (REQ2); that if the radiation level at a waypoint
is too high, then it moves to the original waypoint (REQ3 and REQ4); and that
when there are no more waypoints to inspect, the robot will return to the
original waypoint (REQ1 and REQ4).

Agent
---
Input | Text |  Map of $x,y$ pairs to waypoint ids, function that is true if the robot is at that position, and Radiation Status and inspected values from Radiation Sensor
FOL |  $wayP:WayP,\quad at:AtType,\quad radiationStatus:RadStat,\quad inspected:InspectedType$
Output | Text |  The command (move or inspect)
FOL |  $command:CommandSet$
Assume | Text |  The Radiation Status that it receives is either red, orange, or green
FOL |  $in.radiationStatus\in\\{red,orange,green\\}$
Guarantees | Text |  If the Robot is at, and has inspected waypoint $i$, and the radiation level was not dangerous, then it will move to the next waypoint or to waypoint 0 (the exit) if there is no next waypoint.
FOL |  $\begin{array}[]{l}\forall x^{\prime},y^{\prime}\in\mathbb{R},i\in\mathbb{N}\bullet(\ (in.at(x^{\prime},y^{\prime})=TRUE)\\\ \quad\land(in.wayP(x^{\prime},y^{\prime})=i\land(in.inspected(i)=TRUE)\\\ \quad\land(in.radiationStatus\notin\\{red,orange\\})\ )\\\ \quad\implies(\exists x,y\in\mathbb{R}\bullet((in.wayP(x,y)=i+1\\\ \qquad\lor(\forall x^{\prime\prime},y^{\prime\prime}\in\mathbb{R}\bullet in.wayP(x^{\prime\prime},y^{\prime\prime})\neq i+1\\\ \qquad\quad\land in.wayP(x,y)=0))\\\ \qquad\quad\land out.command=move(x,y)))\end{array}$
Text |  And, if the Robot is at, and has not inspected, waypoint $i$, then inspect it.
FOL |  $\begin{array}[]{l}\forall x^{\prime},y^{\prime}\in\mathbb{R},i\in\mathbb{N}\bullet((in.at(x^{\prime},y^{\prime})=TRUE)\\\ \qquad\land(in.wayP(x^{\prime},y^{\prime})=i)\\\ \qquad\land(in.inspected(i)=FALSE))\\\ \quad\implies out.command=inspect(i)\end{array}$
Text |  And, if the Robot inspects a waypoint and the radiation level is dangerous, or there are no more waypoints, then return to the original waypoint (the exit)
FOL |  $\begin{array}[]{l}\forall x^{\prime},y^{\prime}\in\mathbb{R},i\in\mathbb{N}\bullet\\\ \quad((in.radiationStatus\in\\{red,orange\\})\\\ \qquad\lor(\neg\exists x,y\in\mathbb{R}\bullet in.wayP(x,y)=i+1)\ )\\\ \t{1}\implies(\exists x^{\prime\prime},y^{\prime\prime}\in\mathbb{R}\bullet(in.wayP(x^{\prime\prime},y^{\prime\prime})=0)\\\ \qquad\land(out.command=move(x^{\prime\prime},y^{\prime\prime})\ )\ )\end{array}$
Table 4: A summary of the Agent node’s inputs, outputs, assumptions, and
guarantees.

###  4.4 Step 4a: Heterogeneous Verification

This section describes our verification of the four nodes in our remote
inspection case study. Each node presents its own verification challenges, and
we have chosen a suitable approach to verify that each node obeys its
contract. As mentioned in §3.5, the link between the contracts and the
verification steps is _not_ formal. The information in the contracts informs
the verification steps, enables the use of either formal or non-formal methods
as best suits the node being verified.

Radiation Sensor
---
Input | Text |  The radiation value from the sensors, and the command from the Agent
FOL |  $r:\mathbb{R},command:CommandSet$
Output | Text |  Radiation Status and if this waypoint has been inspected or not
FOL |  $radiationStatus:RadStat,\quad inspected:InspectedType$
Assume | Text |  The radiation reading is less than or equal to 0
FOL |  $0\leq in.r$
Guarantees | Text |  If the command received was to inspect waypoint $i$, then eventually waypoint $i$ will be inspected; and the radiation at waypoint $i$ will be categorised as either green, orange, or red
FOL |  $\begin{array}[]{l}\forall i\in\mathbb{N}\bullet(in.command=inspect(i))\\\ \t{1}\implies(\ (out.inspected(i)=TRUE)\\\ \t{2}\land(0\leq in.r\land in.r<120\implies\\\ \t{3}out.radiationStatus=green)\\\ \t{2}\land(120\leq in.r\land in.r<250\implies\\\ \t{3}out.radiationStatus=orange)\\\ \t{2}\land(250\leq in.r\implies\\\ \t{3}out.radiationStatus=red)\ )\end{array}$
Table 5: A summary of the Radiation Sensor node’s inputs, outputs,
assumptions, and guarantees.

####  4.4.1 Localisation Node

The Localisation node’s contract specifies that it should output a unique
position ($\exists!~{}x,y\in\mathbb{R}\ \cdot Position(x,y)$). Using code
review, we checked that noise from the sensors did not change the position
estimate if the robot has not moved. In practical terms, it might be necessary
to allow a short time-window in which the node could obtain several sensor
readings before converging on a single position estimate.

It would have been temping to verify this property experimentally, as we do
for the Navigation node (see §4.4.2). However, the 3D Gazebo simulation of the
nuclear waste store does not simulate noisy sensors (i.e., in any given
position the value returned by the simulated sensors was deterministic).
Therefore, the position estimates do not change and while we could have
verified this, it would not necessarily have told us anything useful.

Code review was chosen because of the previously mentioned limitations of the
simulation and because the Localisation node relies on well-used ROS
libraries. We inspected the code in the Localisation node and observed that
the message specification for the node could only return one position at a
time.

While a code review was enough for the purposes of this paper, stronger
demonstrations may be needed for (e.g.) regulatory approval. For example, the
performance of the Localisation node could be tested on a physical robot
operating in a safe, test environment. We could specify a time window, after
which a position estimate should have converged to a single value (or a set of
values all within acceptable bounds of each other) and then test, using a
number of routes around the mapped space, that this behaviour occurred.

####  4.4.2 Navigation Node

The Navigation node’s contract specifies that if there was a command to move
to a position $(x,y)$ and the estimated current position of the rover is
$(x,y)$, then the rover has successfully arrived at its destination. We
verified this experimentally in simulations.

Our verification used the 3D Gazebo simulation of the nuclear waste store as
our test environment, and we created an autonomous agent that would take a
random location within the waste store, navigate to that location and stop. We
were then able to compare the goal location with the robot’s actual position
within the store, as reported by Gazebo.

The random location was generated as an action available to the agent in the
Java environment that linked it to ROS. This used Java’s built-in random
number generation to select an $x$ and a $y$ coordinate within the the waste
store map — random coordinates were regenerated if the original pair were in
some inaccessible location, such as one of the tanks or pillars.

In total, we ran 47 experiments. On average the final location of the agent
was 21.4cm away from the goal location with a standard deviation of 4mm. The
worst result was a final position 43cm away from the goal location and the
best result was 8cm from the goal location. The small standard deviation here
implies that the simulated Jackal nearly always ends up approximately 21cm
away from its goal location. From a verification perspective, for this
component to meet its contract we must decide whether a 21cm error counts as
having “arrived at its destination”. If this is within tolerance then the
component has met its contract, if it is not then the component has not. In
our case we had specifically configured movebase to have a 25cm tolerance for
the controller in the $x$ and $y$ coordinates when achieving a goal, and so we
can confirm that the node meets its contract.

#### Other Verification Approaches to Localisation, Mapping and Navigation

Robotic systems often contain a module for Simultaneous Localisation and
Mapping (SLAM), which can be targeted by specific verification techniques [59,
60]. Given an estimate $x$ (i.e., a solution returned by a state-of-the art
iterative solver), the verification approach evaluates whether $x$ corresponds
to a global optimum of a cost function $f(x)$. If the answer is positive, then
the estimate can be trusted; if the answer is negative, then some recovery
technique needs to be performed, because the estimate is not accurate and it
is not safe to use. Moreover, this verification technique can be integrated
seamlessly in standard SLAM pipelines, and provides a sanity check for the
solution returned by standard iterative solvers. In [61] an improved extension
builds upon the work from [59, 60] and introduces a novel formulation leading
to a higher efficiency, reducing verification times by up to 50 times. SLAM
relies on nonlinear iterative optimisation methods that in practice perform
both accurately and efficiently. However, due to the non-convexity of the
problem, the obtained solutions come with no guarantee of global optimality
and may get stuck in local minima.

Other approaches targeting SLAM systems include [62, 63], which are more
experimental works that focus more on testing rather than verification of
SLAM. Also, in [64], a mathematical model is developed for SLAM verification
and for physical model operation in the environment.

Our Localisation and Navigation nodes combine a SLAM capability with a
navigation capability, without an explicit SLAM module so these approaches
were not appropriate here.

####  4.4.3 Agent Node

The Agent node makes the high-level decisions for the robot. It is implemented
in the Gwendolen [65] agent programming language and we use the agent-program
model checker Agent Java PathFinder (AJPF) [66] to verify its decisions. AJPF
is an extension of Java PathFinder (JPF) [67] that enables formal verification
of Belief-Desire-Intention (BDI) [68] agent programs by providing a property
specification language that extends LTL with BDI constructs.

In the BDI model, agents use their beliefs (information that the agent
believes about the world) and desires (a goal state that the agent wants to
achieve) to select an intention for execution. To verify that the Agent node
obeys its contract, we encode its guarantees into the property specification
language for AJPF and check that the agent program meets these specifications.

The main parts of the Gwendolen code for the Agent121212The specification is
available in the Zenodo repository: https://doi.org/10.5281/zenodo.6941344
Accessed: 03/11/2023 are shown in Listing 1. The agent starts with a list of
static beliefs, such as _location_coordinate_ that takes as parameters a
location’s numerical identifier (Location variable), name, and its map
coordinates; and _next_location_ , with two location identifiers as
parameters, where the second parameter is the next location to visit after the
first parameter.

⬇

1+!inspect(Location) : { ~B danger_red, ~B danger_orange, ~B going(0),

2 B location_coordinate(Location,LocationName,X,Y,Z) }

3 <- +going(Location), move(X,Y,Z);

4

5+movebase_result(Id,3) : { B going(L1), B next_location(L1, L2) }

6 <- -going(L1), inspect, +!inspect(L2);

7+movebase_result(Id,3) : { B going(0) }

8 <- print("Decontamination"), do_nothing;

9+movebase_result(Id,2) : { B going(Location) }

10 <- print("Failure");

11

12+danger_red : { ~B going(0), B location_coordinate(0,door,X,Y,Z) }

13 <- +going(0), move(X,Y,Z);

14+danger_orange : { ~B going(0), B location_coordinate(0,door,X,Y,Z) }

15 <- +going(0), move(X,Y,Z);

Listing 1: Partial code of the Gwendolen agent.

The inspect(Location) plan (line 1) is triggered by the addition of the goal
inspect. When the system starts, the Agent begins with a goal to inspect
location 1. The guard (e.g., context or pre-conditions) of the plan is
expressed inside the curly brackets. Here, the guard is that the Agent does
not have the beliefs danger_red, danger_orange, or going(0); where the first
two beliefs indicate that there is radiation in the current location, and the
latter is a bookkeeping belief used to track the location that the robot is
moving towards (0 indicates the entrance of the nuclear waste store, which is
also the decontamination zone). The last belief,
location_coordinate(Location,LocationName,X,Y,Z), is a query to the belief
base which will use the Location value (obtained from calling the plan, e.g.,
1 when the system starts) to match with its respective belief in the belief
base and in turn unify the remaining open variables (e.g., search for a
location_coordinate belief where the Location term is 1, and then unify the
remaining open variables with the values from the matched belief). If the
guard test is successful, then the plan body (preceded by <-) is selected for
execution. The plan body is executed sequentially, in this case first the
bookkeeping belief going is added (+) and then the action move is called with
the coordinates of the desired location.

The second plan, movebase_result(Id,Result) on line 5, has three variations.
All of them are triggered by adding the movebase_result belief, which reports
that the robot’s movement (controlled by the move base library) is complete,
with the second parameter indicating either success (value $3$) or failure
(value $2$). The first variation (lines 5–6) is the main plan, which tests
where the rover was going before the action succeeded (going(L1)) and where
the next location is, and then removes the outdated bookkeeping belief,
performs the inspect action, and then adds the goal to inspect the next
location. The second variation (line 7) is for when the robot is moving to the
decontamination and should thus not take any additional actions. The third
variation (line 9) is for when a move action fails, in which case we simply
log that it has failed.

Finally, the third (line 12) and fourth plans (line 14) are triggered by the
addition of the beliefs danger_red or danger_orange, respectively. In both
cases we test that we are not yet heading to the entrance (going(0)) and get
its coordinates from the belief base. Then, if the test succeeds, we add the
bookkeeping belief and send the move action for execution (this is published
in a ROS topic that is subscribed to by a move base node).

Using AJPF, we prove that the following properties hold131313Note that
predicates specified in formal properties in AJPF must be ground, thus we
present this limited set of properties as representatives, but the complete
set includes all viable permutations of waypoints that we want to prove..
Properties $\varphi_{1}$ to $\varphi_{3}$ map to the Agent’s contract, shown
in Listing LABEL:list:CS1AgentRCL, and $\varphi_{4}$ is an additional property
that we are able to verify because at this stage of the system’s development
we know the details of its implementation.

$\begin{array}[]{l}\varphi_{1}=\Box((\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(4)\land\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,movebase\\_result(\\_,3)\land\\\
\qquad\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_red\land\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_orange\land\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(0))\\\
\qquad\Rightarrow\lozenge G_{\texttt{jackal}}inspect(5))\\\ \end{array}$

Property $\varphi_{1}$ deals with the Agent’s first guarantee (lines 15–18 in
Listing LABEL:list:CS1AgentRCL), where it is always the case that if the agent
believes it is going to waypoint 4 and the result of the movement was
successful and there is no danger of radiation nor the robot is moving to the
decontamination waypoint, then eventually the agent will have the goal to
inspect waypoint 5 (the next waypoint on the list). The goal to inspect a
waypoint includes both movement and inspect actions.

$\begin{array}[]{l}\varphi_{2}=\Box((\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(4)\land\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,movebase\\_result(\\_,3)\land\\\
\qquad\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_red\land\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_orange\land\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(0))\\\
\qquad\Rightarrow\lozenge D_{\texttt{jackal}}inspect)\par\end{array}$

Property $\varphi_{2}$ corresponds to the second guarantee (Lines 20–21 in
Listing LABEL:list:CS1AgentRCL), and it is the same as $\varphi_{1}$ up to the
implication, but in this case it implies that eventually the agent will
execute the inspect action.

$\begin{array}[]{l}\varphi_{3}=\Box(\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_red\lor\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_orange\Rightarrow\lozenge\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(0))\\\
\end{array}$

Property $\varphi_{3}$ covers the third guarantee (lines 23–25 in Listing
LABEL:list:CS1AgentRCL), that is, it is always the case that if the agent
believes the radiation level to be either red or orange, then it should
eventually believe that it is moving to the decontamination zone (waypoint 0).

$\begin{array}[]{l}\varphi_{4}=\Box(G_{\texttt{jackal}}inspect(4)\land(\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_red\\\
\qquad\land\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,danger\\_orange\land\lnot\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(0))\Rightarrow\lozenge\mathrm{{\mathcal{B}}}_{\texttt{jackal}}\,going(4))\par\end{array}$

Property $\varphi_{4}$ is an additional property that was identified while
implementing the agent; it is not part of the contract, but has been added to
address an additional lower-level requirement. It says that it is always the
case that if the agent has a goal to inspect waypoint 4 and there is no danger
of radiation nor the robot is moving to the decontamination waypoint, then
eventually the agent believes that it is going to waypoint 4. This additional
property was added to make sure that whenever an agent has the goal to inspect
a waypoint, the corresponding belief that the agent has started moving to it
has also been added.

####  4.4.4 Radiation Sensor Node

The Radiation Sensor node interprets information from the (simulated)
radiation sensor, categorising the values into either green (low), orange
(medium), or red (high). We modelled the behaviour of the Radiation Sensor as
a simple program in a Hoare Logic-style language [69] and proved properties
corresponding to the node’s guarantee by hand.

⬇

1input := radiation_at(i)

2IF (input < 120) THEN

3 output := green

4ELSE

5 IF (input < 250) THEN

6 output := orange

7 ELSE

8 output := red

Listing 2: Program for the radiation sensor node.

The Radiation Sensor node’s contract assumes that the measured radiation is
$0$ or positive. Its guarantee specifies that if the node is asked to inspect
waypoint $i$ (command = inspect(i)) then:

  1. 1.

the proposition $inspected(i)$ becomes true, $inspected(i)=TRUE$;

  2. 2.

low-level radiation is categorised as green, $0<=r<120\Rightarrow\\\
radiationStatus=green$;

  3. 3.

medium-level radiation is categorised as orange, $120<=r<250\\\ \Rightarrow
radiationStatus=orange$; and,

  4. 4.

high-level radiation is categorised as red, $250<=r\Rightarrow
radiationStatus\\\ =red$.

We proved these four properties by hand using Hoare Logic. If P is our program
from Listing 2 then:

  1. 1.

$\\{\top\\}$ P$\\{input=radiation\\_at(i)\\}$ – The input to the node is
always the radiation level at $i$. This corresponds to the requirement that
$inspected(i)=TRUE$ in the contract.

  2. 2.

$\\{radiation\\_at(i)<120\\}$ P$\\{output=green\\}$ – if the radiation level
at $i$ is less than 120 then, after execution of the program $output$ is
green.

  3. 3.

$\\{120\leq radiation\\_at(i)<250\\}$ P$\\{output=orange\\}$ – if the
radiation level at $i$ is between 120 and 250 then, after execution of the
program $output$ is orange.

  4. 4.

$\\{radiation\\_at(i)\geq 250\\}$ P$\\{output=red\\}$ – if the radiation level
at $i$ is greater than 250 then, after execution of the program $output$ is
red.

We show the proof for property (2) in Fig. 3. The other proofs follow a
similar pattern, and can be found in B.

⬇

1$\\{radiation\\_at(i)<120\\}$

2input := radiation_at(i)

3$\\{input<120\\}$ - Assignment Axiom

4IF (input < 120) THEN

5 $\\{input\ <\ 120\&\ input\ <\ 120\\}$

6 $\\{input\ <\ 120\ \&\ green\ =\ green\\}$ - strengthening

7 output := green

8 $\\{input\ <\ 120\ \&\ output\ =\ green\\}$ - Assignment Axiom

9 $\\{output\ =\ green\\}$ - weakening

10ELSE

11 $\\{input\ <\ 120\ \&\ input\ >=120\\}$

12 $\\{FALSE\\}$ - strengthening

13IF (input < 250) THEN

14 $\\{FALSE\ \&\ input<250\\}$

15 $\\{FALSE\\}$ - strengthening

16 output := orange

17 $\\{FALSE\\}$ - Assignment axiom

18 ELSE

19 $\\{FALSE\ \&\ input\ >=\ 250\\}$

20 $\\{FALSE\\}$ - strengthening

21 output := red

22 $\\{FALSE\\}$ - Assignment axiom

23 $\\{FALSE\\}$ - Conditional Rule

24 $\\{output\ =\ green\\}$ - weakening

25$\\{output\ =\ green\\}$ - Conditional Rule

Listing 3: Hoare Logic Proof that
$\\{radiation\\_at(i)<120\\}$P$\\{output=green\\}$. The program is denoted by
bold text, and the proof steps are indicated by $\\{braces\\}$ .

###  4.5 Step 4b: Automatic Synthesis of Runtime Monitors

This step takes the RCL contracts from Step 2 (§4.2) and synthesises RML
monitors that are compatible with the ROSMonitoring framework [55]. As
mentioned in §3.3, our tool Vanda parses the RCL contracts, and then
automatically generates the monitors and ROSMonitoring configuration files.
Vanda uses a contract translator to produce the configuration file and
structure of each monitor, and calls a FOL translator to translate each
guarantee.

Listing LABEL:list:agentRML shows the RML that was automatically generated
from the RCL contract in Listing LABEL:list:CS1AgentRCL. Lines 1–6 contain the
event types corresponding to the contract’s topics, while on lines 8–12 we
have the RML terms for the contract’s guarantees. These terms are obtained
through the process shown in §3.6. RML offers a Prolog-like notation, where
variables that are not of interest can be replaced with the _ symbol. This is
interpreted by RML as a wildcard variable, which can be assigned to any value
with no restrictions.

To aid the reader’s understanding of this translation step, we show in more
detail how a specific part of this RML specification has been generated. The
approach is described in § 3.6, and the same reasoning is applied to the
translation of the other contracts.

⬇

1node agent{

2…

3topics(

4gazebo_radiation_plugins/Command command matches(out.command),

5gazebo_radiation_plugins/Inspection inspected matches(in.inspected),

6gazebo_radiation_plugins/At at matches(in.at),

7int16 wayP matches(in.wayP),

8string radiationStatus matches(in.radiationStatus)

9)

10…

11guarantee(forall(x’, y’ in REAL, i in NATURAL | in.at(x’, y’) == TRUE and in.wayP(x’, y’) == i and in.inspected(i) == FALSE -> out.command == inspect(i) ))

12…

13}

Listing LABEL:list:CS1AgentRCLSnippet shows a snippet of Listing
LABEL:list:CS1AgentRCL that contains only one of the Agent node’s guarantees.
The guarantee in Listing LABEL:list:CS1AgentRCLSnippet is translated into the
RML term t2 in Listing LABEL:list:agentRML using the $(guarantee)$ rule in
Figure 4.

The body of the guarantee consists of a universal quantifier (forall) that
contains an implication (->). First, we use the $(implies)$ rule in Figure 4
to translate the implication; $(implies)$ negates the left operand and puts it
in disjunction with the right operand. The left operand is: in.at(x’, y’) ==
TRUE and in.wayP(x’, y’) == i and in.inspected(i) == FALSE, which produces the
following RML specification:

($\lnot$at(x, y) $\lor$ $\lnot$wayP(x, y, i) $\lor$ inspected(i))

. Note, that the RML is negated because (a -> b) = ($\lnot$a or b). Then, the
right operand in.command == inspect(i) is directly mapped into RML as:
command(inspect, i). This follows from the $(equals)$ rule in Figure 4, which
maps the command into its corresponding event type and adds it to the set of
event types.

⬇

1at(x, y) matches { topic: ’gazebo_radiation_plugins/At’, posX: x, posY:y };

2wayP(x, y, i) matches { topic: ’gazebo_radiation_plugins/WayP’, posX: x,
posY: y, id: i};

3radiationStatus(Lvl) matches { topic: ’gazebo_radiation_plugins/RadStat’,
level: Lvl };

4command(Cmd, x, y) matches { topic:’gazebo_radiation_plugins/Command’,
command: Cmd, posX: x, posY: y };

5command(Cmd, i) matches { topic:’gazebo_radiation_plugins/Command’, command:
Cmd, id: i };

6inspected(i) matches { topic: ’gazebo_radiation_plugins/Inspection’, id: i };

7

8t1 = {let x1, y1, i; (((*$\lnot$*)at(x1,y1) (*$\lor$*) (*$\lnot$*)wayP(x1,
y1, _) (*$\lor$*) (*$\lnot$*)radiationStatus(green))) (*$\lor$*) {let x2,y2;
(wayP(x2, y2, i+1) (*$\land$*) command(move, x2, y2))}}*;

9

10t2 = {let x, y, i; ((*$\lnot$*)at(x, y) (*$\lor$*) (*$\lnot$*)wayP(x, y, i)
(*$\lor$*) inspected(i)) (*$\lor$*) (command(inspect, i))}*;

11

12t3 = {(radiationStatus(green) (*$\lor$*) {let x, y; wayP(x, y, 0)
(*$\land$*) command(move, x, y))})}*;

Next, the variables derived from the universal quantifier are added to the RML
specification. Thus, we obtain {let x, y, i; t}, where t is the previously
created RML specification (the one denoting the implication). Through this
quantification, in RML we can generalise t over the set of variables { x,y,i
}. Finally, since the guarantee ranges over all possible instantiations for
the variables, an * is added at the end of RML specification (as specified in
the $(guarantee)$ rule in Fig. 4). This operator, as in regular expressions,
requires the RML specification to be matched multiple times. As previously
mentioned, the same reasoning is applied to the other guarantees in Listing
LABEL:list:CS1AgentRCL.

Once the RML specification (Listing LABEL:list:agentRML) and the configuration
file (Listing 4) have been generated, the RV step can be applied, as
previously presented in Fig. 3. Hence, the RML specification can be used to
synthesise an oracle, which will then be queried at runtime by the
corresponding ROS monitors (automatically synthesised from configuration
files).

⬇

1monitors:

2- monitor:

3 id: monitor_agent

4 log: ./agent_log.txt

5 topics:

6 - {action: log, name: gazebo_radiation_plugins/Command, type:
gazebo_radiation_plugins.msg.Command}

7 - {action: log, name: gazebo_radiation_plugins/Inspection, type:
gazebo_radiation_plugins.msg.Inspection}

8 - {action: log, name: gazebo_radiation_plugins/At, type:
gazebo_radiation_plugins.msg.At}

9 - {action: log, name: gazebo_radiation_plugins/WayP, type:
gazebo_radiation_plugins.msg.WayP}

10 - {action: log, name: gazebo_radiation_plugins/RadStat, type:
gazebo_radiation_plugins.msg.RadStat}

Listing 4: The monitor configuration file for the Agent node.

The configuration file automatically generated for ROSMonitoring is shown in
Listing 4. This file is used by ROSMonitoring to generate the Agent node’s
monitor. Lines 3 & 4 show the agent monitor’s identifier and the location
where its log files should be stored. The monitor also requires the list of
topics to subscribe to (lines 5–10) to observe the events at runtime. These
topics are obtained from lines 7–12 in Listing LABEL:list:CS1AgentRCL.

As previously mentioned, ROSMonitoring automatically synthesises runtime
monitors as additional nodes in the ROS program. The monitor nodes that
ROSMonitoring synthesises subscribe to the topics of interest listed in the
configuration file (derived from the RCL specification). After that, they
collect the messages published on those topics and perform the runtime
analysis of the RML specification. If a monitor observes a violation of an RML
specification, it reports the violation to the entire system by publishing a
specific error message. This information can be used by the system to promptly
react and possibly recover from the erroneous behaviour.

An additional step of instrumenting the implementation of the case study was
necessary to fully capture the execution traces that the ROSMonitoring
monitors were expecting to observe. For example, this process of
instrumentation included publishing information that was kept within the
Agent, such as beliefs about which waypoint the robot is at, to a ROS topic.
This allowed ROSMonitoring to then observe such information.

The overheads caused by using RML monitors to perform RV of our contracts are
slight. We conducted an analysis of the overhead introduced by the presence of
monitors in our case study. Following a similar approach to [55], first we
timed our system patrolling its simulated environment without monitors to
establish a baseline, then timed the system with the monitors. Fig. 8(a) shows
the time required for the robot to visit all the waypoints and return to the
exit, averaged over 30 runs. The baseline, without monitors, is shown in blue,
while the scenario with ROSMonitoring’s monitors performing runtime
verification is shown in red. As it can be observed, the overhead introduced
by the monitors is negligible. Fig. 8(b) provides a more detailed view,
showing the percentage overhead at waypoint (relative to the baseline
execution without the monitors). Further experiments on the overhead of
ROSMonitoring are presented in [55], where the overhead of RML monitors in
ROSMonitoring was analysed. This analysis empirically demonstrated that RML
monitors were introducing almost no overhead to the robotic system, as long as
ROSMonitoring was used to detect failures and not to enforce correctness.

(a) The y-axis indicates the time at which the rover completes their visit.

(b) The y-axis indicates the percentage increase with respect to the baseline.

Figure 8: Overhead experiment results in the remote inspection case study. The
x-axis represents the visited waypoints. BASE is WP0, the door location. When
reaching WP7 the rover detects dangerous radiation and then decides to move to
the door for decontamination.

##  5 Beyond the Case Study

This section goes beyond our case study, to demonstrate other features of our
framework, In §5.1, we provide a worked example of how our framework enables
the implementation of one node to be swapped with another, as long as the
replacement node satisfies the specification. In §5.2, we discuss how the
verification step for a node can check more properties than its guarantee
specifies – which can be seen in the verification step for the Agent node
(§4.4.3), but here we provide a more in-depth example. Finally, §5.3 explores
how our approach to composing the node specifications can be applied to
systems that are not implemented in ROS. But first, we discuss the general
utility of our approach, beyond what is presented in §4. The analysis of our
approaches wider applicability, and the two formal models in this chapter are
available from the Zenodo repository that accompanies this paper:
https://doi.org/10.5281/zenodo.6941344.

While we have shown the applicability of the approach to our case study, there
remains a question of whether it is useful in general for the verification of
robotic systems. As a step towards assessing this, we examined fifty-six
papers containing verifications of autonomous systems identified in our
previous survey paper [10]. For each paper, we assessed if our approach would
be applicable to the system it describes. We identified 20 papers with a case
study to which our general approach would be applicable. Three of these,
specifically involved the verification of ROS nodes. Of these 20 papers, nine
involved the verification of a component within a larger autonomous system and
10 involved the system-level verification of a modular system (the remaining
one applied runtime verification to a modular system).

Of the systems where we deemed our approach to be inapplicable, the majority
(20 in total) involved the verification of distributed or swarm systems where
an unspecified number of similar components act to produce system level
behaviour and, at present, our formal system is not equipped to work with such
architectures. Four examples involved the verification of monolithic systems.
In general, the behaviour of these monolithic systems was comparatively simple
when compared to modular systems (typically these were hybrid control systems
where the verification focused on obstacle avoidance behaviour). We identified
nine verification attempts as borderline. These involved fixed-size teams of
independent systems – often individual robots but sometimes independent,
communicating systems within a smart home or similar environment. Our approach
should be extensible to such systems by viewing sub-systems as components in a
hierarchical fashion. One paper contained an analysis of a failed verification
attempt – we also classified this as borderline.

###  5.1 Compositionality enables Interchangeability

One of the advantages of our approach is that we can swap a node’s
implementation with another (similar) implementation, which may be modelled
and verified using different specification languages and verification tools to
the original node, as long as the new implementation conforms to the FOL
contract. For example, instead of using a BDI agent (as we do in §4) we might
choose a simpler way of making the systems’ executive decisions that still
satisfies $\mathcal{G}_{A}(\overline{o_{A}})$.

To demonstrate the modularity of our approach, this section describes a re-
specification and verification of the Agent (§4.4.3) in Dafny [70], which is a
programming language enriched with specification constructs – for example:
pre-/post-conditions and loop invariants. This enables the functional
correctness of Dafny programs to be statically verified, by translating them
into the intermediate verification language Boogie [71] and using the theorem
prover Z3 [72] to automatically discharge the proof obligations for the
specification statements in the program.

The idea here is that instead of using a BDI program, the decision-making
algorithm(s) will be implemented in a general-purpose programming language,
for example C++ or Python for compatibility with ROS. So we use Dafny to
implement and verify the algorithms that the new decision-making component
will execute. Our prior work demonstrates that the correspondence between
Dafny and general-purpose languages, such as Python, makes it relatively
straightforward to translate between formal models and implemented code [43].

Listing 5 shows our Dafny model, in which the Agent method (line 5) provides
an alternative implementation of the agent’s behaviour to the BDI version that
was presented in §4.4.3. Importantly, the Dafny implementation follows the
specification in its contract (Table 4).

In Dafny, pre-conditions (assumptions) are indicated by the requires keyword.
Lines 6–9 of Listing 5 show the Agent method’s pre-conditions, taken from its
contract. One small change is that where the Agent’s contract has an
assumption that the radiation status will be either red, orange, or green; our
Dafny version encodes this constraint as the RadiationLevel datatype (line 3)
using the radiation values, and using this in the parameters (for radstat) of
the Agent method. Importantly, if the Agent method is called by another
method, then the calling method’s guarantees must not violate the assumptions
of the Agent method.

⬇

1datatype Action = Inspect | MoveNext

2datatype Command = Command(a$\colon$Action, w$\colon$int)

3datatype RadiationLevel = red | orange | green

4

5method Agent(waypoints$\colon$ seq<int>, currentpos$\colon$int,
radstat$\colon$RadiationLevel, wheelsready$\colon$bool) returns
(actions$\colon$ seq<Command>)

6requires currentpos $\geq$ 0 $\land$ currentpos $\leq$ 12; //13 waypoints to
patrol

7requires |waypoints| $=$ 13;

8requires $\forall$ i$\colon$int $\cdot$ 0$\leq$i<|waypoints| $\Rightarrow$
waypoints[i] $=$ i;

9requires $\forall$ i$\colon$int $\cdot$ 0$\leq$i<|waypoints| $\Rightarrow$ i
in waypoints;

10ensures (wheelsready) $=$ false $\Rightarrow$ actions $=$[];//safety
check$\colon$ if the hardware is not ready then do nothing.

11ensures $\forall$ i$\colon$int $\cdot$ 0$\leq$i<|waypoints| $\Rightarrow$
(wheelsready $\land$ at(i) $\land$ inspected(i) $\land$ radstat $\neq$ red
$\land$ radstat $\neq$ orange $\Rightarrow$ $\exists$ next$\colon$int $\cdot$
0$\leq$next<|waypoints| $\land$ Command(MoveNext, next) in actions);

12ensures $\forall$ i$\colon$int $\cdot$ 0$\leq$i<|waypoints| $\Rightarrow$
(wheelsready $\land$ at(i) $\land$ (! inspected(i)) $\Rightarrow$
Command(Inspect, i) in actions);

13ensures wheelsready $\land$ (radstat $=$ red $\lor$ radstat $=$ orange)
$\Rightarrow$ Command(MoveNext, 0) in actions;

14{

15 var time, next $\coloneqq$ 0, 0;

16 var current$\coloneqq$currentpos;

17 actions $\coloneqq$ [];

18

19 if(wheelsready){

20 while(wheelsready $\land$ time <200)

21 invariant next in waypoints;

22 invariant current in waypoints;

23 invariant time > 0 $\land$ (radstat $=$ red $\lor$ radstat $=$ orange)
$\Rightarrow$ Command(MoveNext, 0) in actions $\land$ next $=$ 0;

24 invariant time > 0 $\land$ at(current) $\land$ (! inspected(current))
$\Rightarrow$ Command(Inspect, current) in actions;

25 invariant time > 0 $\land$ at(old(current)) $\land$ inspected(old(current))
$\land$ radstat $\neq$ red $\land$ radstat $\neq$ orange $\Rightarrow$
Command(MoveNext, next) in actions $\land$ current $=$ old(next);

26 {

27 if(at(current) $\land$ inspected(current) $\land$ radstat $\neq$ red
$\land$ radstat $\neq$ orange){

28 next $\coloneqq$ getnextwaypoint(current);

29 actions $\coloneqq$ actions + [Command(MoveNext, next)];

30 }

31 if(at(current) $\land$ (! inspected(current))){

32 actions $\coloneqq$ actions + [Command(Inspect, current)];

33 }

34 if(radstat $=$ red $\lor$ radstat $=$ orange){

35 next $\coloneqq$ 0;

36 actions $\coloneqq$ actions + [Command(MoveNext, next)];

37 }

38 time $\coloneqq$ time +20;

39 current $\coloneqq$ next;

40 }

41 }

42}

Listing 5: Dafny Agent

Post-conditions (guarantees) in Dafny are indicated by the ensures keyword.
Lines 10–13 of Listing 5 show the Agent method’s post-conditions, which are
more detailed than the Agent’s contract, because they also check the status of
the software controlling the rover’s wheels before instructing it to carry out
any commands. The post-condition on line 10 specifies that no actions are
assigned when the wheels are not ready141414This is an example of how our
approach allows verifiers to check additional node-level properties, which we
discuss in more detail in §5.2.. The post-conditions on lines 11–13 correspond
to the Agent’s guarantees from its contract (Table 4). For verification in
Dafny, we must include loop invariants (lines 21–25), which help the
verification tool (Z3) to prove the post-conditions. We automatically
discharged the associated proofs in Dafny with Z3 using Visual Studio Code.

Another difference between our Dafny and BDI implementations is that we had to
add a notion of time to the Dafny model (the time variable is declared on line
15 and updated on line 38) to be able to prove loop termination. Dafny is
primarily concerned with program safety, so termination is necessary for
complete verification of Dafny programs.

This Dafny program verifies the decision-making algorithm, using a language
that is closer to those in which ROS nodes can be implemented. Once the Dafny
program has been verified against the Agent contract, it can be carefully
reimplemented as a ROS node. The Dafny Agent can also be used with our
calculus (§3.4) because it preserves the contract’s assumptions and
guarantees. Not only does this allow the user to develop multiple models (and
potentially implementations) of the same node, it also facilitates the use of
predefined or library functions that have been verified previously and also
meet the required contracts. This can potentially streamline the verification
step by supporting the use of previously verified robotic system nodes.

###  5.2 Verifying Additional Node-Level Properties

This section discusses how the verification of a node can check more
properties than are specified in its contract. The contract may under-specify
its guarantee, for example because of implementation-specific details that are
not known when the contract is written, or because the contract language is
too abstract to express all of a node’s verification conditions. Either way,
our approach allows the verification of a node to go further that what its
contract guarantees. This can be seen in the verification of the Agent node
(§4.4.3), where property $\phi 4$ is not part of the node’s contract but is a
lower-level property identified during the node’s implementation.

As a more in-depth example, we briefly describe the contracts and verification
for part of the example from our previous work [19]. In this system, a
simulation of USA’s NASA Curiosity rover moves between waypoints on a map,
each waypoint represents an interesting location at which the rover should
collect some data. The rover has an arm, with data-collection instruments on;
and a mast, with a camera. The rover’s control software picks the next
waypoint, avoiding a waypoint if the radiation is too high, and retracting
(closing) the mast and arm if a waypoint is too windy.

The rover’s arm, mast, and wheels are all controlled using pairs of ROS nodes
that implement the Action library151515ROS Action Library:
http://wiki.ros.org/actionlib Accessed: 03/11/2023 to interface between the
rover’s software and hardware. Each client node accepts instructions from the
rover’s control software, which it then sends to its corresponding server node
as a goal (a task to complete). While this is a relatively simple protocol, it
is crucial to the Robot’s correct operation.

⬇

1node ArmClient

2{

3inputs( arm_down $\colon$ BOOL, arm_result $\colon$ BOOL )

4

5outputs( arm_down $\colon$ BOOL, arm_result $\colon$ BOOL )

6

7assume( TRUE )

8

9guarantee( in.arm_down = out.arm_down )

10

11guarantee( out.arm_result = in.arm_result )

12}

Here, we focus on the contracts and verification of the software nodes
controlling the rover’s arm. The arm’s RCL contracts were developed for this
work, and we compare them with the verification approach used in the previous
work [19]. The arm on the Curiosity rover can either be down (extended), so
that the instruments it holds can be used to inspect the surface of Mars; or
up (retracted), to protect the arm and instruments while the rover is moving.
The RCL contracts are written at a high-level, without including details
specific to the library that the example system implements. The verification
conditions capture more of Action library’s low-level behaviour.

The contract for the ArmClient (Listing LABEL:list:armClient) shows that it
guarantees (lines 9 and 11) two abstract properties. First, that the position
of the arm (i.e is arm_down TRUE or FALSE) that it receives on the input
stream is the same as the position that it passes to the ArmServer
(in.arm_down = out.arm_down). Second, that the result sent back to the system,
on the output stream, matches the result (TRUE if the action has completed, or
FALSE otherwise) it has received from the ArmServer (out.arm_result =
in.arm_result). These conditions ensure that an instruction from the rover’s
control software is correctly passed to the server (for execution) and the
result is correctly returned to the control software.

The contract for the ArmServer (Listing LABEL:list:armServer) shows its
guarantee (line 9); that when it receives an instruction to move the arm, it
produces a result of TRUE and sends it to the ArmClient on the output stream.
This states that the instruction to open or close the arm is performed
successfully, and ensures that the result is returned to the client (which
will return the result to the rover’s control software).

The ArmClient and the ArmServer were modelled and verified as part of the work
described in [19]. The modelling and verification conditions were both based
on the the ROS program in that work, and the documentation for the Action
library. We checked the following three verification conditions:

  1. 1.

when a client sends a goal, it will begin execution on the correct server,

  2. 2.

when a client sends a goal, eventually it receives a result from the server,
and;

  3. 3.

when the rover’s control software instructs a client node to perform an
action, the server informs the rover that it is ready and then eventually the
rover receives a result.

These conditions are lower-level than the contracts in Listings
LABEL:list:armClient and LABEL:list:armServer, so they are ‘aware’ of the
library implementing these nodes and so the conditions relate to the library’s
behaviour.

⬇

1node ArmServer

2{

3inputs( arm_down $\colon$ BOOL )

4

5outputs( arm_result $\colon$ BOOL )

6

7assume( TRUE )

8

9guarantee( out.arm_result = TRUE )

10}

Verification condition (1) maps directly to the guarantee on line 9 of Listing
LABEL:list:armClient: if we send a goal to the ArmServer, then it will be
executed on the ArmServer. The contract’s guarantee states that the arm_down
value it receives on the input stream will be passed, unaltered, to the output
stream. The ArmServer is listening to that output stream, so it will execute
the goal.

However, verification conditions (2) and (3) extend the guarantees in the two
contracts. For the ArmClient and the ArmServer, condition (2) states that if
the ArmClient sends a goal then eventually it will receive a result from the
ArmServer. Since RCL is a more abstract language, the contracts only guarantee
that the ArmClient passes arm_down and arm_result between its input and output
streams without changing the value, and that the ArmServer will eventually say
that the action was complete (arm_result = TRUE). The verification condition
includes information about the ordering of these events, and the notion that
there is some time in between them to allow for computation and the physical
movement of the arm.

Similarly, verification condition (3) contains more information about the
ordering of events than the RCL contracts capture. For the ArmClient and the
ArmServer it states that ArmClient will first receive the value of arm_down
from the rover’s control software, then the ArmServer has to signal that it is
ready to receive another goal, and eventually the rover’s control software
receives the result of executing the goal from the ArmClient. The RCL contract
is only concerned with the data moving between the two nodes, so these signals
and ordering are abstracted away from.

Some of these low-level aspects of ROS programs could be useful to include in
RCL, for example the idea of an output being triggered by an input, which
would allow contracts to specify some ordering of events. However, even
without this, RCL contracts can specify useful properties about a node, which
can be extended by that node’s individual verification. This is especially
useful when the contracts are written before the implementation details of the
system are known.

###  5.3 Towards Applying our Approach to Non-ROS Systems

So far, we have focussed on ROS systems; this section explores how our
approach can be adapted to robotic systems that do not use ROS. We use
previous work [28] as our example, in which heterogeneous verification methods
are used to verify an autonomous rover that is modelled in Simulink. The
rover’s mission is to autonomously navigate around a grid-world of known size,
visiting waypoints to collect data, recharging as necessary. This example has
similar functionality to our case study system in §4, but does not use ROS.

Fig. 9. shows the rover’s architecture in Architecture Analysis and Design
Language (AADL). This rover contains multiple connected modules, some of which
provide functionality that is more critical than others – for example the
ReasoningAgent, which is the core decision-making component of the system. To
account for this mixed-criticality, the work in [28] begins by eliciting the
system’s requirements using an approach driven by a detailed hazard analysis.

One of the system’s most important requirements is that the rover shall not
run out of battery. This particular requirement can be viewed as a system-
level contract that relies on the behaviour of multiple system components. For
example, the Battery_Interface must function correctly, ensuring that the
rover’s goal location is set to the charge station when needed; and the
ReasoningAgent must correctly select the shortest path, to conserve battery
power.

Figure 9: Architecture of autonomous rover from [28].

The work in [28] uses CoCoSim to enable the compositional verification of the
Simulink model of the system. This approach works by attaching contracts to
nodes in the system and then defining a top node where the system-level
contracts are specified. Here, compositional verification involves verifying
(by model-checking) that the node-level contracts imply the system-level
contracts.

A key point of our approach is that it can derive system-level properties from
the node-level contracts. In [28], both component-level contracts and system-
level contracts are derived from the requirements and the component-level
contracts are attached to individual system components. CoCoSim was then used
to verify that the system-level properties could be deduced from the
component-level contracts. The difference between this approach and ours is
that CoCoSim requires a system-level property against which to verify systems,
whereas we support deriving properties about a system’s behaviour for systems
built from (potentially independently developed) components.

To compare with this work and investigate how our approach performs on this
non-ROS system, we examine its component-level contracts to see if we can
derive similar system-level properties to those used in [28]. For this
example, we focus our attention specifically on the NavigationSystem shown in
Fig. 9, which is composed of a ReasoningAgent and a Battery_Interface. The
ReasoningAgent contains a Goal Reasoning Agent (GRA in Fig. 9), to select the
rover’s goal location; the ComputePlan2Charging component, which generates a
plan to the charging point; and the ComputePlan2Destination component, which
generates a plan to other destinations. The Battery_Interface contains a