The Value of Formalism

The value of formalism in software engineering—not least for cyber-physical systems—is palpable. As Robert Boyle wrote in 1666 [1]: “In pure mathematicks, he that can demonstrate well may be sure of the truth of a conclusion without consulting experience about it." A formal model allows reliable reasoning: mathematical proof of invariants and other formally stated requirements; confident evaluation and simplification of expressions; exhaustive checking of preconditions; simulation of a modelled executable process. These are not small advantages, and become hugely more powerful where good software tools are available. While avoiding the risk of logical fallacies, formal modelling also avoids also the pitfalls and obstacles—fuzzy phenomena, contingent physical properties, unexpected interactions, surprising physical effects, and hidden interferences—that characterise the governed world of a cyber-physical system.

Unsurprisingly, there is a price to be paid. The pitfalls and obstacles of the governed world cannot be exorcised by a formal utterance: perversely, they persist, ensuring that a formal model of the physical governed world can never be correct. The software engineering goal must be adequacy, not correctness. A model's fidelity to its subject does not embody timeless global truth, but adequacy to the conditions and purposes of its use. Achieving this adequacy is the work of a necessary practical discipline, not the QED of a mathematical proof. In the most demanding context—in a critical function of a critical system—three conceptual phases of model development can be identified: pre-formal, formal, and post-formal.

The pre-formal phase is an exploration of the governed world, captured in natural language. Natural language allows unfettered discovery because the evolving description can be continually modified and extended during the exploration. The set of primitive types can be enlarged; concepts such as causality and temporal sequencing can be conveniently introduced; higher-order statements can be added to a first order text. Only when substantial understanding has been achieved through such exploration can a language for formalisation be confidently chosen.

In the formal phase the axiomatic aspect of the governed world model is developed in the chosen formalism, describing the domain properties on which the machine will rely to ensure the desired behaviour in the world. Then the behavioural aspect is addressed, combining the axiomatic model with the software machine behaviour at the machine-world interface. Separating these two aspects avoids a potential confirmation bias. The axiomatic properties are first modelled without accompanying references to the specific intended behaviour. Then, they are instantiated in the specific setting of interaction with the machine.

In the post-formal phase the axiomatic and behavioural model aspects are critically audited for previously overlooked vulnerabilities in the physical governed world. For example, in some possible traces a necessary causal link may be disabled by a state value set in an earlier event. In another example, it may be belatedly recognised that a human participant—such as the pilot of an aircraft—may repeat an action often enough for the eventual result to cause a lethal failure.

Echoing Boyle, Herman Weyl [2] characterised the "decisive step of mathematical abstraction: we forget about what the symbols stand for." This amnesia is indeed the essence of formalism. But software engineers must remember.

[1] Robert Boyle; Preface to Hydrostatical Paradoxes made out by New Experiments, For the most part Physical and Easy, 1666.
[2] Herman Weyl; The Mathematical Way of Thinking; Bicentenial Conference, U Penn, 1940.

Links to other posts:
 ← Triplets: Triplets (Machine+World=Behaviour) are system behaviour elements
 ← Triplet Models: What models are needed of the machine and governed world?
 ← The ABC of Modelling: Axiomatic, behavioural, and consequential aspects

The ABC of Modelling

The machine program and the governed world model are the two parts of a simple constituent behaviour. Neither makes sense alone: they must be co-designed. The model describes the properties on which the program relies, defines the behaviour in the world, and shows that the behaviour results in satisfaction of the requirements. These are the Axiomatic, Behavioural, and Consequential aspects—the A,B,C of modelling-in-the-small. Although these aspects follow an obvious logical sequence, they too must be co-designed.

The axiomatic model describes the infrastructure of governed world domains—including the human participants—and the external and internal causal links they effectuate. A link is a causative temporal relation among domain states and events; the property of effectuating the link is imputed to a specific domain. Causal links connect the phenomena of the interface sensors and actuators to other phenomena of the governed world. They are axioms—unquestioned assumptions for designing the constituent behaviour: justified by the specific context and environment conditions for which the behaviour is designed and in which alone it can be enacted. Causal links are complex, usually having multiple effects and multiple causes; in general, effectuation of a link by a domain depends on domain and subdomain states. These and other complexities must be systematically examined and documented to fulfil the axiomatic promise of unquestioned reliability.

The behavioural model is a state machine, formed by combining the axiomatic model with the machine program's behaviour at the interface. The model should be comprehensible, both to its developers and to any human participant in the enacted behaviour—for example, a plant operator or a car driver. To take proper advantage of the reliability afforded by the axiomatic model, states and events of the model state machine should be justified explicitly by reference to causal links and their effectuating domains. The behavioural model defines the trace set of the behaviour: the set of exactly those traces over events and state values that can occur in an enactment of the behaviour. It must be possible to determine whether a putative trace—for example, a trace that contravenes a relevant requirement— belongs to the trace set.

