Automated Annotation of Simulink Generated C Code Based on the Simulink Model
Abstract: 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.
AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)