Automatisk Kommentar av Simulink Genererad C kod Baserad på Simulink Modellen

There has been a wave of transformation in the automotive industry in recent years, with most vehicular functions being controlled electron- ically instead of mechanically. This has led to an exponential increase in the complexity of software functions in vehicles, making it essential for manufactures to guarantee their correctness. Traditional software testing is reaching its limits, consequently pushing the automotive in- dustry to explore other forms of quality assurance. One such technique that has been gaining momentum over the years is a set of verification techniques based on mathematical logic called formal verification tech- niques. Although formal techniques have not yet been adopted on a large scale, these methods offer systematic and possibly more exhaus- tive verification of the software under test, since their fundamentals are based on the principles of mathematics.In order to be able to apply formal verification, the system under test must be transformed into a formal model, and a set of proper- ties over such models, which can then be verified using some of the well-established formal verification techniques, such as model check- ing or deductive verification. This thesis focuses on formal verification of automatically generated C code based on Simulink models using deductive verification techniques. More specifically, the aim is to ex- plore whether the generated code can be automatically annotated using the underlying Simulink model as an executable specification, thereby making it suitable for verification using state-of-the-art tools. Our in- vestigation of Simulink generated C code shows that the same can be annotated using the corresponding Simulink model as an executable specification. Consequently, we propose an algorithm that automates the annotation generation and their injection into C code for a specific class of Simulink models and code generated under specific conditions. Successful verification would mean that the code satisfies all functional properties of the model irrespective of the code generator used.We validate our approach on a prototype implementation of a Brake-by-Wire (BBW) functionality of heavy load vehicles. Most of the functional properties of the generated code were satisfied.Det har skett en våg av omvandling inom fordonsindustrin i de senas- te åren, där de flesta fordonsfunktioner nu styrs elektroniskt istället för mekaniskt. Detta har lett till en exponentiell ökning i komplexite- ten av programvarufunktioner i fordon, vilket gör det väsentligt för tillverkare att kunna garantera deras korrekthet. Traditionell testning av programvara är nära sina gränser och driver därför bilindustrin att utforska andra former av kvalitetssäkring. En teknik som har fått fart genom åren är en uppsättning verifieringstekniker baserade på matematisk logik som kallas formella verifikationstekniker. Även om formella tekniker ännu inte har införts på en stor skala erbjuder dessa metoder systematisk och möjligen mer genomgripande verifiering av programvaran som testas, eftersom dess grund är baserad på mate- matikens principer. För att kunna tillämpa formell verifiering behöver systemet som testas omvandlas till en formell modell och en upp- sättning egenskaper över sådana modeller, som sedan kan verifieras med hjälp av några väletablerade formella verifieringstekniker, såsom modellkontroll eller deduktiv verifiering. Denna avhandling fokuse- rar på formell verifiering av automatiskt genererad C-kod baserad på Simulink-modeller med hjälp av deduktiva verifieringstekniker. Mer specifikt är syftet att undersöka om den genererade koden automa- tiskt kan antecknas med den underliggande Simulink-modellen som en körbar specifikation, vilket då skulle göra den lämplig för verifiering med toppmoderna verktyg. Vår undersökning av Simulink-genererad C-kod visar att samma sak kan kommenteras när den motsvarande Simulink-modellen används som en körbar specifikation. Följaktligen föreslår vi en algoritm som automatiserar anteckningsgenereringen och dess injektion i C-kod för en specifik klass av Simulink-modeller och kod genererad under specifika förhållanden. Lyckad verifiering skulle betyda att koden uppfyller alla funktionella egenskaper av mo- dellen oavsett vilken kodgenerator som används.Vi validerar vår strategi med en prototypimplementering av enBrake-by-Wire (BBW) -funktionalitet för tunga lastbilar. De mesta funk- tionella egenskaperna för den genererade koden var uppfyllda