https://www.mdu.se/

The increasing demand for autonomous machines in construction environments necessitates the development of robust object detection algorithms that can perform effectively across various weather and environmental conditions. This paper introduces a new semantic segmentation dataset specifically tailored for construction sites, taking into account the diverse challenges posed by adverse weather and environmental conditions. The dataset is designed to enhance the training and evaluation of object detection models, fostering their adaptability and reliability in real-world construction applications. Our dataset comprises annotated images captured under a wide range of different weather conditions, including but not limited to sunny days, rainy periods, foggy atmospheres, and low-light situations. Additionally, environmental factors such as the existence of dirt/mud on the camera lens are integrated into the dataset through actual captures and synthetic generation to simulate the complex conditions prevalent in construction sites. We also generate synthetic images of the annotations including precise semantic segmentation masks for various objects commonly found in construction environments, such as wheel loader machines, personnel, cars, and structural elements. To demonstrate the dataset’s utility, we evaluate state-of-the-art object detection algorithms on our proposed benchmark. The results highlight the dataset’s success in adversarial training models across diverse conditions, showcasing its efficacy compared to existing datasets that lack such environmental variability.

Software architecture relies heavily on modeling techniques to describe, analyze, and verify system designs. The Unified Modeling Language (UML) is widely recognized as both a de facto and de jure standard for modeling various types of systems. While UML has formalized semantics that enhance consistency and precision, it is not inherently designed for model checking. Rebeca, an actor-based modeling language, is designed to enable formal verification of concurrent reactive systems. Previous efforts to bridge UML and Rebeca through model transformations have required combining multiple UML diagrams and a deep understanding of Rebeca, limiting practical applicability. In this paper, we explore the potential of leveraging large language models, specifically GPT-4, to automate the transformation of UML state diagrams into Rebeca models. Using a few-shot learning approach, we investigated the feasibility of this translation process. Initial results revealed that UML state diagrams alone were insufficient for generating accurate Rebeca models. To address this limitation, we augmented the diagrams with metadata, enabling GPT-4 to produce models that required only minor corrections to be executable in Rebeca's model-checking tool, Afra. Our findings demonstrate that LLMs hold promise in facilitating model transformations for software architecture, particularly for translating UML state diagrams into Rebeca models for formal verification. While not yet fully automated, this approach significantly reduces the effort required for transformation, paving the way for further research into the integration of LLMs into model-driven engineering practices.

This paper presents a method and a practical implementation that complements traditional conformance testing. We infer a Mealy state machine of the system-under-test using active automata learning. This automaton is checked for bisimulation with a specification automaton modeled after the standard, which provides a strong verdict of conformance or nonconformance. We further present a method to learn models of multiple communication protocols running on the same device using a dispatcher system in conjunction with the same automata learning algorithms. We subsequently use similar checking methods to compare it with separately learned models. This allows for determining whether there is some interference or interaction between those protocols. In the practical execution of the system, we concentrate on lower levels of the Near-Field Communication (NFC, ISO/IEC 14443-3) and the Bluetooth Low-Energy (BLE) protocols. As a by-product, we share some observations of the performance of different learning algorithms and calibrations in the specific setting of ISO/IEC 14443-3, which is the difficulty to learn models of systems that a) consist of two very similar structures and b) timeout very frequently, as well as the role of conformance testing for compound models and speed optimizations for time-sensitive protocols.

The Rebeca modeling language is designed as an imperative actor-based language with the goal of providing an easy-to-use language for modeling concurrent and distributed systems, with formal verification support. Rebeca has been extended to support time and probability. We extend Rebeca further with inheritance, polymorphism, interface declaration, and annotation mechanisms. These features allow us to handle variability within the model, support non-disruptive model evolution, and define method priorities. This enables Rebeca to be used more effectively in different domains, like in Software Product Lines, and holistic analysis of Cyber-Physical Systems. We develop specialized analysis techniques to support these extensions, partly integrated into Afra, the model checking tool of Rebeca.

