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

代码驱动机器人、航天器、武器系统和更广泛的网络物理系统与世界互动。然而，在大多数情况下，代码由去除了真实世界语义的机器逻辑组成。这意味着计算机无法阻止代码中指定的操作违反从物理世界继承的物理约束。传统的编程语义学可以告诉我们，表达式3.0+4.0意味着7.0，因为7.0是对该表达式求值的结果。但我们的编程语义学的传统概念并没有解决问题，3个什么，4个什么，或者7个什么，或者这样的总和是否有任何物理意义。例如，3米加4克在身体上是没有意义的。由于机器允许对没有明确物理含义的表达式进行求值，因此发生了重大系统故障。为了提高网络物理系统的安全性和可靠性，这个项目将开发和评估这样一个命题，即未来的软件代码应该包括机器逻辑与解释，这些解释将代码中的术语映射到它们预期的物理含义的形式规范，最终在程序执行中，以便可以自动检查代码与更大系统的物理意义的一致性。研究人员的目标是建立一种新的、正式的程序物理语义概念，其基础是将代码元素映射到精确表示物理世界中的对象和其他现象的数学量。拥有这样的映射将反过来支持评估代码与其预期的物理解释的一致性，从而显著提高系统的可靠性。该项目将通过将代码从代码级术语的解释映射扩展到可机械检查的有维度物理量的规范，如点和变换，从而为网络物理代码的物理语义奠定理论基础，这些规范在构造性逻辑证明助理的高阶逻辑中形式化。该项目将建立各种机制，使解释的构建大大自动化，从而能够对软件密集型系统进行实际的物理层面的分析和检查。它将通过研究指定和分析这种解释的方法来推动软件工程理论和实践，包括物理语义的自动推理机制、形式化的物理抽象库、强制对代码施加解释的系统，以及为测试、程序理解、系统集成和其他用例利用物理解释的方法。该项目将通过编写关于形式化物理抽象的教材和支持正在进行的基于使用构造性逻辑证明助手的本科生离散数学课程来促进教育。它将为网络物理系统的研究和软件工程方面的劳动力发展做出贡献。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.