With the pervasiveness of software-intensive systems, autonomous agents are increasingly involved in missions entailing close cooperation with humans in critical domains. Human-Machine Teaming (HMT) requires agents to have a high degree of autonomy to make dependable decisions in safety-critical settings and quickly react to unexpected changes in the environment. We present AdaptEASE, a framework that leverages formal modeling and verification to model HMT missions offline and predict the mission outcome at runtime through Machine Learning (ML) models trained on Statistical Model Checking (SMC) results. The framework also exploits explainable AI techniques to inform stakeholders on what factors impact the predicted outcome positively or negatively. Building upon previous work, AdaptEASE enhances the controlled autonomous agents with the capability to self-adapt at runtime proactively. Specifically, if an unfavorable situation emerges during the HMT, AdaptEASE identifies an adaptation action that guarantees balance between the agents' performance and the involved human subjects' comfort levels. While runtime adaptation exploits ML predictors to preserve the timeliness of the HMT, the proposed adaptation action is asynchronously subject to formal verification to provide stakeholders with an assessment of the agents' decisions and of the overall HMT trustworthiness. The validation testbed is a case study from the healthcare robot domain. The optimized versions of 1000 different mission configurations lead to a statistically significant estimated increase of HMT performance. The asynchronous SMC formal verification confirms that 75% of the optimized configurations increase the HMT performance.

Autonomous agents operating in socio-critical settings must coordinate with humans under uncertainty while respecting explicit safety constraints. Existing approaches either account for social dynamics without formal guarantees or provide formal assurance while abstracting away human behaviour. We introduce FormIDEAble, a formally grounded approach for synthesising socially-aware cooperation strategies with safety guarantees. The cooperation between humans and the autonomous agent is modelled as a Priced Timed Markov Decision Process, and decision-making is formulated as a cost-bounded reachability problem. We illustrate the approach using an emergency evacuation scenario. Initial experimental evidence demonstrates the effectiveness of the approach and highlights the trade-offs between optimisation and safety guarantees. FormIDEAble provides a principled foundation for formally assured, socially-aware decision-making in socio-critical systems.

The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractions have been shown to outperform zones in specific subclasses of TA. To complement and support mature zone-based tools, we introduce TARZAN, a C++ region-based verification library for TA. The algorithms implemented in TARZAN use a novel region abstraction that tracks the order in which clocks become unbounded. This additional ordering induces a finer partitioning of the state space, enabling backward algorithms to avoid the combinatorial explosion associated with enumerating all ordered partitions of unbounded clocks, when computing immediate delay predecessor regions. We validate TARZAN by comparing forward reachability results against the state-of-the-art tools Uppaal and TChecker. The experiments confirm that zones excel when TA have large constants and strict guards. In contrast, TARZAN exhibits superior performance on closed TA and TA with punctual guards. Finally, we demonstrate the efficacy of our backward algorithms, establishing a foundation for region-based analysis in domains like Timed Games, where backward exploration is essential.

Early-stage specifications of safety-critical systems are typically expressed in natural language, making it difficult to derive formal properties suitable for verification and needed to guarantee safety. While recent Large Language Model (LLM)-based approaches can generate formal artifacts from text, they mainly focus on syntactic correctness and do not ensure semantic alignment between informal requirements and formally verifiable properties. We propose an agentic methodology that automatically extracts verification-ready properties from unstructured specifications. The modular pipeline combines requirement extraction, compatibility filtering with respect to a target formalism, and translation into formal properties. Experimental results across three scenarios show that the pipeline generates syntactically and semantically aligned formal properties with a 77.8

Linear Temporal Logic (LTL) can be used for problem-solving when all problem constraints can be specified in this logic through the use of satisfiability checking techniques. In optimization problems such as scheduling with preferences, where constraints are primarily temporal, LTL is a desirable specification formalism. However, LTL cannot be used as a standalone formalism due to the fact that it is unable to specify soft constraints. This article introduces Optimization LTL (OLTL), an optimization-oriented extension of LTL that can specify both hard and soft constraints in optimization problems. The syntax, semantics and basic formal properties of this logic are presented, along with an encoding based on bit-vector logic and Linear Real Arithmetic (LRA). Additionally, a tool called LiTeLLab ( Li near Te mporal L ogic Lab oratory) is introduced to solve optimization problems specified by OLTL. The feasibility and scalability of using OLTL as a specification formalism is demonstrated through two case studies. These problems, with multiple optimization parameters, are specified in OLTL and LiTeLLab successfully generates optimal solutions.

