CPS: Medium: Collaborative Research: Credible Autocoding and Verification of Embedded Software (CrAVES)

CPS：媒介：协作研究：嵌入式软件的可信自动编码和验证 (CrAVES)

• 批准号: 1135955
• 负责人: Eric Feron
• 金额: $ 57万
• 依托单位: Georgia Tech Research Corporation
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-09-15 至 2015-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1135955&HistoricalAwards=false
• 关键词: CPS; Medium; Collaborative; Research; Credible

The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems. During the autocoding process, the properties of control system specifications are transformed into proven assertions explicitly written in the resulting source code. Thus CrAVES aims at transforming the extensive safety and reliability analyses conducted by control system engineers, such as those based on Lyapunov theory, into rigorous, embedded analyses of the corresponding software implementations. CrAVES comes as a useful complement to current static software analysis methods, which it leverages to develop independent verification systems.Computers and computer programs used to manage documents and spreadsheets. They now also interact with physical artifacts (airplanes, power plants, automobile brakes and robotic surgeons), to create Cyber-Physical Systems. Software means complexity and bugs - bugs which can cause real tragedy, far beyond the frozen screens we associate with system crashes on our current PCs. Software autocoding is becoming the de facto recommended practice for many safety-critical applications. CrAVES aims to evolve this towards higher standards of quality and reduced design times and costs. Rigorous, mathematical arguments supporting safety-critical functionalities are the cornerstone of CrAVES. Collaborative programs involving high-school teachers will encourage the transmission of this message to STEM education in high-schools through university programs designed for that purpose.

CrAVES 项目旨在为嵌入式系统的可靠自动编码奠定知识基础，通过该技术，满足给定开环和闭环属性的图形控制系统规范会自动转换为保证满足相同属性的源代码。目标是通过专用的校对系统可以轻松、独立地验证这些代码的正确性。在自动编码过程中，控制系统规范的属性被转换为明确写入结果源代码中的经过验证的断言。因此，CrAVES 旨在将控制系统工程师进行的广泛安全性和可靠性分析（例如基于李雅普诺夫理论的分析）转化为相应软件实现的严格嵌入式分析。 CrAVES 是对当前静态软件分析方法的有用补充，它利用该方法来开发独立的验证系统。用于管理文档和电子表格的计算机和计算机程序。他们现在还与物理制品（飞机、发电厂、汽车制动器和机器人外科医生）进行交互，以创建网络物理系统。软件意味着复杂性和错误 - 这些错误可能会导致真正的悲剧，远远超出我们当前 PC 上与系统崩溃相关的冻结屏幕。软件自动编码正在成为许多安全关键型应用事实上的推荐做法。 CrAVES 旨在将其发展为更高的质量标准并减少设计时间和成本。支持安全关键功能的严格数学论证是 CrAVES 的基石。涉及高中教师的合作项目将鼓励通过为此目的设计的大学项目将这一信息传递到高中的 STEM 教育。