Data are increasingly released for secondary use, yet identity disclosure remains a persistent concern even after standard de-identification. Disclosure risk often arises not from isolated attributes, but from the relational structure of a release design and its interaction with external information. Statistical guarantees and empirical testing may therefore fail to expose structural risks at design time. This paper treats identity disclosure as a design-level relational property. We model data schemas, de-identification policies, and re-identification assumptions as explicit relations. Disclosure is reduced to a bounded relational reachability problem and analysed using Alloy as an executable verification engine. Satisfiable instances produce concrete disclosure witnesses, while unsatisfiability establishes bounded non-disclosure within the analysed scope. A healthcare-inspired setting illustrates that disclosure can emerge purely from relational composition, even when conventional criteria are satisfied. By recasting identity disclosure as a verifiable relational property, this work complements statistical privacy models with assumption-aware design-time verification. This reframing enables disclosure to be verified at design time, prior to data release.
Formal verification of autonomous systems is well established for safety and liveness analysis, yet the explicit modelling and verification of adversarial behaviour at the system level remains limited. In particular, attacker behaviour is often encoded implicitly, obscuring the distinction between attacker capability and system response. This paper presents a security-minded, state-based modelling approach in which the system and the attacker are represented as separate transition systems that interact exclusively through shared inputs. This separation preserves semantic clarity, enables compositional reasoning, and supports rigorous security analysis using standard model-checking techniques. The approach is demonstrated on an autonomous space docking system. An attacker transition system is systematically derived from CAPEC-148 (Content Spoofing) and models image-spoofing attacks against a vision-based navigation subsystem. Security countermeasures are modelled as constrained variations of the system transition semantics. Security properties are specified in LTL and verified using the SPIN model checker. The results show that explicit separation of system and attacker transition systems enables the identification of insecure configurations and the formal verification of mitigation effectiveness, providing design-time security assurance for autonomous systems.
Spectabular is a model-based specification and analysis tool supporting tabular specifications. These allow specifications to be written naturally by considering cases and to be checked for totality, disjointness, definedness, possibility, and necessity. Tabular specifications are intended to be read and checked by domain experts. Spectabular is used to model and analyze the adaptive exterior light automotive case study proposed for ABZ’20.
We present a partial formal analysis of the ABZ 2026 planetary rover case study, focusing on abnormal scenarios and failure-handling behavior. From a space-systems engineering perspective, we first identified representative abnormal scenarios through what-if analysis and then formalized the relevant interactions among goal reasoning, planning, map validation, communication, and recovery-related components in Quint as a shared-state transition system. We analyzed this model through simulation and bounded verification, which revealed several specification issues and ambiguities, including a gap in the interruption semantics of safe-location instructions and underspecified decision criteria in failure handling. We also explored a focused Event-B model of the FailureMode component as a complementary analysis. The study shows how lightweight formal modeling can help domain engineers clarify abnormal behavior in an autonomous space-system specification.
Lock-free data structures are notoriously difficult to design and implement correctly. The absence of critical sections protected by synchronization primitives makes reasoning much harder, often leading to almost unreproducible bugs and subtle errors. All of these can be systematically addressed using formal methods. We use TLA+, a state-based formal method especially suitable for working with concurrency, to verify SALSA, a scalable and low synchronization NUMA-aware algorithm for producer-consumer pools. The task pool was considered as part of a redesign phase of inter-process communication in a microkernel-based operating system under development. During this work, we uncovered numerous issues with the algorithm, from small typos in the pseudocode to significant design flaws. The work was completed in two person-months and resulted in a decision to abandon this task pool in favor of a more traditional lock-free queue. This potentially saved us many more months of development and debugging and advanced formal verification use within the company.
Autonomous systems are increasingly required to comply with ethical norms and human values, motivating the need for rigorous methods to specify and analyze ethical requirements. Social, Legal, Ethical, Empathetic, and Cultural (SLEEC) rules provide a structured means to encode such requirements; however, ensuring their correctness and well-formedness calls for formal specification and systematic, tool-supported analysis. This paper presents an approach based on Abstract State Machines (ASMs) and the ASMETA tool set for the formal specification and well-formedness analysis of SLEEC requirements. We formally define the semantics of the SLEEC domain-specific language, enabling systematic validation of SLEEC models through conflicts and redundancies detection. Moreover, we extend the core when–then–unless structure of a SLEEC rule with response delays and with a clause unless–until to support the temporary suspension of a rule. The validated ASMETA-based SLEEC model is directly executable and can be readily adopted as a runtime model to support the subsequent phase, namely the operationalization of ethical requirements in autonomous systems.
The healthcare sector is increasingly recognising cybersecurity as an integral part of patient safety. In recent years, healthcare computer networks have been severely affected by numerous large-scale cyberattacks that have exposed fundamental security gaps in network architectures. As a result, governments and regulatory organizations have introduced comprehensive cybersecurity standards and cyberdefense strategies for healthcare infrastructure. In this paper, we develop a security requirements specification for a healthcare computer network and present a combined approach to formally model and verify it using Alloy and TLA ^+ . With Alloy, we analyse the structural constraints, which include network segmentation, the security lattice, and access control rules. In TLA ^+ , we verify temporal correctness properties, with particular emphasis on dynamic reconfiguration, state-based monitoring, and the isolation of critical devices during cyberattacks. By integrating two state-based methods, we demonstrate how both static and dynamic security properties can be analysed within a unified framework, enabling the formal verification of cybersecurity requirements for critical infrastructure.
The current state of art lacks a methodical, rigorous and scalable single approach to analysis of safety and security requirements. We present SHARCS (Systematic Hierarchical Analysis of Requirements for Critical Systems), addressing this gap by adopting an abstraction-based incremental approach to hazard analysis. SHARCS combines STPA-style control action analysis with Event-B formal modeling and refinement to analyze safety and security of cyber-physical systems by flowing down system-level requirements to component-level requirements. This paper summarizes our recent journal publication [6] with emphasis on two key contributions: (1) a systematic three-phase workflow (system level, component level, consolidation) that guides the incremental development process; (2) control abstraction diagrams, a novel visual notation for modeling control structures at different abstraction levels before concrete design. We demonstrate SHARCS on the Tokeneer secure enclave system, showing how these contributions enable scalable hierarchical decomposition with rigorous traceability.
Decentralized Autonomous Organizations (DAOs) manage governance and financial processes through blockchain-based smart contracts, posing significant challenges in specification, implementation, and verification. While visual and model-driven approaches support DAO design, they lack integrated formal verification and reliable code generation mechanisms. In this short contribution, we outline our long-term research vision aimed at integrating visual DAO specification with formal verification based on Abstract State Machines (ASMs). The proposed approach supports the verification of governance properties before deployment, thereby reducing the risk of vulnerabilities in smart contracts and enhancing assurance guarantees for stakeholders.
Partial-order reduction (POR) is a technique for tackling the state-space explosion problem in model checking. The search space can be significantly reduced by disabling certain events at the state level. Recent research has brought to light issues in the theory behind several POR approaches. In this work, we demonstrate a method for rigorously testing the soundness of POR theories using Alloy, a SAT-based formal specification tool. We apply this method to several POR theories and formalisms. To explain the modelling challenges that we faced, we show two Alloy models in detail. In our experiments, Alloy manages to produce counterexamples to all theorems that we know to be flawed. This indicates that our ideas are viable for preventing comparable issues in the future development of POR methods.
Model-driven development enables collaborative design across heterogeneous modelling domains, but it also raises the risk of inconsistent models. We study the problem of extracting minimal submodels that preserve cross-domain consistency. Concretely, given two sets of models related by a consistency specification and a model from the first set, we seek an equiconsistent slice, that is, a submodel that preserves the same consistency relationships with models of the second set. Since the definition of equiconsistency quantifies over the complete second set, a direct computation is infeasible (and undecidable in general). Thus, we formulate slicing as a declarative synthesis problem and solve it using counterexample-guided inductive synthesis (CEGIS). The procedure iteratively proposes candidate slices and refines them using counterexamples (models obtained as violation witnesses if a candidate is not a valid slice). Iterating the CEGIS loop converges to equiconsistent, minimal slices within the bounds used by the model finder. We instantiate the abstract equiconsistency slice problem using attributed typed graphs as models, express consistency relations declaratively, and further realize it using relational logic and SAT-based solving. We then obtain an automated synthesis of equiconsistent slices based only on the consistency relation. We evaluate the method on a synthetic dataset to compare three CEGIS implementations: an explicit loop in Alloy, an explicit loop in Alloy*, and a quantified encoding in Alloy*. We highlight their practical trade-offs.
Open Radio Access Networks (O-RAN) aims to transition telecommunication networks from vendor-specific hardware to open, virtualised control architectures. As interest grows in deploying O-RAN in non-terrestrial networks (NTNs), understanding the robustness of its protocol specifications becomes critical. This paper reports on the formal modelling of the stable O2 O-RAN interface specification using the Alloy modelling language. We encode ten representative operational scenarios from the O2 specification and formalise safety and feasibility properties relevant to deployment constraints. Bounded model checking reveals several classes of specification weaknesses, including underconstrained pre/post conditions, ambiguous sequencing of protocol steps, and conflicting simultaneous triggers that permit inconsistent system states or violate intended progress conditions.
We explore the application of Constraint Programming (CP) tools to modelling state-based systems and verifying their properties. This includes finding execution traces leading to a particular state, and proving deadlock-freedom up to a given bound on the number of transitions. We present three distinct case studies. The first formulates a railway signal in the Essence CP modelling language, demonstrating use of Essence types and operators to model states, transitions, and invariants, in a system with a single finite-state automaton. The second case study is based on Dining Philosophers, and demonstrates effective CP modelling of a system with a large number of automata, synchronised on transitions. The third case study is part of the Alpha Algorithm, an example from swarm robotics. It introduces a clock, and has transitions with guards that refer to the clock. It also has triggers, representing sensor inputs, and non-deterministic waits, demonstrating that these concepts can be represented in a CP model. Finally we demonstrate that the CP approach is complementary to a model checking approach using FDR4. In many cases the CP approach can scale substantially better than the model checker, despite the CP toolchain being general-purpose, i.e. not explicitly designed for verifying properties of state-based models.
Current formal verification practices for autonomous systems often develop in isolation from diverse stakeholders who interact with, operate, or are affected by these systems. Although formal methods excel at providing mathematical guarantees, they often fail to address the broader ecosystem of requirements and perspectives that determine real-world acceptance. This vision paper argues for human-centred formal verification that embeds stakeholder engagement throughout the verification lifecycle. We propose a framework that maintains rigour while ensuring that verification processes are accessible, inclusive, and responsive to stakeholder needs. Our approach addresses the gap between technical correctness and stakeholder confidence through participatory specification development, multi-perspective verification processes, and stakeholder-appropriate result communication. This is a vision paper presenting a research agenda with technical details left to future work, aiming to advance discussion on integrating formal rigour with socio-technical stakeholder needs.
The Belief–Desire–Intention (BDI) paradigm is a popular framework in the development of autonomous systems. However, assuring the correct design of BDI agents remains difficult: existing modelling formalisms often require ad-hoc encodings of BDI agents that can be difficult to validate, maintain, and reason about. This paper focuses on modelling the syntax of BDI agents and shows how algebraic modelling in Event-B theories (e.g. inductive data types and polymorphic constructors) yields a faithful, compact, and reusable encoding of BDI syntax. Even without committing to the full BDI semantics, the encoding already supports useful reasoning, including belief entailment and belief-based invariant checking, and provides a path towards a future BDI semantic encoding via operators in theories and machine events in Event-B.
Specifications of modern complex systems can become so large that model cutting or abstraction is required to enable automatic analysis by model checkers. Moreover, relying solely on model simulators or scenario-based validation does not provide sufficient guarantees regarding the model’s compliance with requirements or its satisfaction of desired properties. Building on the idea of code fuzzing and leveraging the executability of models, this paper introduces a model fuzzing approach for Abstract State Machine specifications developed in ASMETA. The supporting tool, specified in ASMETA, enables randomized executions of models with the aim of triggering unexpected behaviors such as crashes, assertion failures, or security vulnerabilities. To evaluate our approach, we consider two well-known case studies from the literature, one from security protocols and one from concurrent systems, to demonstrate its analysis capabilities.
Parallelism is a key semantic feature of Abstract State Machines (ASMs), represented in the Asmeta tool set by the par construct, which enables synchronous execution of multiple rules. While its theoretical importance is firmly grounded in the ASM formalism, which models synchronous updates through parallel rule execution, an evaluation of its real usefulness in real-world models has received limited attention. This paper presents an experimental study evaluating how and when parallelism is effectively used in Asmeta. We analyzed existing specifications to measure the adoption of the par construct, and generated sequential variants replacing par with seq to compare behavior through randomized test suites. Our findings show that par is widely adopted and useful: it rather frequently produces results different from those obtained by sequential execution.
This document summarises the ABZ 2026 case study challenge. The system under consideration is that of an autonomous planetary rover. We summarise the architecture for the rover, its requirements and the tasks that participants in the case study track should focus on. We also outline several extensions that may be considered in future work or that offer other perspectives for formal modelling and verification.
Formal modeling languages provide strong support for the specification, analysis, and validation of cyber-physical systems, but their adoption in practice is often hindered by the effort and expertise that are required to produce correct and complete models. In this paper, we investigate whether Large Language Models (LLMs) can support the modeling process by assisting in the generation and refinement of ASMETA specifications from natural language requirements. We propose an iterative and human-in-the-loop workflow in which an LLM is used to derive an initial ASMETA model, progressively refine it, and support scenario-based validation using existing ASMETA tools. The approach explicitly combines automated assistance with human inspection to mitigate modeling errors and potential biases introduced by the LLM. We evaluate the feasibility and effectiveness of this workflow through a case study based on the ABZ 2026 planetary rover problem, using GPT-5.2, accessed via the ChatGPT interface and leveraging the Projects functionality to support persistent and multi-iteration interactions. Our experience suggests that LLMs can significantly lower the entry barrier to formal modeling and support engineers by accelerating the creation of analyzable ASMETA artifacts, but expert oversight is necessary to ensure correctness, completeness, and alignment with stakeholder intent.
Systems deployed for long periods of time in dynamic environments may experience performance degradation that affects timing guarantees, even when their functional behaviour remains unchanged. In the design and verification of critical systems, such timing guarantees are often expressed using Metric Temporal Logic (MTL). Under degradation, these specifications may no longer hold as stated, although weaker variants that relax timing bounds may still be satisfied and remain meaningful. For example, while an elevator may initially be required to arrive within 30 s of a request, degradation of its motor may only allow us to guarantee arrival within 60 s. Although weaker, this guarantee is still useful and allows the system to maintain a reasonable level of operation. In this paper we present CEGIW, an iterative, counterexample-guided algorithm for automatically weakening timing intervals in MTL specifications so that they hold for a given system model. The algorithm preserves the logical structure of the original specification and weakens only interval bounds. We prove the correctness and optimality of CEGIW, and conduct an empirical evaluation to demonstrate the practicality of interval weakening using formalised requirements from a number of real-world case-studies. Using a model checker to produce counterexamples, CEGIW either identifies the strongest interval weakening under which the specification holds, or determines that no such weakening exists.
