Improving the Synthesis of Annotations for Partially Automated Deductive Verification

This work investigates possible improvements to an existing annotation inference tool. The tool is part of a toolchain that aims to automate the process of software verification using formal methods. The purpose of the annotations is to facilitate the use of deductive verification, which is the formal method used in this project for proving that a given program meets its specifications. In the project, two categories of annotations are established. The first category is the category of functional annotations. These annotations describe the behavior of a function or a module. The other category is what we call auxiliary annotations. These annotations describe properties that are necessary for proving the correctness of the functional annotations. The tool that this work tries to improve is dedicated to inferring the auxiliary annotations. To our knowledge, this is the first tool of its kind to automatically infer auxiliary annotations for a complete module given the module’s source code and its interface specifications. The work contributed in four areas: inferring annotations from the interface specifications of a module and propagating these annotations to all the helper functions used in the module; inferring annotations for floating-point constructs; inferring annotations for pointer constructs; and finally, inferring annotations for array constructs. The improved tool was tested on production embedded code used in the heavy automotive industry. The results demonstrated a considerable improvement and were in line with earlier findings. The work confirms the feasibility and usability of auxiliary annotation inference in this scope.
Detta arbete undersöker möjliga förbättringar av ett befintligt verktyg för härledning av annoteringar (annotations). Verktyget är en komponent i en verktygskedja som syftar till att automatisera processen för mjukvaruverifiering med formella metoder. Syftet med annoteringarna är att underlätta användningen av deduktiv verifiering, vilket är den formella metod som används i detta projekt för att bevisa att ett givet program uppfyller dess specifikationer. I projektet fastställs två kategorier av annoteringar. Den första kategorin är kategorin funktionella annoteringar. Dessa annoteringar beskriver beteendet hos en funktion eller en modul. Den andra kategorin är vad vi kallar hjälp annoteringar (auxiliary annotations). Dessa annoteringar beskriver egenskaper som är nödvändiga för att bevisa korrektheten av de funktionella annoteringarna. Verktyget som detta arbete försöker förbättra är dedikerat till att härleda hjälp annoteringar. Arbetet bidrog inom fyra områden: att härleda annoteringar från gränssnittsspecifikationerna (interface specifications) för en modul och sprida dessa annoteringar till alla hjälpfunktioner som används i modulen; härleda annoteringar för flyttalskonstruktioner (floating-point constructs); härleda annoteringar för pekarkonstruktioner; och slutligen, härleda annoteringar för arraykonstruktioner. Det förbättrade verktyget testades på produktionsinbyggdad kod som används inom fordonsindustrin. Resultaten visade en avsevärd förbättring och var i linje med tidigare resultat. Arbetet bekräftar genomförbarheten och användbarheten av hjälpannoteringshärledning i projektets omfattning.