Correct translation of abstract specifications to C-Code

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

Correct translation of abstract specifications to C-Code (VeriCode)The refinement based approach is a successful technique for the development of verified software. It usually ends with imperativeprograms (organized in components) together with axiomatic descriptions of data structures and functions in predicate logic. Many projects have used this methodology successfully. One very extensive project is our Flashix project, in which we developed and verified a file system for Flash memory.Specifications and programs use the referentially transparent copy semantics of predicate logic, the weakest precondition calculus forsequential programs, and a rely-guarantee calculus for concurrent programs. To get executable code from such programs, theorem provers typically generate functional programs with immutable data structures.The resulting code is usually inefficient since destructive updates, that are necessary for the efficient use of e.g. arrays, are notcorrect in general. In addition, the necessary garbage collection is not possible for applications in operating system kernels, or inreal-time applications. These require code that manages memory explicitly, e.g. C-Code.Moving from abstract, referentially transparent data structures to efficient, destructive code is difficult, since explicit informationwhere memory should be allocated or which updates can overwrite is not present.In previous work we have developed an approach, that translates in a way that keeps all data structures disjoint (unshared) betweencomponents, and modifies unshared data structures destructively. Although this leads to a considerable improvement it is stillinefficient compared to manually written code (ca. a factor of 10, depending on the application), since an assignment x := ystill has to copy the data structure stored in y including all substructures (if y is still used). These copy operations can often be avoided using a careful analysis.The goal of this project is to develop a systematic data flow analysis that allows the generation of optimal C-Code with a minimum of copy operations, such that the resulting code is comparably efficient to manually written code (factor 1-3). For this, we want to define a specification framework with algebraic specifications for abstract data types, as well as concurrent imperative programs. We want to formally specify the core of the data flow analysis and verify that the transformation from the specification language yields correct code without memory leaks.To document the success of the project, its results will be evaluated with several case studies.The abstract specification framework allows the project result to be used by all other verification systems, and can significantly improve the practical usage of verified programs.