Modern software systems increasingly operate in dynamic and uncertain environments, where traditional dependability mechanisms, such as fault prevention and tolerance, could prove to be insufficient. This limitation has motivated research into methods for optimising and reconfiguring systems to enable dynamic adaptation to environmental changes. Nowadays, with the rise of artificial intelligence, numerous optimisation algorithms have emerged that can support systems and improve their performance. In this paper we explore whether Digital Twins equipped with Active Inference (AIF), a framework for adaptive behaviour under uncertainty, are a proper alternative to reconfigure software systems in order to optimise the performance of systems. AIF agents maintain internal generative models and continuously update their beliefs and actions based on new evidence, making it possible to optimise the system over time. We introduce an architecture that integrates AIF within a Digital Twin (DT), a virtual representation of a system synchronised with real-time and historical data. This architecture enables both a proactive adaptation and the exploitation of the new acquired knowledge. We evaluate our approach using SWIM, a web application simulation platform, to enhance the reproducibility and replicability of our proposal. The evaluation shows that the developed AIF-enhanced DT autonomously manages workload balancing and resource provisioning, demonstrating measurable improvements over reactive strategies. This work provides a computational foundation for engineering optimised service-oriented systems, contributing to the broader goal of dependable software in uncertain environments.
SQL is the main language used to query data in relational databases and interact with them. However, for accomplishing certain reasoning tasks (such as semantic query optimization, reasoning, query containment, etc), it is desirable to translate SQL into first-order languages (e.g., relational calculus, or Datalog). Indeed, a first-order logic formalism facilitates the analysis of SQL queries without having to depend on the nuances of their implementations. The possibility of this translation is already known due to the equivalence in expression power between relational algebra and relational calculus. Unfortunately, although this equivalence was discovered more than 40 years ago, to date there is no public, open-source, and validated tool to obtain these translations. This paper presents BLAST, an automatic and bidirectional translator between SQL expressions and first-order logic, focused on mapping SQL queries, views or assertions into logic queries, derivation rules, or logic constraints, and vice versa. The translator comes with two interfaces, a GUI one (for end users), and a Java API (for integrating the translator into other tools); and provides two different translation strategies depending on the user needs. To ensure that the code is easy to adopt, maintain, and contribute to, the whole project is based on metamodels.
Robotics and Autonomous Systems are increasingly deployed in safety-critical domains, so that demonstrating their safety is essential. Assurance cases (ACs) provide structured arguments supported by evidence, but generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve. We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow. The approach addresses three challenges: systematically deriving formal assertions from natural language requirements using templates, orchestrating multiple formal verification tools to handle diverse property types, and integrating formal evidence production into the workflow. Leveraging RoboChart, a domain-specific modelling language with formal semantics, we combine model checking and theorem proving in our approach. Structured requirements are automatically transformed into formal assertions using predefined templates, and verification results are automatically integrated as evidence. Case studies demonstrate the effectiveness of our approach.
Metamodels are central artefacts in model-driven engineering and continuously evolve in response to changing requirements, technologies, and domain concepts. Such evolutions directly impact all related models, which must be co-evolved accordingly. Therefore, co-evolution depends on correctly recorded changes at the meta level since even small inaccuracies can affect the models that will be evolved. In practice, however, the history of a metamodel is often incomplete, imprecise, or lost, as metamodel evolution is usually tracked using text-based version control systems that only store the textual difference instead of the semantic changes. In this paper, we propose a novel approach that allows engineers to reconstruct the history of metamodels with the help of ChangeTrees. Each ChangeTree represents alternative sequences of possible changes, allowing engineers to explore and assess different interpretations of metamodel evolution. To assist engineers in navigating the potentially large search space, we introduce a ranking and recommendation mechanism that prioritises the most likely changes for each change type. We evaluate our approach on 18 metamodels from different domains and complexities, applying up to 351 changes per metamodel. The results demonstrate that our approach correctly reconstructs and recommends all applied changes. Additionally, in our experiments, the recommendation mechanism significantly reduces the number of candidate changes presented to engineers. Furthermore, the performance results show that, in the worst-case scenario, our approach required 36.82 s to detect and generate a ChangeTree, resulting in 60,618 alternative sequences of changes. In addition, even in the worst-case scenarios, the recommendation mechanism consistently ranked the correct change within the top three recommendations per change type.
