SHF: Small: Explicating and Exploiting the Physical Semantics of Code

University Of Virginia Main Campus, Charlottesville VA

Investigators

Abstract

Code drives robots, space vehicles, weapons systems, and cyber-physical systems more generally, to interact with the world. Yet in most cases, code consists of machine logic stripped of real world semantics. This means that there is no way for the computing machine to prevent operations specified in code from violating physical constraints inherited from the physical world. Traditional programming semantics can tell us that the expression, 3.0 + 4.0 means 7.0, in the sense that 7.0 is the result of evaluating that expression. But our traditional conception of programming semantics does not address the questions, 3 of what, 4 of what, or 7 of what, or whether such a sum makes any physical sense. For example 3 meters plus 4 grams does not make physical sense. Major systems malfunctions have occurred due to the machine-permitted evaluation of expressions that have no well defined physical meanings. To improve the safety and reliability of cyber-physical systems, this project will develop and evaluate the proposition that the software code of the future should comprise machine logic paired with interpretations that map terms in code, and eventually in program executions, to formal specifications of their intended physical meaning so that the consistency of code with the physics of the larger system can be automatically checked. The investigators aim to establish a new and formal concept of the physical semantics of programs based on interpretations that map code elements to mathematical quantities that precisely represent objects and other phenomena in the physical world. Having such mappings will in turn support the evaluation of code for consistency with its intended physical interpretation, enabling significant improvements in system dependability. This project will establish theoretical foundations for physical semantics of cyber-physical code by augmenting code with interpretation mappings from code-level terms to mechanically checkable specifications of dimensionful physical quantities, such as points and transformations, formalized in the higher-order logic of a constructive logic proof assistant. This project will establish mechanisms to substantially automate the construction of interpretations to enable practical physics-level analysis and checking of software-intensive systems. It will advance software-engineering theory and practice by investigating means for specifying and analyzing such interpretations, including mechanisms for automated inference of physical semantics, libraries of formalized physical abstractions, systems to enforce interpretations imposed on code, and means for exploiting physical interpretations for testing, program understanding, system integration, and other use cases. The project will contribute to education by developing teaching materials on formalized physical abstractions and by supporting the ongoing development of a discrete mathematics course for undergraduates based on the use of a constructive-logic proof assistant. It will contribute to workforce development in research and in software engineering for cyber-physical systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.