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