390 research outputs found
Model-Driven Development of Formally Verified Human-Robot Interactions
No full textService robots will operate in unconstrained environments due to the significant presence of humans. We present a model-driven framework based on formal methods to develop interactive robotic applications designed to handle the uncertainty of human behavior. Users formally model the human-robot interaction scenario, estimate the most likely outcome, and subsequently deploy the application. Collected traces constitute the data pool for an active automata learning algorithm to update the human model based on the accumulated knowledge. We validate the framework on realistic use cases from the healthcare setting
Model-Driven Development of Formally Verified Human-Robot Interactions
No full textIntroducing service robots into everyday settings entails a significant technological shift for the robotics community. Service settings are characterized by critical sources of uncertainty (mainly due to human behavior) that current software engineering techniques do not handle. This chapter introduces a model-driven framework for developing interactive service robotic scenarios, relying on formal verification to guarantee robustness with respect to unexpected runtime contingencies. Target users specify the characteristics of the scenario under analysis through a custom textual Domain-Specific Language, which is then automatically converted into a network of Stochastic Hybrid Automata. The formal model captures non-traditional physiological (e.g., physical fatigue) and behavioral aspects of the human subjects. Through Statistical Model Checking, it is possible to estimate several quality metrics: if these meet the set dependability requirements, the scenario can be deployed. Specifically, the framework allows for deployment on the field or simulation. Field-collected data are fed to a novel active automata learning algorithm, called
, to learn an updated model of human behavior. The formal analysis can then be iterated to update the scenario’s design. The overall approach has been assessed in terms of effectiveness and accuracy through realistic scenarios from the healthcare settin
Teaching Formal Methods to Software Engineers through Collaborative Learning (Short Paper)
No full textIt is common knowledge among researchers in the field that teaching formal methods can prove a challenging task. This paper reports on the approach adopted for a Master’s Degree course at Politecnico di Milano, Italy, as an attempt to reverse this trend by introducing collaborative learning activities. Students put concepts learned during theoretical lectures into practice through a hands-on group assignment. Each group develops the formal model of a Cyber-Physical System through the Uppaal tool, starting from a set of requirements provided by the instructor. After delivering the assignment, we invite students to fill an evaluation survey whose results suggest a very high satisfaction level towards the hybrid theoretical-practical approach of the course
Towards Verifiable Multi-Agent Interaction Pattern Specification
No full textSmart cyber agents play a crucial role in software-intensive systems by monitoring their physical surroundings and making impactful decisions. This paper addresses the challenge of specifying multi-Agent patterns, which include interactions with human agents in possibly safety-critical environments. To this end, we introduce the foundations of a domain-Agnostic and flexible Domain-Specific Language (DSL) called LIrAs. The language is designed to be accessible to users without programming expertise. LIrAs' semantics are mapped to Deterministic Finite-state Automata, making specifications amenable to formal verification. The DSL is exemplified through an illustrative scenario from the service robotics field
Specification, stochastic modeling and analysis of interactive service robotic applications
No full textAssistive robotic systems are quickly becoming a core technology for the service sector as they are understood capable of supporting people in need of assistance in a wide variety of tasks. This step poses a number of ethical and technological questions. The research community is wondering how service robotics can be a step forward in human care and aid, and how robotics applications can be realized in order to put the human role at the forefront. Therefore, there is a growing demand for frameworks supporting robotic application designers in a “human-aware” development process. This paper presents a model-driven framework for analyzing and developing human–robot interactive scenarios in non-industrial settings with significant sources of uncertainty. The framework's core is a formal model of the agents at play – the humans and the robot – and the robot's mission, which is then put through verification to estimate the probability of completing the mission. The model captures non-trivial features related to human behavior, specifically the unpredictability of human choices and physiological aspects tied to their state of health. To foster the framework's accessibility, we present a verification tool-agnostic Domain-Specific Language that allows designers lacking expertise in formal modeling to configure the interactive scenarios in a user-friendly manner. We compare the formal analysis outputs with results obtained by deploying benchmark scenarios in the physical environment with a real mobile robot to assess whether the formal model adheres to reality and whether the verification results are accurate. The entire development pipeline is then tested on several scenarios from the healthcare setting to assess its flexibility and effectiveness in the application design process
A Deployment Framework for Formally Verified Human-Robot Interactions
No full textIn the future, assistive robots will spread to everyday settings and regularly interact with humans. This paper introduces a deployment approach for assistive robotic applications where human-robot interaction is the main element. The deployment infrastructure hinges on a model-to-code transformation technique and a ROS-based middleware layer and enables deployment in real life or simulation in a virtual environment. The approach fits into a model-driven framework for the formal verification of interactive scenarios. At design-time, the application analyst estimates the most likely outcome of the robotic mission through Statistical Model Checking of a Stochastic Hybrid Automata network modeling the scenario. We introduce an innovative approach to convert a specific subset of Stochastic Hybrid Automata into executable code to control the robot and respond to human actions. Deploying or simulating the application allows analysts to validate the results obtained at design time or to refine the formal model based on runs in the real or the virtual scene. The methodology’s effectiveness is tested via simulation of use cases from the healthcare setting, which can significantly benefit from this kind of approach thanks to its innovative features related to human physiology and autonomous behavior
Architecting Federated Learning Systems: A Requirement-Driven Approach
No full textThe emerging Federated Learning (FL) paradigm offers significant advantages over the traditional centralized architecture of machine learning (ML) systems by reducing privacy risks and distributing computational load. However, the network topology (i.e., the number of available clients and their characteristics) has a critical impact on performance metrics. This work investigates how application-specific requirements can drive architectural choices and how such choices impact FL performance. Specifically, we present a requirement-driven reference architecture for FL applications. Using a standard benchmark, we empirically evaluate 20 architecture realizations under different boundary conditions. The effectiveness of each realization is assessed on the basis of the accuracy of the trained model and the wall clock time required to complete the training. By combining our experimental results with existing qualitative studies from the literature, we devise a guideline to help prospective users select the most suitable configuration based on their application-specific non-functional requirements
Formal Verification of Human-Robot Interaction in Healthcare Scenarios
No full textWe present a model-driven approach for the creation of formally verified scenarios involving human-robot interaction in healthcare settings. The work offers an innovative take on the application of formal methods to human modeling, as it incorporates physiology-related aspects. The model, based on the formalism of Hybrid Automata, includes a stochastic component to capture the variability of human behavior, which makes it suitable for Statistical Model Checking. The toolchain is meant to be accessible to a wide range of professional figures. Therefore, we have laid out a user-friendly representation format for the scenario, from which the full formal model is automatically generated and verified through the Uppaal tool. The outcome is an estimation of the probability of success of the mission, based on which the user can refine the model if the result is not satisfactory
Statistical Model Checking of Human-Robot Interaction Scenarios
No full textRobots are soon going to be deployed in non-industrial environments. Before society can take such a step, it is necessary to endow complex robotic systems with mechanisms that make them reliable enough to operate in situations where the human factor is predominant. This calls for the development of robotic frameworks that can soundly guarantee that a collection of properties are verified at all times during operation. While developing a mission plan, robots should take into account factors such as human physiology. In this paper, we present an example of how a robotic application that involves human interaction can be modeled through hybrid automata, and analyzed by using statistical model-checking. We exploit statistical techniques to determine the probability with which some properties are verified, thus easing the state-space explosion problem. The analysis is performed using the Uppaal tool. In addition, we used Uppaal to run simulations that allowed us to show non-trivial time dynamics that describe the behavior of the real system, including human-related variables. Overall, this process allows developers to gain useful insights into their application and to make decisions about how to improve it to balance efficiency and user satisfaction
Model-driven Risk Analysis for the Design of Safe Collaborative Robotic Applications
No full textIn human-robot collaboration (HRC), humans and robots share the same workspace while executing hybrid tasks. Their close proximity imposes higher possibility of contacts that could potentially be dangerous. Hence, physical safety and risk analysis become of utmost importance during system design.In this paper, we propose a tool-supported interactive technique that facilitates the design of safe HRC systems for designers by performing iterative risk analysis and suggesting risk reduction measures (RRMs) to mitigate unsafe physical contacts
- …
