https://www.um.edu.mt/library/oar/handle/123456789/8338 2026-06-30T18:56:20Z https://www.um.edu.mt/library/oar/handle/123456789/147747 Title: FLARE — monitoring for the regulatory requirements of a drone case study Authors: Fenech, Sean; Colombo, Christian; Pace, Gordon; Curmi, Axel Abstract: As regulatory requirements for software systems in the European Union continue to evolve, there is growing pressure to embed mechanisms into deployed systems that ensure both operational trustworthiness and legal accountability. Frameworks such as the AI Act and the Cyber Resilience Act introduce obligations related to cybersecurity, incident response, transparency, and auditability, particularly for high-risk and autonomous systems. These demands go beyond traditional verification and increasingly call for runtime components capable of monitoring behaviour, detecting non-compliance, and preserving forensic evidence. In this work, we present FLARE, a runtime verification tool that combines automated monitoring with tamper-evident logging to support regulatory compliance. Building on existing runtime verification techniques, FLARE enables the construction of both a system harness that monitors live interactions with the environment and flags policy violations; and a forensic node, capable of recording verifiable logs. We demonstrate the application of FLARE on a waste-identification and localisation drone, a cyber-physical system subject to multiple legal and safety constraints. Our case study shows how FLARE can support legal and operational requirements while introducing minimal overhead, providing a practical path towards compliance-aware software instrumentation. 2026-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/145790 Title: Reversible computation vs. runtime adaptation in industrial IOT systems Authors: Attard, Duncan Paul; Bugeja, Keith; Francalanza, Adrian; Galea, Marietta; Tabone, Gerard; Zahra, Gianluca Abstract: This paper presents a comparative study between two software engineering techniques, reversible computation and runtime adaptation, in the context of industrial IoT. We frame our comparison around a representative Industry 5.0 shop floor case study that focuses on the high-precision manufacturing of integrated circuits. The case study identifies four error scenarios that can arise in typical shop floor operations and evaluates how reversible computation and runtime adaptation address them, highlighting the strengths and limitations of each approach. 2025-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/143412 Title: Marco Polo - a tool for automated exploratory testing of previously unseen online stores Authors: Gatt, Cristina; Micallef, Mark; Bugeja, Mark Abstract: Online stores continue to increase in popularity with 2.3 billion people estimated to have shopped online during 2022. Whilst every online store is unique in its own right, the online shopping domain itself is quite constrained in terms of the type of functionality being offered. This begs the question as to why companies invest so much time, effort and money into developing complete test suites for their specific systems. In this paper, we argue that it would be more efficient for companies to leverage the abundant common ground between most systems in the domain such that they need only focus on features that make their product unique when it comes to allocating testing effort. We go on to present Marco Polo, an automated exploratory testing tool inspired by the renowned explorer and trader from the 13th century. Using behavioural cloning to train on expert traces from a sample of online stores, this tool is able to exploratory-test previously unseen websites whilst handling reactive websites and events such as cookie/GDPR consents. We discuss design decisions as well as challenges and opportunities for further development. A demo URL is also provided. 2023-04-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/141715 Title: Centralized vs. decentralized monitors for hyperproperties Authors: Aceto, Luca; Achilleos, Antonis; Anastasiadi, Elli; Francalanza, Adrian; Gorla, Daniele; Wagemaker, Jana Abstract: This article focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralized monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation. 2025-01-01T00:00:00Z