Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Automatic Verification of Embedded Systems Using Horn Clause Solvers
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2019 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

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.

Place, publisher, year, edition, pages
2019. , p. 79
Series
IT ; 19021
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-395932OAI: oai:DiVA.org:uu-395932DiVA, id: diva2:1365694
Educational program
Masters Programme in Embedded Systems
Supervisors
Examiners
Available from: 2019-10-25 Created: 2019-10-25 Last updated: 2019-10-25Bibliographically approved

Open Access in DiVA

fulltext(1661 kB)41 downloads
File information
File name FULLTEXT01.pdfFile size 1661 kBChecksum SHA-512
f11a832793cdfe8bad398bb15e3e57398a3c09a1c9d7336839ce745bbef0f5eab40c39136267658beef8f58df26d0ad8f7637f84aca6093a16769abf9a971934
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 41 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 329 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf