Over-the-air (OTA) updates are becoming a standard practice for upgrading Cyber-Physical Systems (CPS) software, allowing software systems to be modified through a wireless network. They are beneficial in several contexts. For example, in the automotive domain, OTA updates enable manufacturers to update vehicle software without physical access. However, the considerable number of products (e.g., vehicles within the fleet) and frequent changes and updates to software components can generate many software configurations that are impossible to analyze beforehand without any automated support. This problem hampers the verification of the system’s safety. This paper proposes a contract-driven framework for reasoning about the safety of OTA updates. Our framework supports (a)contract composition, which enables reasoning about the behavior composition of different software components, and (b) verification ofcomponent substitutability, which allows checking if the software component deployed by an OTA update can replace another component without generating any safety breach.We rigorously define our framework and formally prove that if the OTA update ensures the satisfaction of its contract, the system (safety) properties are preserved. We propose an instance of our solution that targets CPS designed with Simulink®System Composer, a widely used tool for modeling the different components of the system architecture and their interaction. We propose using Simulink®Requirements Tables to express the contracts of CPS components, as they enable engineers to model the system requirements using pre/post-conditions within their Simulink®models. We implemented our solution as a software prototype that extends THEANO, a tool that enables engineers to verify the consistency and completeness of Requirements Tables. We evaluated our solution by considering the Ten Lockheed Martin Cyber-Physical Problems. We defined 20 OTA updates and effectively identified issues in 9 of them. We analyzed and fixed the problems, inspecting each unsafe OTA update to understand the causes of the safety breaches. After fixing the problems, THEANO confirmed the safety of all OTA updates. THEANO required less than a minute to analyze each OTA update, making it practical for industrial applications.

Abstract Developing robotic applications with human–robot interaction for the service sector raises a plethora of challenges. In these settings, human behavior is essentially unconstrained as they can stray from the plan in numerous ways, constituting a critical source of uncertainty for the outcome of the robotic mission. Application designers require accessible and reliable frameworks to address this issue at an early development stage. We present a model-driven framework for developing interactive service robotic scenarios, allowing designers to model the interactive scenario, estimate its outcome, deploy the application, and smoothly reconfigure it. This article extends the framework compared to previous works by introducing an analysis of the impact of human errors on the mission’s outcome. The core of the framework is a formal model of the agents at play—the humans and the robots—and the robotic mission under analysis, which is subject to statistical model checking to estimate the mission’s outcome. The formal model incorporates a formalization of different human erroneous behaviors’ phenotypes, whose likelihood can be tuned while configuring the scenario. Through scenarios inspired by the healthcare setting, the evaluation highlights how different configurations of erroneous behavior impact the verification results and guide the designer toward the mission design that best suits their needs.

With many applications across domains as diverse as logistics, healthcare, and agriculture, service robots are in increasingly high demand. Nevertheless, the designers of these robots often struggle with specifying their tasks in a way that is both human-understandable and sufficiently precise to enable automated verification and planning of robotic missions. Recent research has addressed this problem for the functional aspects of robotic missions through the use ofmission specification patterns. These patterns support the definition of robotic missions involving, for instance, the patrolling of a perimeter, the avoidance of unsafe locations within an area, or reacting to specific events. Our article introduces a catalog ofQUantitAtive RoboTic mission spEcificaTion patterns(QUARTET) that tackles the complementary and equally important challenge of specifying the reliability, performance, resource usage, and other key quantitative properties of robotic missions. Identified using a methodology that included the analysis of 73 research papers published in 17 leading software engineering and robotics venues between 2014–2021, our 22 QUARTET patterns are defined in a tool-supported domain-specific language. As such, QUARTET enables: (i) the precise definition of quantitative robotic-mission requirements and (ii) the translation of these requirements into probabilistic reward computation tree logic (PRCTL), supporting their formal verification and automated planning of robotic missions. We demonstrate the applicability of QUARTET by showing that it supports the specification of over 95% of the quantitative robotic mission requirements from a systematically selected set of recent research papers, of which 75% can be automatically translated into PRCTL for the purposes of verification through model checking and mission planning.

Robots are currently mostly found in industrial settings. In the future, a wider range of environments will benefit from their inclusion. This calls for the development of tools that allow professionals to set up dependable robotic applications in which people productively interact with robots aware of their needs. Given the co-existence of humans and robots, the precise analysis-e.g., through formal verification techniques-of properties related to aspects such as human needs and physiology is of paramount importance. In this paper, we present a formally-based, model-driven approach to design and verify scenarios involving human-robot interactions. Some of the features of our approach are tailored to the healthcare domain, from which our case studies are derived. In our approach, the designer specifies the main parameters of the mission to generate the model of the application, which includes mobile robots, the humans to be served, including some of their physiological features, and the decision-maker that orchestrates the execution. All components are modeled through hybrid automata to capture variables with complex dynamics. The model is verified through Statistical Model Checking (SMC), using the Uppaal tool, to determine the probability of success of the mission. The results are examined by the developer, who iteratively refines the design until the probability of success is satisfactory.

A crucial aspect of physical human-robot collaboration (HRC) is to maintain a safe common workspace for human operator. However, close proximity between human-robot and unpredictability of human behavior raises serious challenges in terms of safety. This article proposes a risk analysis methodology for collaborative robotic applications, which is compatible with well-known standards in the area and relies on formal verification techniques to automate the traditional risk analysis methods. In particular, the methodology relies on temporal logic-based models to describe the different possible ways in which tasks can be carried out, and on fully automated formal verification techniques to explore the corresponding state space to detect and modify the hazardous situations at early stages of system design.