Classical Timed Games formulations may be unsuitable, or require substantial modeling effort, to capture complex interaction patterns between a controller and its surrounding environment, in which the non-determinism must be resolved after the controller has chosen which action to perform. This paper introduces Timed CLTLoc Games (TCGs), a novel Timed Game variant designed to facilitate the modeling of such patterns. Unlike classical Timed Games, TCGs partition locations rather than actions, and use Constraint Linear Temporal Logic over clocks formulae to specify the controller’s objectives. We implement algorithms for solving TCGs in our C++20 region-based library Tarzan, leveraging OpenMP for efficient parallelization. We then validate our theoretical results through an empirical evaluation on a Production Cell case study, demonstrating that the region-based implementation is computationally efficient in practice for medium-sized models.

Code generation through Large Language Models (LLMs) has made significant progress in recent years. However, when the code generation involves a lesser-known Domain-Specific Language (DSL), a standard tool in software development for cyber-physical systems, LLMs' performance significantly decreases. We present an exploratory study assessing LLMs' performance in generating LIrAs (Language for Interactive Agents) code, a DSL for robotic and multi-agent tasks specification. This work is a stepping stone towards improving LLM-generated DSL code through iterative specification repair techniques driven by formal verification results.

A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult to detect, yet a high level of confidence in the outcome is expected. Indeed, these tools are frequently novel and may not have been thoroughly tested. When standard benchmarks may be insufficient or unavailable, random test case generation offers a promising approach. To scale up, random testing requires comparing actual versus expected results, i.e., solving the oracle problem. To address this challenge, this work introduces a novel theoretical framework based on a modular variant of Timed Automata (TA), called Tiled Timed Automata (TTA), for testing model checkers operating with variations of TA, by building oracles based on Weighted Automata. The framework is initially applied to verify model checkers solving the emptiness problem for Parametric TA and it is validated, in this specific scenario, by our tool, TABEC, which randomly generates tests predicting their expected outcome through automated oracle generation. Furthermore, the general nature of TTA facilitates the framework adaptation to model checkers solving other decidable problems on TA, as detailed for the minimum-cost reachability problem of Priced TA.

In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the same transition. The model has the same expressive power of TA, but it may require one more clock than an TA to recognize the same language. We consider the parametric version of nrtTA, where one parameter can appear in clock guards of transitions. The focus of this draft is to prove that the ω-language emptiness problem for 2-clock parametric nrtTA is decidable. This result can be compared with the parametric version of TA, where the emptiness problem for 2-clock TA with one parameter is not known to be decidable. Our result, however, extends the known decidability of the case of TA with one clock and one parameter from finite words to infinite words.

Protection systems are a crucial part of the electric power system. A tool has been developed to formally verify the correct configuration of protection systems in a low-voltage distribution grid. It uses a formal model, based on Timed Automaton, representing the relevant elements of a low-voltage distribution grid. The developed tool encountered several challenges related to the limited number of faults it could handle and the significant amount of time required for the verification process. Additionally, the verification output was hard to interpret, and in cases of multiple incorrectly configured circuit breakers, only the first one detected by the tool was presented to the user. This paper proposes a solution to address these challenges by implementing two versions of the procedure called Automatic Subdivision of Queries (ASQ) in the tool, namely ASQ(alpha) and ASQ(Omega), to overcome these challenges.

