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