Functional Block Diagrams (FBDs) are widely used for safety analysis in complex industrial electronic systems, such as smart grids and autonomous platforms. They model stochastic behaviors and cascading dependencies of system components using hierarchical Functional Blocks (FBs). Event Tree (ET) modeling is typically integrated with FBDs to capture complete and partial failure scenarios. This paper introduces 𝔽𝔼𝕋𝕄𝔸 (Functional Block Diagram and Event Tree Modeling and Analysis), a software tool for automating FBD construction and safety evaluation. We use 𝔽𝔼𝕋𝕄𝔸 to analyze an automated smart grid substation comprising three levels: Station, Bay, and Process. The tool identifies all possible failure and reliability events across these levels. To evaluate 𝔽𝔼𝕋𝕄𝔸 ’s scalability, accuracy and execution time, we compare its results with MATLAB-based Monte Carlo simulations, the Isograph software and manual analysis.
The rapid advancement of Deep Reinforcement Learning (DRL) has opened new opportunities for improving the autonomy and energy efficiency of Unmanned Aerial Vehicles (UAVs) in collaborative missions. In this paper, we propose E-MAPPO-CTDE (Energy-aware Multi-Agent Proximal Policy Optimization with Centralized Training and Decentralized Execution), a novel trajectory optimization framework designed for UAV swarms operating in constrained environments. Unlike existing approaches, E-MAPPO-CTDE integrates a realistic energy consumption model based on displacement, acceleration, and flight time into a centralized learning process that yields decentralized, real-time decision policies. Each UAV learns to generate collision-free, communication-aware, and energy efficient trajectories using a multi objective reward function. Through extensive simulations involving static obstacles and multiple agents, E-MAPPO-CTDE demonstrates significant energy savings and improved path coordination. These results confirm the potential of our framework for scalable deployment in real-world scenarios such as surveillance, search and rescue, and logistics.
Formal verification of cyber-physical systems (CPS) requires a model that accurately represents physical measurements from the real world. Incorporating explicit units into these measurements enhances rigour by enabling the verification of unit compatibility and correction in computations. While formal methods such as Event-B support static type checking, they lack the capability to annotate variables with physical measurement units. This paper proposes extending the Event-B type-checking system by defining a generic theory that offers the possibility to annotate Event-B variables with measurement units. This approach allows the specification of physical quantities, units, and measurements using the Theory plug-in.
The railway signaling system is responsible for managing traffic and ensuring a safe distance between trains in all circumstances. Faced with growing demand for rail transport, renowned for its low carbon footprint, the traditional signaling system, based on the fixed block concept, is reaching its capacity limits. Future signaling systems, based on the moving block concept, aim to reduce the spacing between succeeding trains, thus optimizing the use of existing infrastructure. However, the full requirements for these systems are still under development and require further refinement before they can be considered as a viable and, above all, safe solution for European railways. In this context, European projects X2Rail-1 (2019), X2Rail-3 (2020) and X2Rail-5 (2022) provide detailed descriptions of the functional and safety requirements of these systems in structured natural language. This article presents a method for analyzing these requirements. The study relies on rule-based tools and custom scripts to extract, track, and visualize the evolution of these requirements. The identified requirement changes guided the update of the system’s functional architecture to align with the most recent specifications.
Reversibility is a critical property of concurrent systems, reflecting their ability to return to the initial state without external intervention. Petri nets (PN) are widely used to model such systems, as they effectively capture complex interleavings and asynchronous behaviors. Traditional approaches to reversibility checking typically rely on constructing the reachability graph (RG) of a PN, which often encounters state-space explosion. Although partial order methods have been proposed to mitigate this issue by eliminating redundant interleavings, few are tailored to reversibility analysis. In this work, we propose a novel approach based on the notion of sound steps and introduce a definition called reversibility-aware score. Each transition is annotated with a reversibility-aware score indicating the likelihood of returning to the initial marking after its firing. At a given marking, transitions with the highest scores in a maximal sound step are grouped and fired simultaneously, resulting in a new marking. This procedure is conducted iteratively until no new markings are generated, producing a reversibility-aware step graph (RASG). We formally prove that RASG preserves the presence of deadlocks and enables efficient reversibility checking.
In Publicly Verifiable Secret Sharing (PVSS) schemes, any participant can verify the validity of the shares distributed among the participants as well as the correctness of the recovered secret. Thus, the corrupted shares and misbehaving participants can be identified and there is no need for complaint management phase. Since there are less communication rounds, this contribution offers a positive impact in distributed protocols that are based on PVSS to decrease communication’s complexity. An aggregatable PVSS permit to homomorphically combine several transcripts into a single transcript relative to the sum of their individual secrets. In this paper, we propose a Distributed Multi-Key Generation (DMKG) protocol with partially aggregatable and publicly verifiable transcripts. The proposed protocol benefits from the efficiency of the complaint management strategy introduced by Kalai et al. in [20] and from the contribution of the publicly verifiable secret sharing (PVSS) scheme based on the enhanced SCRAPE PVSS presented by Gurkan et al. in [18].
This paper presents an approach to provide stochastic bounds for models based on task graphs completion when the elementary durations are stochastic and not independent. When the parameters are deterministic, the complexity of computing the completion time is polynomial. Here, we consider the much more complex case where the durations are discrete random variables. Such an assumption drastically changes the complexity of the problem. Furthermore, we assume that these random variables are somehow correlated. We propose to give stochastic bounds based on the stochastic order for discrete multivariate random vectors to compute bounds on the completion time.
Time-Sensitive Networking (TSN) is crucial for ensuring deterministic communication in real-time applications. In TSN, Network Traversal Time (NTT) is a critical metric that quantifies the timeliness of received data. Maintaining low NTT is essential for ensuring accurate system responses and to prevent outdated information from affecting real-time operations. However, the presence of non-zero arrival jitter negatively impacts NTT and poses challenges in providing predictable performance. When jitter increases, packets may arrive inconsistently, causing some to be delayed while others may arrive in bursts. To address this, we analyze the NTT bounds for time-critical flows, influenced by arrival jitter. We propose an analytical framework to estimate best- and worst-case ST slots for data transmission, considering interference from higher priority flows and establishing data reachability along the network path across the switches. To validate our analysis, we conducted experiments using both a synthetic task set and an automotive use case. We also analyzed the impact of flow parameters on NTT determination, which, in some scenarios, led to pessimistic bound estimations.
Laplacian matrices are essential algebraic representations of network systems, which facilitate the description of topological characteristics, such as connectivity and symmetry. However, a critical issue emerges when the Laplacian matrix of a network is inherently singular, i.e., its inverse does not exist. In this case, it is crucial to use the generalized inverse of the matrix, known as pseudoinverse. In this paper, we provide a rigorous formalization of the pseudoinverse of the Laplacian matrix representing a weighted graph within higher-order logic theorem proving. Particularly, we formalize in Isabelle/HOL the generic concept of a matrix pseudoinverse that is applicable for both singular and nonsingular matrices. We then formalize the pseudoinverse of a Laplacian matrix and verify its classical properties. As an application, we formally verify the Kirchhoff index of a two-horizontal bridge circuit network.
Nowadays, with the rapid expansion of Internet of Things (IoT) net-works, extending device battery lifetime has emerged as a paramount challenge. The 3GPP Narrowband IoT (NB-IoT) standard introduces advanced power-saving mechanisms, notably Power Saving Mode (PSM) and extended Discontinuous Reception (eDRX), designed to enhance device energy efficiency. However, achieving optimal energy savings necessitates a comprehensive evaluation of energy consumption under varying traffic conditions and configuration parameters. This paper proposes a stochastic Petri net (SPN) model to rigorously analyze the energy dynamics of NB-IoT devices, providing system designers with a robust analytical tool for performance evaluation and energy optimization. The model accurately reflects real-world device behavior by integrating Radio Resource Control (RRC) states, stochastic uplink and downlink traffic patterns, and critical 3GPP timer settings to simulate battery drain scenarios. Performance analyses conducted across diverse traffic loads and configurations of PSM intervals and eDRX cycles enable the quantification of energy consumption and the identification of optimal parameter settings to maximize battery lifetime. Validation results confirm the model’s effectiveness, particularly in characterizing mean sojourn times across operational states. Ultimately, this approach empowers NB-IoT system designers to tailor configurations that balance power efficiency with performance requirements, thereby facilitating the deployment of more sustainable IoT networks. While the model provides valuable insights for device-level parameter tuning under idealized conditions, future extensions should address dynamic traffic patterns, network-level effects, and broader empirical validation to enhance real-world applicability.
There is an increasing demand for automation in system engineering, particularly for the development of complex systems, to speed up the development process and minimise the risk of coding errors. In current setting, Python has increasingly become a preferred choice for developers and industries for prototype development, particularly due to its robust ecosystem of open-source libraries and frameworks. However, it lacks safe coding features for critical systems. Formal methods are important for designing safe systems by verifying essential safety properties. Event-B and B methods are already in the core industrial practices for the verification and validation of system requirements. These verified models can be further used for code generation. However, manual code generation can be prone to errors and is often time-consuming, which may result in serious system failures. To produce safe Python code from formal models, we advocate for automating the code generation process. This paper introduces a code generation methodology, along with tool support, for generating Python code from Event-B models. Additionally, we have implemented and tested a plugin, called EB2Py, on several Event-B examples to demonstrate scalability and reliability of our approach.
In a context where the increasing complexity of discrete event systems (DES) makes flexible modeling tools essential, interoperability between different formalisms has become a central challenge. This work addresses this issue by exploring the transformation between three widely used formalisms: automata, Petri Nets, and DEVS models (Discrete Event System Specification). The proposed approach involves two main steps. First, a systematic review of existing transformation rules reported in the literature is conducted. Second, generative artificial intelligence is employed to automatically generate transformation rules. The rules derived from the literature and those generated by the AI are then compared. Based on this comparison, a refined set of transformation rules was manually defined. These rules were applied to a practical case study: modeling the behavior of an autonomous cleaning robot. The robot’s behavior was initially modeled as an automaton and then transformed into a Labelled Petri Net using the defined rules. This transformation was implemented in Python, enabling automated validation of the correspondence between the two formalisms while preserving the system’s behavioral logic.
This paper investigates the impact of static temporal parameters on the behavior of timed discrete event systems modeled using dual-time Petri nets. In such models, the firing of transitions is essential to ensure correct system evolution. However, improperly configured temporal constraints may result in dead transitions, where certain transitions are prevented from firing despite being enabled with respect to markings, thereby disrupting expected system behavior. To address this issue, we analyze the conditions under which dead transitions occur due to invalid temporal functions within the net structure. Based on this analysis, a set of adjustment options is introduced to resolve a dead transition, designed to restore an invalid firing window by modifying temporal parameters. Furthermore, we propose a cost-based adjustment strategy that iteratively derives a valid temporal function, ensuring the absence of dead transitions in the revised system. At each iteration, the strategy selects the adjustment option with the lowest associated cost to resolve a specific dead transition. To validate the effectiveness of the proposed approach, an extended state class graph is employed as a structural representation of D-TPN evolution, enabling verification of the resolution of dead transitions under each revised temporal function.
Modern autonomous-driving solutions rely on neural networks for visual perception. They typically lack precise specifications for when their behavior is considered to be correct, which complicates the use of traditional specification-driven verification approaches. To address this challenge, ISO standard 21448 (“Safety of the Intended Functionality”, SOTIF) proposes activities focused on reducing – rather than eliminating – the risk of using machine-learned models and the resulting extent of harm. One valuable activity in a SOTIF-based development process is runtime monitoring, as it provides a safeguard against scenarios that could not be anticipated during development. In the context of visual perception components based on learned neural networks, a runtime monitor can detect previously unknown driving scenarios during operation. For a SOTIF-based safety argument, however, the value it brings to the table needs to be quantified. In this paper, we show how by combining activation pattern monitoring with ideas from conformal testing, a monitoring approach with statistical guarantees can be defined that supports a SOTIF safety argument. We apply an ellipsoid-based abstraction of the activation patterns that are local to the output of a YOLO real-time object-detection neural network. We demonstrate that by restricting the scope of the monitor to detect input that is clearly out-of-domain (OD) at runtime, a high accuracy of the monitor can be obtained, leading to strong safety guarantees that a SOTIF safety argument can build on.
This paper investigates on the integration of Large Language Models (LLMs) with the QC-OpenDRIVE framework in order to generate syntactically and semantically correct OpenDRIVE files. OpenDRIVE files play an important role in the scenario-based validation of autonomous driving systems as they define the static part (e.g. road layout) on which the function are validated. While LLMs excel at generating code or similar tasks which mostly needs to be syntactically correct, the validation of semantic, especially normative, correctness remains challenging. To ensure norm-adherent correctness of generated OpenDRIVE files this paper proposes an integration of a feedback-loop with LLMs and QC-OpenDRIVE. While LLM allow to easily generate different road layouts, they often show issues like missing or unconnected roads or improper continuity. To address this issue, we have implemented E.5.9.1 to ensure geometric continuity between connected roads, which is a key contribution of this paper. State-of-the-art models are evaluated on three tasks to create OpenDRIVE road networks and validate the results featuring the feedback-loop. Results show that models leveraging Retrieval Augmented Generation (RAG) or internal reasoning and using the feedback loop can generate syntactically and semantically valid outputs after iterative corrections. However, challenges remain to prompt complex scenarios and tasks, especially following geometric rules without explicit feedback. The results demonstrate the necessity of domain-specific normative validation frameworks to prepare the use of LLMs for safety-critical applications. They can be used to enable scalable generation of edge-case scenarios while ensuring compliance with industry standards. This work bridges the gap between automated scenario generation and rigorous validation of reliable autonomous driving systems.
Model-Based Systems Engineering (MBSE) is increasingly adopted to manage the growing complexity of modern systems, offering a structured, collaborative design approach through modeling languages like SysML. However, its adoption remains challenging due to steep learning curves and the need for interdisciplinary coordination. This paper investigates the use of voice-enabled AI avatars to simplify MBSE interaction by allowing users to query system artifacts using natural language. By integrating a speech-based interface with AI assistants and human-like avatars representing various engineering roles, we aim to lower entry barriers, foster collaboration, and support diverse perspectives inherent in MBSE. Our proposed pipeline converts model data into a machine-readable format for large language models (LLMs) to generate contextualized, role-based responses. We explore the potential of using MBSE models as a knowledge base for AI and examine how such tools can enhance system model comprehension. Contributions include a prototype implementation, support for multi-turn interactions, and an initial evaluation of the approach.
As Artificial Intelligence (AI) continues to shape individual lives, institutional processes, and societal structures, ensuring its responsible and trusted development has become a critical imperative. However, meeting this imperative is far from straightforward. AI systems frequently lack transparency and are embedded in environments where the distribution of responsibility and accountability is unclear, normative standards are disputed, and system behavior is unpredictable. The Responsible and Trusted AI track at AISoLA 2025 addresses these and similar challenges by fostering interdisciplinary collaboration across philosophy, law, psychology, economics, sociology, political science, and informatics. This introduction outlines the motivation for the track, emphasizing the sociotechnical embeddedness of AI and the need for approaches that go beyond technical performance to consider questions related to trust and responsibility. It highlights three core themes explored in this year’s contributions: democratic legitimation and normative alignment, legal compliance and human oversight, and runtime safety in high-risk contexts. Together, these contributions underscore the importance of interdisciplinary discussions to navigate normative ambiguity, regulatory uncertainty, and behavioral unpredictability in AI systems. The track aims to advance dialogue and collaboration that support the development and deployment of AI systems that are not only effective but are also designed and implemented responsibly and can be trusted.
This is an introduction to the track ‘AI Assisted Programming’ (AIAP), organized at the third instance of the AISoLA conference during the period November 1–5, 2025. AISoLA as a whole aims to study opportunities and risks of late advances of AI. The motivation behind the AIAP track in particular, which also takes place the third time, is the emerging use of large language models for the construction and analysis of software artifacts. An overview of the track presentations is provided.
This extended abstract outlines technical reasons that embodiment qualitatively changes the nature of AI agents and potentially enables sentience. Specifically, I argue that knowledge can be purely subjective, not externally observable, and that sentience is this form of knowledge. I further argue that first-person interaction can gain knowledge that no objective observation can gain. And finally, I argue that the introduction of feedback through the physical world enables distinguishing self from non-self, an essential distinction for sentience. Putting all these together, I conclude that embodied AI agents may in fact become sentient, but also that we can never know for sure whether this has happened.
While large language models (LLMs) have exhibited strong capabilities in translating code, particularly from C to Python, their performance noticeably declines when dealing with less common languages like LF. Prior research indicates that Retrieval-Augmented Generation (RAG) can enhance LLMs capabilities in code generation by integrating codebase retrieval. Despite its promise, RAG systems are constrained by LLMs capabilities to deal with less common languages. Agentic AI coding assistants offer a different approach by acting as AI co-developers, automating tedious tasks and allowing developers to focus on high-level design. This paper proposes a novel system that combines RAG with agentic AI assistants to improve the accuracy of converting LF programs with target C into LF code with target Python. We conduct a comparative evaluation of state-of-the-art proprietary and open-source code LLMs in this task, demonstrating that RAG can significantly narrow the performance gap between small and large language models. Furthermore, we integrate an agentic assistant within an AI-powered IDE to automate developer-assisted error correction and refactoring, streamlining the development workflow. In terms of syntax correctness and successful execution rates, experiments highlight the significant improvements achieved by the combined approach.
