SHF: Small: M2C: Models to Code

软件是经济基础设施的关键部分，软件错误每年造成数百亿美元的损失。模型通常用于捕获软件组件、用户和物理环境的行为，以及它们之间的交互。然而，在代码中实现系统时，这些模型经常被忽略。M2C(模型到代码)项目是一项试验性研究，旨在通过从高级设计模型生成正确高效的代码来弥合设计级模型和代码级实现之间的差距。M2C项目创建用于定义模型的基础设施，使用它们来设计通过构造正确的系统，并生成在一系列平台上忠实地实现这些模型的代码。这将有助于在全球范围内改进软件开发过程，并大幅节省相关成本。在M2C中，形式化的计算模型被用于对复杂系统进行建模。对这些模型进行组合分析以确保正确性，并从它们生成代码以支持模拟和高效执行。研究人员特别考虑了两种基本范式。第一种是PVS规范和验证系统的函数子语言，可用于定义广泛使用的数学和统计操作，并捕获处理器指令集、编程语言和计算模型的语义。第二种是基于准周期执行的计算组合模型，它是体系结构定义语言Radler的基础。通过专注于从经过验证的模型生成正确和高效的代码，该项目为基于安全的软件系统创建了一个无缝的设计流程，从抽象的数学模型到可用于模拟或执行的具体代码。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Software is a critical part of the economic infrastructure and software errors cost tens of billions of dollars annually. Models are often used to capture the behavior of software components, users, and the physical environment, as well as their interaction. However, these models are often ignored when implementing the system in code. The M2C (Models to Code) project is a pilot study aimed at bridging the gap between design-level models and code-level implementations through the generation of correct and efficient code from high-level design models. The M2C project creates infrastructure for defining models, using them in designing systems that are correct by construction, and generating code that faithfully implements these models on a range of platforms. This will help improve the software development process globally, with substantial savings in associated costs.In M2C, formalized models of computation are used to model complex systems. These models are analyzed compositionally for correctness, and code is generated from them to support simulation and efficient execution. The investigators specifically consider two basic paradigms. The first is a functional sublanguage of the PVS Specification and verification system that can be used to define widely used mathematical and statistical operations, and to capture the semantics of processor instruction sets, programming languages, and models of computation. The second is a compositional model of computation based on quasi-periodic execution that underpins the architecture definition language Radler. By focusing on the generation of correct and efficient code from verified models, this project creates a seamless design flow for safety-critical software-based systems going from abstract mathematical models to concrete code that can be used for simulation or execution.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.