Abstract
Software systems, especially cyber-physical systems, sense and influence real-world entities under the control of software logic in order to realize desired real-world behaviors. Such software systems are based upon three essential components: (1) a computing platform, (2) a set of physical entities with which the computing platform interacts, and (3) the relationship between the first two components. These three components seem familiar, and the third component seems trivial. In fact, the third component, the relationship, is crucial, because it defines how logical values read and produced by the computing platform will be affected by and will affect the various physical entities.
Formally, the relationship between real-world entities and a computer system’s logic is the interpretation of the logic. Software logic is necessarily formal, but, in practice, interpretations are usually documented informally and incompletely, and programmers treat elements in software logic as if they were the real-world entities themselves. As a result, faults are introduced into systems due to unrecognized discrepancies, and executions end up violating constraints inherited from the real world. The results are software and system failures and adverse downstream consequences.
This dissertation argues that, to mitigate such risks, software engineers should produce not just traditional software, but a new engineering structure, the interpreted formalism. The structure combines software logic with an explicitly documented interpretation. Among other things, an interpretation documents differences that arise inevitably between real-world values and corresponding logic values. An interpreted formalism provides centralized documentation of a system’s software and its intended relationship to the real world in an analyzable form, facilitating fault detection.
An implementation of the interpretation, real-world type, is introduced. For a specific software system, an interpretation is composed of a set of real-world types, and an interpreted formalism is implemented as a real-world type system combined with a software system.
The pragmatics of the interpreted formalism concept are illustrated by conducting case studies on open-source software systems of different sizes. The interpreted formalism is evaluated from several viewpoints: (a) overall feasibility, (b) error detection capability, (c) effort level required, and (d) scalability. The results of the case studies suggest that (1) the interpreted formalism concept can be used on modern software systems of different sizes, (2) the technology is capable of detecting real errors that violate real-world constraints, and (3) the effort required from engineers for developing and using the interpreted formalism can be reduced greatly by an automated synthesis framework developed as part of this research.
