https://www.mdu.se/

It is not often that someone possesses qualities akin to those found in quantum phenomena, such as cleverness and quick reactions. Hence, I consider myself privileged that I have met and collaborated for many years with Tiziana Margaria, a renowed professor of Software Engineering and respected friend. This personal note that I dedicate to her tries to reflect both the professional and personal admiration that I hold for her. 

The European Train Control System Level 3 (ETCS-L3) leverages continuous communication and precise train localization to optimize traffic management and enhance safety. This paper presents a formal modeling approach for the control of railway switches within the ETCS-L3 framework. Formal methods enable the development of precise and verifiable models to ensure the correctness of switch operations, essential for train routing and collision avoidance. The work is part of the PERFORMINGRAIL project, integrating advanced formal verification tools and techniques to facilitate rigorous analysis and validation. The project also explores model diversity in moving block systems' safety and performability analysis. This paper specifically focuses on the control logic of railway switches, capturing the behavior of the point control subsystem and leveraging various modeling approaches. The switch control models address various operational scenarios, including normal operations, failure modes, and recovery procedures. The findings show that formal methods can significantly improve the robustness of railway switch systems, thereby contributing to safer and more efficient railway networks. This work paves the way for future research and implementation of formalized control systems in the broader context of smart and autonomous railway operations.

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose formal syntax and semantics of Simulink blocks and their composition, and introduce the tool SIMPPAAL that automates a previously introduced pattern-based, execution-order preserving transformation of Simulink atomic and composite blocks into stochastic timed automata. The resulting model can then be analyzed formally with UPPAAL Statistical Model Checker. We validate the approach on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

In the labyrinthine world of real-time systems, few names resonate as powerfully as that of Prof. Wang Yi. As the co-inventor of the UPPAAL model checker, alongside Prof. Kim G. Larsen and Prof. Paul Pettersson, Wang has charted new territories in computer science, setting a benchmark that stands as a testament to excellence.

To simplify the formal verification of ROS 2-based applications, in this paper, we propose a novel approach to the automation of their model-based verification using model-driven engineering techniques. We propose a methodology starting with ROS 2 execution traces, generated by ROS2_tracing and using models and model transformations in Eclipse to automatically initialize pre-defined formal model templates in UPPAAL, with system parameters. While the methodology targets the simplification of formal verification for robotics developers as users, the implementation is at an early stage and the toolchain is not fully implemented and evaluated. Hence, this paper targets tool developers and researchers to give a first overview of the underlying idea of automating ROS 2 verification.

Hence, we propose a toolchain that supports verification of implemented and conceptual ROS 2 systems, as well as iterative verification of timing and scheduling parameters. We propose using four different model representations, based on the ROS2_tracing output and self-designed Eclipse Ecore metamodels to model the system from a structural and verification perspective. The different model representations allow traceability throughout the modeling and verification process.Last, an initial proof of concept is implemented containing the core elements of the proposed toolchain and validated given a small ROS 2 system. 

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 in predicting system behaviour, facilitating multiple real-time tests, and reducing 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 sketch here an approach to build an adaptable and trustable framework for building and operating DT systems, which is the basis for the academia-industry project 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. 

Energy-efficient motion planning for autonomous battery-powered vehicles is crucial to increase safety and efficiency by avoiding frequent battery recharge. This paper proposes algorithms for synthesizing energy- and time-efficient motion plans for battery-powered autonomous vehicles. We use stochastic hybrid games to model an appropriate abstraction of the autonomous vehicle and the environment. Based on the model, we synthesize energy- and time-efficient motion plans using Q-learning in Uppaal  Stratego. Via experiments, we show that pure Q-learning is insufficient when the problem becomes complex, e.g., Motion Planning (MOP) in large environments. To address this issue, we propose Concatenated Motion Planning (CoMOP), which divides the environment into several regions, synthesizes a motion plan in each region and concatenates the local plans into an entire motion plan for the whole environment. CoMOP enhances the applicability of Q-learning to large and complex environments, reduces synthesis time, and provides efficient navigation and precise motion plans. We conduct experiments with our approaches in an industrial use case. The results show that CoMOP outperforms MOP regarding synthesis time and the ability to deal with complex models. Moreover, we compare the energy- and time-efficient strategies and visualize their differences on different terrains.

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.

Robotic systems often operate under real-time constraints,requiring timely responses to sensor inputs. Early consideration of suchrequirements during design is advantageous. The Robot Operating System(ROS) provides a mature framework for system setup and communication,with ROS2 offering real-time capabilities. However, determiningthe maximum reaction time within a ROS network is intricatedue to complex variable processing and scheduling, especially with periodicand event-triggered tasks. In this report, we propose a model ofROS-based structural designs with timed automata semantics, facilitatingreal-time behavior analysis. We extend this model to incorporatenon-deterministic execution time and probabilistic loads, employing statisticalmodel checking (SMC) for scalability and accuracy. We compareagainst previous work to confirm the validity of our approach.