Automatic Verification of Embedded Systems Using Horn Clause Solvers

Sammanfattning: Recently, an increase in the use of safety-critical embedded systems in the automotive industry has led to a drastic up-tick in vehicle software and code complexity. Failure in safety-critical applications can cost lives and money. With the ongoing development of complex vehicle software, it is important to assess and prove the correctness of safety properties using verification and validation methods. Software verification is used to guarantee software safety, and a popular approach within this field is called deductive static methods. This methodology has expressive annotations, and tends to be feasible even on larger software projects, but developing the necessary code annotations is complicated and costly. Software-based model checking techniques require less work but are generally more restricted with respect to expressiveness and software size. This thesis is divided into two parts. The first part, related to a previous study where the authors verified an electronic control unit using deductive verification techniques. We continued from this study by investigating the possibility of using two novel tools developed in the context of software-based model checking: SeaHorn and Eldarica. The second part investigated the concept of automatically inferring code annotations from model checkers to use them in deductive verification tools. The chosen contract format was ACSL, derived from Eldarica and used later in Frama-C. The results of the first part showed that the success of verification was tool-dependent. SeaHorn could verify most of the safety functional requirements and reached a higher level of abstraction than Eldarica. The comparison between this thesis and the related work showed that model checkers are faster, scaled to the code size, required less manual work, and less code overhead compared to deductive verification tools. The second part of the thesis was implemented as an extension of TriCera, using Scala. The ACSL annotations were tested with Frama-C using verification tasks from SV-COMP benchmark, and the results showed that it was possible to generate adequate contracts for simple functions.