The Physical Semantics of Code

Numerous mishaps involving cyber-physical systems have occurred due to divergences between software representations of the physical world and the actual phenomena be- ing represented. An example is the failure of the Mars Polar Orbiter mission due to the fact that a physical impulse was calculated in two different unit systems: impe- rial and metric[1]. This error manifested the problem that a complete and explicit representation of physical quantities is often stripped from code. The problem in such cases is that software is over-abstracted and thus becomes under-constrained in its behavior. Such systems can perform operations without type errors that have no physical meaning, leading to the production of values that can cause major malfunc- tions. Modern compilers provide type-checking, but physical type errors, by which we mean operations that are inconsistent in the world represented by the software, elude ordinary type checking. This thesis contributes to recent work on imbuing soft- ware with physical semantics through the provision of separate, formal, computable interpretations that map terms in code to enriched entities in the language of mathe- matical physics. Unique to our approach is the use of a higher-order constructive logic proof assistant to formally represent the physical domain. We present an initial proof of concept system that mostly automatically constructs interpretations by mapping terms in C++ code that represent physical quantities to enriched terms expressed in the language of the Lean Prover. Type checking in this domain then reveals physical type errors. A human analyst provides information needed to complete this mapping. In our work to date, this information specifies distinct vector spaces to which differ- ent vectors represented in the code are assumed to belong. Lean’s type checker then detects undefined operations involving vectors in different spaces. By augmenting cyber-physical systems code with physical semantics, we show that it is possible to detect physical type errors that cannot be detected by ordinary type checking. To help develop and to evaluate our concepts we developed a prototype system that finds and constructs interpretations of vector values and operations in C++ code.