Generating customized verifiers for automatically generated code
Generating customized verifiers for automatically generated code
复制标题
DOI：
10.1145/1449913.1449926
复制
发表时间：
2008-10
期刊：
影响因子：
--
通讯作者：
E. Denney;B. Fischer
中科院分区：
文献类型：
--
作者：
E. Denney;B. Fischer
使用Hoare式技术进行程序验证需要许多逻辑注释。我们以前已经开发了一种通用的注释推断算法，该算法在确保自动生成代码的安全属性所需的所有注释中编织。它使用模式来捕获发电机和特定于属性的代码成语以及特定于属性的元编程片段来构建注释。该算法是通过指定代码模式并将其与以注释构建的元编程片段集成来自定义的。但是，这很困难，因为它涉及乏味且容易出错的低级术语操纵。在这里，我们描述了一种使用生成技术自定义任务自动化任务的方法。它使用一个小的注释模式编译器，该编译器采用了针对特定代码生成器和安全属性量身定制的高级声明注释模式的集合，并生成了所有自定义分析功能和与通用算法核心接口所需的所有自定义分析功能和胶水代码，从而有效地创建了一个定制注释推理算法。编译器提高了抽象水平，并简化了模式的开发和维护。它还可以照顾制定模式和模式的一些常规方面，特别是处理无关的程序片段以及程序结构中的无关紧要，从而降低了所需的大小，复杂性和数量的大小，复杂性和数量。此处描述的改进使自定义系统或新发电机的系统更加容易，更快，我们通过自定义来证明这一点，以证明太空飞行导航代码的框架安全，该框架是由Mathworks的MathWorks的Simulink Models自动生成的。 - 时间研讨会。
Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the meta-program fragments for annotation construction. However, this is difficult since it involves tedious and error-prone low-level term manipulations. Here, we describe an approach that automates this customization task using generative techniques. It uses a small annotation schema compiler that takes a collection of high-level declarative annotation schemas tailored towards a specific code generator and safety property, and generates all customized analysis functions and glue code required for interfacing with the generic algorithm core, thus effectively creating a customized annotation inference algorithm. The compiler raises the level of abstraction and simplifies schema development and maintenance. It also takes care of some more routine aspects of formulating patterns and schemas, in particular handling of irrelevant program fragments and irrelevant variance in the program structure, which reduces the size, complexity, and number of different patterns and annotation schemas required. The improvements described here make it easier and faster to customize the system to a new safety property or a new generator, and we demonstrate this by customizing it to certify frame safety of space flight navigation code that was automatically generated from Simulink models by MathWorks' Real-Time Workshop.