Due to the critical consequences of possible failures, robot systems must be formally verified to guarantee that their behaviors are correct and safe. There is, however, a gap in terms of building safe behaviors between the formal methods and robotic communities as the latter focuses on informal design and its implementation in a manner which is accessible to robotics engineers. In this paper, we present an approach to bridge that gap which enables a tight coupling of informal robot behaviors defined in SMACH, Python state machine API, with formal models through a process of translation. A set of mapping rules, which facilitates transformation is provided and the result is utilized for formal verification of safety properties. We also discuss the current limitations of such work along with recommendations on how these might be addressed.

Unmanned Aerial Systems (UAS, typically known as drones) are useful in many application domains, such as logistics and precision farming, especially when they fly Beyond Visual Line of Sight (BVLOS). To effectively use multiple UAS for BVLOS missions, it is required to precisely plan the flight of each UAS involved in the missions, allocating the required airspace ahead of time. The dots Domain-Specific Language (DSL) can be used to plan and execute such missions but does not support the adaptation of missions when unexpected changes occur during the execution of these missions. Such dynamic replanning of missions to changing conditions is a crucial feature for the safe integration of UAS into the airspace since it allows the UAS to adapt to these changes, such as yielding to emergency response aircraft.

The behavior of a robot is typically expressed as a set of source code files written using a programming language. As for any software engineering activity, programming robotic behaviors is a complex and error-prone task. This paper propose a methodology that aims to reduce the cost of producing a reliable software describing a robotic behavior by automatically testing it.We employ a fuzz testing technique to stress software components with randomly generated data. By applying fuzz testing to a complex robotic-software, we identified errors related to the coding, the way data is handled, the logic of the robotic behavior, and the initialization of architectural components. Furthermore, a panel of experts acquainted with the analyzed behavior have highlighted the relevance and the significance of our findings. Our fuzzer operates on the SMACH and ROS frameworks and it is available under the MIT public open source license.

In a robotics context, visualizing the data scanned by a robot is crucial to understand what the robot's sensors perceive about its environment. Consequently, robotic visualizations show these values in a 3-D world, such that they can be compared with the real world. However these visualizations do not allow developers to see this data in a manner that allows it to be interpreted for program construction. As a result, these visualizations are in many cases ineffective for programming robot behaviors. To address this issue, we have built several visualizations of robot sensor data for the programming of behaviors, and we report on them here. Our visualizations focus on better revealing the hard data, which allows developers to faster understand it and consequently to faster create and adapt robot behaviors.