Large-scale graph processing and Stream processing are two distinct computational paradigms for big data processing. Graph processing deals with computation on graphs of billions of vertices and edges. However, large-scale graph processing frameworks mostly work on graphs that do not change over time, while on the other end of the spectrum, stream processing operates on a continuous stream of data in real time. Modern-day graphs change very rapidly over time, and finding patterns in temporally evolving graphs could reveal a lot of insights that can not be unveiled using traditional graph computations. We have proposed a novel framework called FlowGraph which could find patterns in dynamic and temporally evolving graphs. Computations on large-scale graphs are iterative and take multiple steps before final results can be calculated, which is very different from stream processing which is one-shot computation. Therefore, the most critical bottleneck of such a system is the time required to process the query. In this work, we have proposed a query optimization technique that could reduce the time required to process the pattern. The proposed system has an optimization technique that could reduce the time required to process the pattern, especially those related to the temporal evolution of the graph. Our method shows for eight clauses the execution time is reduced by 75%, we also proved that this improvement is not affected by the scaling of the graph or the change of elements in given clauses.

As software systems have become increasingly important, teaching Software Engineering students how to develop high-quality software is essential. In this regard, formal modeling and verification are important educational tools that help students in getting an indepth understanding of software. Nonetheless, formal languages are not straightforward to teach and, therefore, carefully designed materials are needed to convey them. In this paper we focus on Alloy, which is an easy-to-learn formal language equipped with a usable analyser, and we present a complete teaching module that can be used by teachers to support students in learning the temporal constructs defined in its latest version, Alloy 6. The module is designed exploiting active learning methods and is supported by multimedia content. It is openly available and can be reused and tailored to the need of specific courses.

Smart 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.

The paper addresses the problem of estimating the energy consumed by production resources in manufacturing so that alternative process designs can be compared in terms of energy expenditure. In particular, the proposed methodology focuses on Computer Numerical Controlled (CNC) machining centers. Classical approaches to energy modeling require high expertise and large development effort since, for example, data acquisition is resource-specific and must be repeated frequently to avoid obsolescence. An automated and flexible data-driven methodology is designed in this work. A data-driven method is employed to learn a hybrid and stochastic model of a CNC machining center’s energetic behavior. The learned model is used to provide offline energy consumption estimates of simulated part-programs before the actual execution of the cutting. Numerical results show the performance of the proposed method on a set of case studies. The methodology is also applied to a real industrial application, including data collected during machine production. Note to Practitioners —This article provides a flexible and autonomous data-driven approach to building models representing the energetic behavior of production resources, particularly CNC machining centers. The learned models can predict machine energy consumption while executing complex part-programs. The algorithm uses data that are commonly acquired by contemporary machine monitoring systems and does not require ad-hoc experimental tests for training. Specifically, it requires the spindle rotary speed signal, part load/unload signal, and spindle (or machine) power signal during the learning phase, whilst the estimation phase uses only the load/unload and spindle speed simulated signals.

Smart cyber agents are pivotal in software-intensive systems such as smart manufacturing, robotics, and the Internet of Things. These agents monitor physical surroundings through sensors and make impactful decisions that influence the environment. Software engineering challenges in this domain include the specification of interactive multi-agent tasks. The general-purpose Domain-Specific Language named LIrAs, Language for Interactive Agents, is a high-level language that allows for unambiguous custom pattern definition. Additionally, LIrAs facilitates interactions with human agents, a safety-critical situation requiring particular attention. This paper lays the foundation for LIrAs specifications translation to Stochastic Hybrid Automaton (SHA). The target SHA model structure follows a three-layer hierarchical structure and makes LIrAs specifications amenable to formal verification, specifically Statistical Model Checking, through the Uppaal tool, capable of including time-dependent physical phenomena, such as human fatigue and robot dynamics.

Software-intensive systems include enterprise systems, IoT systems, cyber-physical systems, and industrial control systems where software plays a vital role. In such systems, the software is increasingly responsible for autonomous decision-making. However, trust can be hindered by the black-box nature of these systems, whose autonomous decisions may be confusing or even dangerous for humans. Thus, explainability emerges as a crucial non-functional property to achieve transparency and increase the understanding of the systems' behavior, fostering their acceptance in our society. This paper introduces a conceptual framework for eliciting explainability requirements at different granularity levels. Each level is associated with a set of meta-requirements and means for instantiating the framework within a system to make it capable of producing explanations in a given application domain. We illustrate our conceptual framework using a running example from the robotics domain.

