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

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

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.