Passports are part of critical infrastructure for a very long time. They also have been pieces of automatically processable information devices, more recently through the ISO/IEC 14443 (Near-Field Communication - NFC) protocol. For obvious reasons, it is crucial that the information stored on devices are sufficiently protected. The International Civil Aviation Organization (ICAO) specifies exactly what information should be stored on electronic passports (also Machine Readable Travel Documents - MRTDs) and how and under which conditions they can be accessed. We propose a model-based approach for checking the conformance with this specification in an automated and very comprehensive manner: we use automata learning to learn a full model of passport documents and use trace equivalence and primitive model checking techniques to check the conformance with an automaton modeled after the ICAO standard. Since the full behavior is underspecified in the standard, we compare a part of the learned model and apply a primitive checking ruleset to assure proper authentication. The result is an automated (non-interactive), yet very thorough test for compliance, despite the underspecification. This approach can also be used with other applications for which a specification automaton can be modeled and is therefore broadly applicable.

ROS2 is an increasingly popular middleware framework for developing robotic applications. A ROS2 application is composed of nodes that run concurrently, coordinate with each other through asynchronous interfaces, and can be deployed in a distributed manner. Rebeca is an actor-based language for modelling asynchronous and concurrent systems. Timed Rebeca adds timing features to deal with timing requirements of real-time systems. The similarities in concurrency and message-based asynchronous interactions of reactive nodes, and the ability of modelling timed behaviours justify using Timed Rebeca models to assist the development and verification of ROS2 applications. Model-based development and model-checking techniques allow faster prototyping and earlier detection of system errors before developing the entire real system. However, there are challenges in bridging the gap between continuous behaviours of robotic systems and discrete states in a model for automatic verification, and between complex robotic computations and inequivalent programming facilities in a modelling language like Timed Rebeca. We investigated the problem systematically and have succeeded in modelling a realistic multiple autonomous mobile robots (AMR) system using Timed Rebeca, creating corresponding ROS2 demo code, and showing the match between the model and the program. Based on experiments, we demonstrated the value of the model in development and automatic formal verification of correctness properties (target reachability, collision freedom, and deadlock freedom). Our model-checking results show that certain system problems are not always detected through simulation. The modelling principles, modelling and implementation techniques that are created and used in this work can be generalized for many other cases. 

We propose CRYSTAL framework for automated cybersecurity assurance of cyber-physical systems (CPS) at design-time and runtime. We build attack models and apply formal verification to recognize potential attacks that may lead to security violations. We focus on both communication and computation in designing the attack models. We build a monitor to check and manage security at runtime and use a reference model, called Tiny Digital Twin, in detecting attacks. The Tiny Digital Twin is an abstract behavioral model that is automatically derived from the state space generated by model checking during design-time. Using CRYSTAL, we are able to systematically model and check complex coordinated attacks. In this paper we discuss the applicability of CRYSTAL in security analysis and attack detection for different case studies, Temperature Control System (TCS), Pneumatic Control System (PCS), and Secure Water Treatment System (SWaT). We provide a detailed description of the framework and explain how it works in different cases.

Integration of the Internet of Things (IoT) in industrial settings necessitates robust cybersecurity measures to mitigate risks such as data leakage, vulnerability exploitation, and compromised information flows. Recent cyberattacks on critical industrial systems have highlighted the lack of threat analysis in software development processes. While existing threat modeling frameworks such as STRIDE enumerate potential security threats, they often lack detailed mapping of the sequences of threats that adversaries might exploit to apply cyberattacks. Our study proposes an enhanced approach to systematic threat modeling and data flow-based attack scenario analysis for integrating cybersecurity measures early in the development lifecycle. We enhance the STRIDE framework by extending it to include attack scenarios as sequences of threats exploited by adversaries. This extension allows us to illustrate various attack scenarios and demonstrate how these insights can aid system designers in strengthening their defenses. Our methodology prioritizes vulnerabilities based on their recurrence across various attack scenarios, offering actionable insights for enhancing system security. A case study in the automotive industry illustrates the practical application of our proposed methodology, demonstrating significant improvements in system security through proactive threat modeling and analysis of attack impacts. The results of our study provide actionable insights to improve system design and mitigate vulnerabilities.

A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.

In this paper, we report our ongoing work on safe and secure controller synthesis for cyber-physical systems (CPS). Our approach separates the synthesis process into three phases, in which we alternatively perform exhaustive and selective exploration of the system’s state space. In this way, we combine the strengths of exhaustive search and learning to mitigate the state-space-explosion problem in controller synthesis while preserving the guarantee of safety and security. We implement the synthesis algorithms in the Rebeca (Reactive Objects Language) platform, which provides modelling, verification, and state-space visualization. We evaluate the new approach in an experiment, demonstrating the reduced number of explored states, which shows the potential of our approach for synthesizing safe and secure controllers for complex CPS.