Evidence is rapidly accumulating that multifactorial nocturnal monitoring, through the coupling of wearable devices and deep learning, may be disruptive for early diagnosis and assessment of sleep disorders. In this work, optical, differential air-pressure and acceleration signals, acquired by a chest-worn sensor, are elaborated into five somnographic-like signals, which are then used to feed a deep network. This addresses a three-fold classification problem to predict the overall signal quality (normal, corrupted), three breathing-related patterns (normal, apnea, irregular) and three sleep-related patterns (normal, snoring, noise). In order to promote explainability, the developed architecture generates additional information in the form of qualitative (saliency maps) and quantitative (confidence indices) data, which helps to improve the interpretation of the predictions. Twenty healthy subjects enrolled in this study were monitored overnight for approximately ten hours during sleep. Somnographic-like signals were manually labeled according to the three class sets to build the training dataset. Both record- and subject-wise analyses were performed to evaluate the prediction performance and the coherence of the results. The network was accurate (0.96) in distinguishing normal from corrupted signals. Breathing patterns were predicted with higher accuracy (0.93) than sleep patterns (0.76). The prediction of irregular breathing was less accurate (0.88) than that of apnea (0.97). In the sleep pattern set, the distinction between snoring (0.73) and noise events (0.61) was less effective. The confidence index associated with the prediction allowed us to elucidate ambiguous predictions better. The saliency map analysis provided useful insights to relate predictions to the input signal content. While preliminary, this work supported the recent perspective on the use of deep learning to detect particular sleep events in multiple somnographic signals, thus representing a step towards bringing the use of AI-based tools for sleep disorder detection incrementally closer to clinical translation.

Interoperability is one of the critical challenges in the construction and management of distributed and collaborative systems. Hence, a deep understanding of the fundamental barriers to interoperability and of the key requirements that systems must meet to be interoperable is essential. In this direction, in the first part of this research, we conducted a questionnaire survey of stakeholders and practitioners of distributed and collaborative systems. As a result, we identified eight essential interoperability requirements and corresponding challenges. Then, in the second part of our study, we performed a critical literature survey of the building blocks of interoperability to understand the ability of current conceptual approaches---and related technologies---to address the identified requirements. The results of our research can significantly impact the software engineering of interoperable systems by introducing their fundamental requirements and the best practices to address them.

Interoperability stands as a critical hurdle in developing and overseeing distributed and collaborative systems. Thus, it becomes imperative to gain a deep comprehension of the primary obstacles hindering interoperability and the essential criteria that systems must satisfy to achieve it. In light of this objective, in the initial phase of this research, we conducted a survey questionnaire involving stakeholders and practitioners engaged in distributed and collaborative systems. This effort resulted in the identification of eight essential interoperability requirements, along with their corresponding challenges. Then, the second part of our study encompassed a critical review of the literature to assess the effectiveness of prevailing conceptual approaches and associated technologies in addressing the identified requirements. This analysis led to the identification of a set of components that promise to deliver the desired interoperability by addressing the requirements identified earlier. These elements subsequently form the foundation for the third part of our study, a reference architecture for interoperability-fostering frameworks that is proposed in this paper. The results of our research can significantly impact the software engineering of interoperable systems by introducing their fundamental requirements and the best practices to address them, but also by identifying the key elements of a framework facilitating interoperability in Systems of Systems.

In power systems protection, selectivity is a key property that must be guaranteed. It ensures the minimum amount of load is unfed when a fault occurs and it reduces the time needed to restore service. Selectivity is achieved through coordination of circuit breakers (CBs), whose logic is most commonly determined by a combination of time and current thresholds. Verifying the correctness of CBs' settings is crucial when designing power system protections and may become a challenging task for big networks. This paper proposes an approach for the rigorous verification of the correct configuration of protection systems in low-voltage (LV) distribution grids. The method utilized depends on a precise model that employs Timed Automata (TA) to represent the crucial elements of an LV distribution grid. Additionally, it incorporates a system for producing and validating formal models from higher-level JSON-based depictions of electrical networks, taking advantage of the Uppaalmodel checker. The effectiveness of the approach has been tested on several realistic power systems.