Daniele E. Domenichelli

Michele Colledanchise, Giuseppe Cicala, Daniele E. Domenichelli et al.

In this paper, we present a toolchain to design, execute, and verify robot behaviors. The toolchain follows the guidelines defined by the EU H2020 project RobMoSys and encodes the robot deliberation as a Behavior Tree (BT), a directed tree where the internal nodes model behavior composition and leaf nodes model action or measurement operations. Such leaf nodes take the form of a statechart (SC), which runs in separate threads, whose states perform basic arithmetic operations and send commands to the robot. The toolchain provides the ability to define a runtime monitor for a given system specification that warns the user whenever a given specification is violated. We validated the toolchain in a simulated experiment that we made reproducible in an OS-virtualization environment.

Michele Colledanchise, Giuseppe Cicala, Daniele E. Domenichelli et al.

In this paper, we enable automated property verification of deliberative components in robot control architectures. We focus on formalizing the execution context of Behavior Trees (BTs) to provide a scalable, yet formally grounded, methodology to enable runtime verification and prevent unexpected robot behaviors. To this end, we consider a message-passing model that accommodates both synchronous and asynchronous composition of parallel components, in which BTs and other components execute and interact according to the communication patterns commonly adopted in robotic software architectures. We introduce a formal property specification language to encode requirements and build runtime monitors. We performed a set of experiments, both on simulations and on the real robot, demonstrating the feasibility of our approach in a realistic application and its integration in a typical robot software architecture. We also provide an OS-level virtualization environment to reproduce the experiments in the simulated scenario.

Ali Paikan, Daniele Domenichelli, Lorenzo Natale

Real-Time communication are important in all those distributed applications where timing constraints on data proccessing and task executation play a fundamental role. Standards-base software engineering does not yet specify how real-time properties should be integrated into a publish/subscribe middleware. This article describes an approach for integration of priority quality of service in a publish/subscribe middleware. The approach simply leverages the operating system functionalities to provide a framework where specific communication channels can be prioritized at run-time. The quality of service is implemented in YARP (Yet Another Robot Platform) framework and the primarily results of performance tests are presented.