Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

Abstract This paper proposes an approach to pattern-based modeling and Uppaal-based verification for ROS 2 applications. The proposed verification focuses on callback execution latencies and buffer overflow. We propose formal model templates to model the execution of ROS 2 system components, created using a pattern-based approach. The model templates simplify the formal modeling of an ROS 2 application. Using Uppaal, we model in Uppaal timed automata, allowing the description of computation chains of ROS 2-based applications. Our focus is on execution behavior, including two versions of the mainline single-threaded executor of ROS 2. System traces generated using the formal models are validated in multiple experiments. Furthermore, we compare two approaches to modeling the execution of nodes that are typically the core units of computation of ROS 2. The first approach is a holistic approach to model ROS 2 applications, including communication and execution in computation chains. The second is an approach for individual nodes only, at a higher abstraction level. Additionally, we show the application of the verification by model checking in two ROS 2 system scenarios where we compare generated model traces to actual system executions. Overall, through formal modeling and verification, we showcase the potential for uncovering errors in the execution of distributed robotic systems.

Digital Twins (DTs) are virtual representations of physical products in many dimensions, such as geometry and behaviour. As a backbone of Industry 4.0, DTs help interpret and even predict the behaviour of physical processes, provide a virtual testbed for maintenance and upgrade, and enable automatic decision-making supported by artificial intelligence. Despite the promising future, challenges exist, such as the absence of a framework that facilitates the development and application of DTs in industrial contexts. We propose a service-oriented architecture (SOA) DT framework for dynamic and robust distributed systems. The framework contains two types of services. One includes the services provided to the users and is supported by an orchestration mechanism to ensure a quality of service (QoS). The other one refers to the common functions of all DTs. Further, we describe the DT-based decision-making enabled by our QoS-oriented learning of the framework and a Hoare-logic-based verification of QoS.

Digital Twins (DTs) serve as the backbone of Industry 4.0, offering virtual representations of actual systems, enabling accurate simulations, analysis, and control. These representations help predict system behaviour, facilitate multiple real-time tests, and reduce risks and costs while identifying optimization areas. DTs meld cyber and physical realms, accelerating the design and modelling of sustainable innovations. Despite their potential, the complexity of DTs presents challenges in their industrial application. We continue here the development of our approach to build an adaptable and trustable framework for building and operating DT systems - A Digital Twin Framework for Dynamic and Robust Distributed Systems (D-RODS). D-RODS aims to address the challenges above, aiming to advance industrial digitalization and targeting areas like system efficiency, incorporating AI and verification techniques with formal support. We employ existing large-usage tools to illustrate the approach in development based on a synthetic adaptable use case.

Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy given requirements. In this article, we propose a tool-supported mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements, a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it in a special case of an industrial case study.

Robot operating system 2 (ROS 2) is increasingly popular both in research and commercial robotic systems. ROS 2 is designed to allow real-time execution and data communication, enabling rapid prototyping and deployment of robotic systems. In order to predict and calculate execution times in ROS 2, one needs to analyze its internal scheduler, called executor. The executor has been updated in various distributions of ROS 2, which is shown to impact significantly the periodic execution invoked by the underlying operating system’s timers, potentially causing unexpected latencies. To expose the mentioned impact due to executor differences, in this paper, we present an experimental evaluation of the execution behavior of ROS 2’s schedulable entities, namely callbacks, among the existing versions of the executor. We visualize the differences of callback execution order via simulation, and we create design-level scenarios that impact the execution of periodically scheduled callbacks, negatively. Moreover, we show how such negative impact can be mitigated by using multi-threaded executors. Finally, we illustrate the observed behavior on a real-world centralized multi-agent robot system. Our work aims to raise awareness within the ROS 2 developer community, regarding possible problems of timer blocking, and propose a mitigation solution of the latter.

Planning is a critical function of multi-agent autonomous systems, which includes path finding and task scheduling. Exhaustive search-based methods such as model checking and algorithmic game theory can solve simple instances of multi-agent planning. However, these methods suffer from state-space explosion when the number of agents is large. Learning-based methods can alleviate this problem, but lack a guarantee of correctness of the results. In this paper, we introduce MoCReL, a new version of our previously proposed method that combines model checking with reinforcement learning in solving the planning problem. The approach takes advantage of reinforcement learning to synthesize path plans and task schedules for large numbers of autonomous agents, and of model checking to verify the correctness of the synthesized strategies. Further, MoCReL can compress large strategies into smaller ones that have down to 0.05% of the original sizes, while preserving their correctness, which we show in this paper. MoCReL is integrated into a new version of Uppaal Stratego that supports calling external libraries when running learning and verification of timed games models.

Abstract Path planning and task scheduling are two challenging problems in the design of multiple autonomous agents. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space explosion problem that makes it inefficient at solving the problems when the number of agents is large, which is often the case in realistic scenarios. In this paper, we propose a new version of our novel approach called MCRL that integrates model checking and reinforcement learning to alleviate this scalability limitation. We apply this new technique to synthesize path planning and task scheduling strategies for multiple autonomous agents. Our method is capable of handling a larger number of agents if compared to what is feasibly handled by the model-checking technique alone. Additionally, MCRL also guarantees the correctness of the synthesis results via post-verification. The method is implemented in UPPAAL STRATEGO and leverages our tool MALTA for model generation, such that one can use the method with less effort of model construction and higher efficiency of learning than those of the original MCRL. We demonstrate the feasibility of our approach on an industrial case study: an autonomous quarry, and discuss the strengths and weaknesses of the methods.