We develop a theoretical framework for thinking about systems in complex human contexts and the problem of explaining their behaviour. Structurally, systems are made of modular and hierarchical components that we abstract in a general system model using notions of modes and mode transitions . A mode is an independent component of the system with its own objectives, monitoring data, and algorithms. The behaviour of a mode, including its transitions to other modes, is determined by functions that interpret each mode’s monitoring data in the light of its objectives and algorithms. We show how these belief functions can help explain system behaviour by quantifying and visualising their evaluation of monitoring data as trajectories in higher-dimensional geometric spaces. These ideas are formalised mathematically by abstract and geometric simplicial complexes . We offer three techniques—a framework for design heuristics, a general system theory based on modes, and a geometric visualisation—and apply them in examples of three types of human-centred systems.
Formal methods have long promised enhanced software reliability through rigorous mathematical reasoning, yet concerns over scalability, cost, and accessibility have historically limited their industrial adoption. This paper critically evaluates the public record on the use of formal methods in engineering at Amazon Web Services (AWS). Drawing on publicly available case studies, engineering reports, and technical documentation, we examine reported applications of model checking, SMT solving, and lightweight formal methods across domains such as distributed systems, cloud networking, cryptography, and security policy verification. We organise the analysis around 16 targeted questions across five themes: (1) technical impact, (2) organisational adoption, (3) scalability in complex and heterogeneous systems, (4) long-term strategic value, and (5) future directions. By placing these AWS case studies alongside historical precedents at companies such as IBM, Microsoft, and Google, we highlight both continuity and innovation in industrial practice. Across the published case studies, authors report benefits such as early bug detection, performance optimisation, and strengthened security assurance, including integration with CI/CD workflows in some settings. However, the evidence base is selective and does not support organisation-wide claims about prevalence, cost-effectiveness, or ROI; quantitative baselines are sparse, and survivorship bias is plausible. We discuss the resulting methodological limits, highlight challenges such as maintaining specifications under continuous evolution, and outline a research agenda to improve empirical validation, methodological refinement, and the preservation of industrial verification artefacts.
Malware analysis represents a difficult task due to its ever-changing nature, where attackers invent new techniques for avoiding or counter-attacking analysis and prevention mechanisms. During fast-response investigations, a vital element is extracting or checking information, in order to take proper action. One key aspect that is currently missing, in a general sense, is a system which security researchers can query in order to obtain a quick verdict about the capabilities of a malware. The proposed solution is a framework for formal analysis of applications’ behavior, called Formal Tainting-Based Framework, that uses a combination of binary instrumentation, taint analysis, and runtime verification in order to selectively extract behavioral properties of a malware. These are then formalized in order to check if the application expresses certain capabilities. The formal aspect also represents a significant contribution, as we introduce a specific temporal logic, which overcomes obstacles for expressing program events. The findings are accompanied by a concrete implementation, which proved effective and efficient against real-life malware, as highlighted by an evaluation. Furthermore, the framework has been evaluated in realistic cyber forensics scenarios, demonstrating its potential to assist security researchers by reducing analysis time and effort.
Starting from Gurevich’s New Thesis that every computational device can be simulated by an appropriate dynamic structure , the article describes the development of the Abstract State Machines (ASM) method in theory and practice. ASMs, originally called evolving algebras , provide a computation model on structures capturing arbitrary algorithms—understood very generally to comprise all computation systems—on arbitrary levels of abstraction. The theoretical investigations have resulted in a variety of behavioural theories showing that a particular class of algorithms (or algorithmic systems) is captured by some well-defined class of ASMs. Most importantly, the theories capture the classes of sequential, recursive, synchronous parallel, concurrent and reflective algorithms. Each such class gives rise to an associated ASM logic that enables reasoning over properties of states and state transitions. These logics have been proven to be complete, and recent research resulted in complete temporal extensions. Furthermore, specific subclasses of ASMs have been discovered that capture algorithms solving problems in certain complexity classes. The application-oriented investigations have led to a large variety of rigorous specifications including correct and complete refinements and the verification of desired system properties. This includes among others proofs of compiler correctness for various languages, specification and verification of web browsers, specifications and verification of ambient systems, specifications and verification of hybrid systems, and specifications of reflective programming languages. The seamless coupling of deep theory and rigorous scientific practice enables the targeted analysis of rigorous specifications and the systematic reification on target platforms.
In 1980 Tony Hoare received the ACM Turing Award “for his fundamental contributions to the definition and design of programming languages”. This article examines the achievements that led to this award.
Recently a divergence-sensitive branching bisimilarity has been proposed and studied for the randomized CCS model. In this article, we give an equivalent inductive characterization for the bisimilarity, which is a probabilistic extension of the previous work on the non-probabilistic model. Based on the new characterization, a novel polynomial-time verification algorithm for the divergence-sensitive branching bisimilarity is proposed.
The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this article, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.
It all began at the IBM L 1973–1974. I will reminisce of how VDM, the Vienna Development Method, emerged. We were to develop a compiler for PL/I. In Feb. 1974 IBM HQ curtailed this and related projects. So three of the co-developers of VDM went abroad. Peter Lucas to the US, Cliff Jones via Brussels back to the UK, and I to Denmark. With students and later, at Dansk Datamatik Center (DDC), we then developed compilers for CHILL and Ada according to the IBM Lab. Vienna ideas. They led to the design of the RAISE (Rigorous Approach to Industrial SE) Method—with RSL (the Raise Specification Language). As UN Director of the UN University’s Intl. Inst. for Software Technology, in Macau, 1991–1997, we pursued Formal Methods and their theoretical underpinnings, and applied Formal Methods to the development of systems for railways (in China), finance ministry (Vietnam), country wide telephone system (The Philippines), multi-script documents (for Mongolia), and so on. I will survey these projects – emphasizing how Domain Modeling emerged. I will then outline recent work, since my retirement, at age 70 in 2007, in Domain Science and Engineering. I will end the article by “revealing” my “emergence” as a scientist from being an engineer/researcher.
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.
Reactive systems, which maintain ongoing interactions with their environment, are typically modeled using ω-regular languages. These languages characterize system behavior with infinite-length execution traces and are represented as nondeterministic Büchi automata (NBAs) or ω-regular expressions. Existing methods for synthesizing expressions from NBAs only handle state-based acceptance. This limitation forces the conversion of compact transition-based NBAs into larger state-based NBAs before synthesis. This article introduces the first direct synthesis method for ω-regular expressions from transition-based NBAs, eliminating the need for this transformation. The method works by decomposing an NBA into triplets of nondeterministic finite automata, subsuming existing pair-based decompositions to handle transition-based acceptance. We prove that our decomposition is correct, establishing our method’s soundness and completeness. We discuss the time and descriptional complexity of our method. Our empirical evaluation on 185 linear temporal logic formulas supports our hypothesis; transition-based synthesis reduces postfix size by 4.1× and 1.5× for recurrence and reactivity properties, respectively. We also analyze the structural NBA factors that determine when the transition-based NBA will yield a more compact expression and develop this into a simple criterion that, when applied, yields expressions that are at least as compact as those obtained by direct state-based synthesis.
This article gives a historical overview of the background, motivation and development of μCRL and its successor mCRL2, from the inception to the present. Both mCRL2 and μCRL are similar, compact, but very expressive formalisms based on process algebra, term rewriting, and the modal mu-calculus. They are developed to model and analyse the behaviour of interacting systems, i.e., systems that communicate by exchange of messages, among each other and with the outside world. Every contemporary computer system can be viewed as such an interacting system and their communication schemes are difficult to design correctly. By sticking to the mathematical foundations, but being led by the desire to be practically relevant, the formalism has grown to become very versatile. In particular, mCRL2 does not only foster the development of theory and the formulation of correctness proofs, but it is also the basis of a large set of automatic tools that help to provide insight in the behaviour of complex computer controlled systems.
We present a framework for the formal modeling of state-based systems in the context of the Lean4 programming language and proof assistant. In this context, the main objective is to support a step-wise refinement methodology inspired conceptually by the Event-B formal method. As a starting point, the LeanMachines framework proposes Lean4 constructions for the main Event-B concepts such as contexts, machines and events. Most importantly, the associated refinement principles are introduced in the form of typeclass constructions inspired by (and in fact built upon) the Mathlib mathematical framework. Beyond the basic concepts and structures, we also experiment with extensions of the framework. First, we develop an algebra of event combinators that allow to compose complex event structures out of simpler ones. These combinators are based on algebraic structures – functors, arrows, etc. – that have been developed and studied in the context of (functional) programming language theory. Our proposed formalization of the Event-B concepts is very shallow in the sense that all the constructions are directly based on the Lean4 logic and abstractions. One benefit is that proof obligations can be discharged using the tactic language of Lean4 with almost no embedding overhead such as an abstraction barrier that would require syntactic conversions, or the necessity to use some dedicated proof tactics. As an important design guideline, we enforce the fundamental principle of correctness-by-construction: machine states, events structures and refinement steps cannot be fully constructed without discharging the prescribed proof obligations.
We describe the input/output automaton model, a model for concurrent and distributed discrete event systems. We define the model, illustrate the model with several examples concerning vending machines and a leader election algorithm, and survey the ways in which the model has been used. 1 , 2
Jean-Raymond Abrial (6 November 1938 – 26 May 2025), one of the founding figures of modern formal methods in computer science, passed away at the age of 86. His contributions laid the groundwork for mathematically rigorous software development, and his influence spans generations of researchers, engineers, and educators worldwide.
We explore the contributions of Alfonso Caracciolo di Forino, 1925–1996, to the creation of a school of formal methods in Italy, focusing on the problem of the formal definition of programming languages, including the semantic and pragmatic levels. In particular, we present his search for metalanguages and methods that could be used to give a “declarative definition” of a programming language. This research led him to the introduction of Generalized Markov Algorithms (GMAs), which extend Markov’s Normal Algorithms with metalinguistic variables, computable functions, and conditional applicability. For Caracciolo, a language definition was a GMA that, given a string, either rejects it if it is not a legal program or gives its meaning as a state-transforming function, thus taking care of the syntax (both context-free and context-dependent aspects) and semantics of the language, including non-terminating computations. Caracciolo’s group applied GMAs to several language definitions, to a complete simulation of the formalism used by the IBM Vienna Research Center to define PL/I, and, more generally, to the definition and simulation of dynamical systems. We contextualize these contributions in the Italian computing environment of the late 1950s and 1960s.
We carry out an analysis of message-passing concurrency primitives, namely a synchronous channel and an alt (alternation) construct, implemented in Scala. We model these primitives using the process algebra CSP, and analyse them using the model checker FDR. We consider the correctness properties of synchronisation linearisation (informally, that each completed operation execution corresponds to a correct synchronisation) and progressibility (informally, that executions don't get stuck if they could synchronise): we show how these properties can be captured in CSP. Our initial analysis discovered an error in a previous implementation; our subsequent analysis helped us to produce a correct implementation. It turns out that a direct analysis of the composition of an alt and corresponding channels scales quite poorly. To overcome this, we perform a compositional analysis: we show that a channel and an alt each satisfies a more abstract description; and show that the composition of these abstract descriptions satisfies synchronisation linearisation and progressibility.