The consequential model, based on the behavioural model, aims to show that all relevant requirements will be satisfied during the behaviour enactment. Satisfaction may be an obvious consequence of the behaviour, possibly with additional causal links and phenomena. It may need informal judgment or operational experiment—for example, of emotional and psychological reactions of human participants in the governed behaviour. It may need investigation and discourse outside the scope of software engineering—for example, of profitability or market acceptance. There are rich fields of activity here, but the primary focus of this blog is on the axiomatic and behavioural models. They are emphasised because they must reflect the fundamental competence of a software engineer—to predict, with high dependability, the governed world behaviour that will result from executing the developed software.

Links to other posts:
 ↑ Physical Bipartite System: The nature of a bipartite system
 ↑ System Behaviour Complexity: The component structure of system behaviour
 ↑ Reliable Models: Reliability in a world of unreliable physical domains
 ↑ Triplets: Triplets (Machine+World=Behaviour) are system behaviour elements
 ↑ Requirements and Behaviours: Requirements are consequences of behaviours

More than Physics

Between the machine and the governed world the sensors and actuators provide an Application Programming Interface—an API. Where is the API manual? You have to write your own, piecing it together from information about the infrastructure of the world—the physical domains and their properties and interactions. This manual will be an axiomatic model. It's axiomatic because it records the assumptions that you have decided not to question. It doesn't describe the machine or the governed behaviour: that is the role of a behavioural model that will rely on your axiomatic model exactly as a program relies on the programming language manual. The axiomatic model describes the physical domains and—crucially—their causal links in the governed world by which the desired behaviour can be woven together and connected to the API.

What can be assumed? What can be taken as axiomatic? The laws of physics, certainly. But they are far from sufficient. Physical laws say nothing of causality. For most reasoning about governed world behaviour their scale is either too small—particle physics—or too broad—conservation of energy. At the relevant intermediate scales physical domains are irregularly shaped and structured; they are mutable and richly connected, and each is host to the interacting effects of many natural causes. Abstractions of the domains and their causal properties are inescapably informal and imperfect: everything is approximate, and nothing is unconditionally true.

In short, the task in hand is engineering, not science: the scientist's scope is the universe, but the engineer's is a specific system, narrowly bounded in space and time. This narrow bounding gives a vital clue to addressing the difficulty of cyber-physical behaviour design: there must be many axiomatic models, and their scopes must be narrow. First, system behaviour is a structure of constituent behaviours. An approach based on triplets associates a distinct axiomatic model with each distinct behaviour: the assumptions are chosen only to support the associated behaviour, and are assumed to hold only while it is enacted. Second, each causal link is explicitly attributed to a specific effectuating domain of the governed world, reflecting the operational principle [1,2] of the behaviour design. This attribution focuses the search for threats to validity of the assumed link, and sharpens and enlivens analysis of potential and actual failures. Third, in the development task of combining concurrent constituent behaviours, their axiomatic models highlight the assumptions of each that may cause interference or conflict in combination. Fourth, a critical system must maintain operation in the face of increasingly adverse conditions. For each new adversity a different behaviour, often with degraded function, may be enacted: such degraded behaviours depend only on their newly reduced axiomatic assumptions. Unlike the universal laws of physics, axioms for engineering must be local.

The fundamental expression of an operational principle—how a designed behaviour works—is in its assumed causal links. Clarity about the assumed domain properties and links depends directly on a clear separation of axiomatic and behavioural models.

[1] Michael Polanyi; The Tacit Dimension, pp39-40, U Chicago Press, 2009.
[2] Michael Polanyi; Personal Knowledge, pp328-329, U Chicago Press, 1974.

Links to other posts:
 ↑ Not Just Physics: Software Engineering's unique view of the physical world
 ↑  Physical Bipartite System: The nature of a bipartite system
 ← Causality: Causality is the explanation of how a system works
 ← Triplets: Triplets (Machine+World=Behaviour) are system behaviour elements

Triplet Models

A triplet is a simple bipartite cyber-physical system in microcosm. Its two physical interacting parts are the machine M and the governed world W: the third part of the triplet is the behaviour B resulting from their interaction. The software engineer's obligation is to devise a governed behaviour B to satisfy the relevant requirements, programming the bipartite system to ensure that this behaviour is enacted by the system in operation.

This obligation demands good models of the machine and governed world. As in any creative task in the physical world, two distinct kinds of model are needed—often combined, obscuring the distinction. The first is an axiomatic model, describing the given properties of the governed world that will form the substance and context of the new creation. The second is a behavioural model, describing the behaviour of the governed world that will emerge from its interaction with the machine. The axiomatic model is the indispensable foundation for the behavioural model: the given properties it describes simultaneously enable and limit the possible behaviours.

