SHF: Small: M2C: Models to Code

点击翻译按钮获取中文摘要

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.