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

SHF：小：解释和利用代码的物理语义

• 批准号: 1909414
• 负责人: Kevin Sullivan
• 金额: $ 51.5万
• 依托单位: University of Virginia Main Campus
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1909414&HistoricalAwards=false
• 关键词: SHF; Small; Explicating; Exploiting; Physical

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.

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

项目成果

A Novel Web-Based and Mobile Application to Measure Real-Time Moral Distress: An Initial Pilot and Feasibility Study

一种新颖的基于网络的移动应用程序来测量实时道德困扰：初步试点和可行性研究

• DOI: 10.1016/j.jcjq.2023.05.005
• 发表时间: 2023
• 期刊: The Joint Commission Journal on Quality and Patient Safety
• 作者: Amos, Vanessa;Phair, Nicholas;Sullivan, Kevin;Wocial, Lucia D.;Epstein, Beth
• 通讯作者: Epstein, Beth

Fuzzing Mobile Robot Environments for Fast Automated Crash Detection

• DOI: 10.1109/icra48506.2021.9561627
• 发表时间: 2021-05
• 期刊: 2021 IEEE International Conference on Robotics and Automation (ICRA)
• 作者: Trey Woodlief;Sebastian G. Elbaum;K. Sullivan

ConEx: Efficient Exploration of Big-Data System Configurations for Better Performance

• DOI: 10.1109/tse.2020.3007560
• 发表时间: 2022-03-01
• 期刊: IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
• 影响因子: 7.4
• 作者: Krishna, Rahul;Tang, Chong;Ray, Baishakhi
• 通讯作者: Ray, Baishakhi