Introduction

We present a development process for dependable robotic architectures that is settled on the concepts of skills. These skills, grouped into skillsets, are on one side an abstraction of the functional architecture of robotic systems, and therefore give to the decision layer a high-level description of nominal executions and failure modes of the system, necessary to define higher level behaviors. On the other side, skills can act as controllers of the functional layer, by orchestrating the use of sensors/processing/actuators while satisfying properties. In the development process proposed, the central element is the skillset. The objective of this development process is to define the skill-layer of an autonomous robot, to help the development by generating components that manage the skills execution, and to propose verification and analysis tools that make the resulting architecture trustworthy in its management of failure conditions.

The first step of the process consists in defining the skillsets of our robotic system. Skillsets are mainly composed of resources and skills, both formally specified. A Domain Specific Language (RobotLanguage) then allows to specialize these resources and skills for a specific system.

The next step of the process is to verify the correctness of the skillset models specified by the developer. The model written using the DSL and the semantics of skillsets are translated into a Satisfaction Modulo Theory (SMT) problem, on which the solver Z3 is applied to check for inconsistencies. In case some inconsistencies are raised, the general process calls for improving the skillset model to avoid inconsistent behaviors.

Once a correct model of a skillset is designed, the next step of the development process is to generate an execution managing component. This component, implements the execution semantics of the skills. It also provides a standardized interface to trigger skill execution from a decision layer. Finally, the link with the functional layer must be implemented by the user as a specific C++ class, that extends the general skillset semantics. The part of the skillset manager that corresponds to a system specific code is called the skillset implementation.

The resulting skillset manager takes the form of a ROS2 node, managing the execution of the skillset according to its semantics, making the link with the functional layer, and providing an API to be controllable from the decision layer.