For the machine M, the axiomatic model is—or should be—provided off-the-shelf by the hardware order code specification and the programming language semantics; the behavioural model is the program to be executed. This view holds for a machine-code program, a program in an abstract high-level language, and everything between. Elevating the machine models to a level incorporating abstractions far above—but never, of course, excluding—the machine's ports and physical interfaces may seem obvious today; but it is possible only because computing machinery has advanced far towards the unattainable twin goals of perfect reliability and perfect formality. In some settings, these near-perfections have allowed computer programming to become more abstract, sharing much with mathematics and logic.

The governed world too needs axiomatic and behavioural models; but the physical world's character—unlike the machine's—is inherently non-formal and unreliable. These imperfections makes it hard to find firm ground on which to build the axiomatic model of the governed world that is essential to a reliable behavioural model—that is, to support dependable governed behaviour in the world. The primary obligation of software engineering in a cyber-physical system is to develop behavioural models from which the triplet system's behaviour in the given physical world can be predicted with justified confidence. Where, then, can we base an axiomatic model on which a reliable behavioural model can be based? The nature and development of an axiomatic model of the governed world of a triplet is a topic that demands another post.

Links to other posts:
 ↑ Triplets: Triplets (Machine+World=Behaviour) are system behaviour elements
 ↑ Models: Types and purposes of models of the physical world
 → The Right-Hand Side: Why the model-reality relationship is problematic
 → Axiomatic Models:  Capturing basic assumptions for a behaviour

Causality

Causality is a difficult concept. For a lawyer[1]: did the accused cause the death of the deceased? For a health scientist[2]: does eating red meat cause cancer? For a philosopher[3]: can we reason reliably about necessary and sufficient causes? And for a physicist[4]: was Newton's concept of force a euphemism for the concept of cause that he rejected?

These are difficulties of defining causality and providing a consistent theory and a logic. Software engineers commonly use causal links in models. A state transition from Si to Sj labelled "e1/a3" means that in state Si the event e1 causes both the action a3 and the transition to state Sj: the causal link is implicit in the state-machine formalism. A recent paper [5] reviews some explicit treatments of causality in cyber-physical systems.

For us, the axiomatic model of a triplet's governed world is composed of causal links. Just as a computer's physical semantics define its behaviour in program execution, so the axiomatic model defines the governed world's behaviour in interaction with its triplet's machine. Cause-effect transmission in these axiomatic links is what allows machine behaviour at the sensors and actuators to govern behaviour in the real world.

The basic elements of a causal link are a cause phenomenon, an effect phenomenon, and a physical domain whicheffectuates the link—that is, the domain ensures that when the cause occurs the effect follows. For example, the domain may be an electric motor, the cause an event applyPower, and the effect motorRotating. The cause and effect phenomena are both phenomena in which the effectuating domain participates, and may independently be internal or external phenomena of the domain.

Causality is an informal abstraction. We do not attempt to build a formal logic for it, because its elements do not have the required characteristics: nothing is atomic; no property is mathematically certain; all definitions stumble on hard cases and counterexamples. Nonetheless, in developing and understanding system behaviour, the informal concept provides an essential tool. A causal link poses a bounded question: will this link be effectuated?

The effectuation of a causal link is always contingent. At a finer granularity, the structure of the domain can be seen, and the link itself appears as a chain of sublinks, each contingent on the state of its effectuating subdomain. If the power supply is overloaded, or the winding of the electric motor is burnt out, or the shaft bearing is distorted, the motor will not rotate. These disabling states can be brought about by previously effectuated links, reflecting the rich connectivity of the physical world. The concurrency introduced when behaviours are combined to give the whole system behaviour is another potential source of disabling conditions.

If causal links are so contingent, and so problematical, and so vulnerable, why are we relying on them? We rely on them because they form the axioms—the governed world properties—on which the triplet behaviour design will rely unconditionally. The causal link abstraction bounds the checking of these axioms: each link is the smallest element of system behaviour, in one constituent behaviour. If the system fails, the failure can be initially located at a causal link that should have been—or should not have been—effectuated, and pursued from there along the structures of causal chains that implement the system's operational principle.

[1] Joseph Y Halpern; Actual Causality; MIT Press, 2016.
[2] J L Mackie; The Cement of the Universe: A Study of Causation, Oxford University Press, 1974.
[3] Judea Pearl and Dana Mackenzie; The Book of Why: The New Science of Cause and Effect; Penguin, 2018.
[4] David Bohm; Causality and Chance in Modern Physics; Taylor and Francis, 2005.
[5] Ibrahim et al; Practical Causal Models for Cyber-Physical Systems; in Proc NASA Formal Methods Symposium, 2019.

Links to other posts:
 ← Triplets: Triplets (Machine+World=Behaviour) are system behaviour elements
 → Axiomatic Models:  Capturing basic assumptions for a behaviour