<div class="csl-bib-body">
<div class="csl-entry">Durand, T. (2020). <i>Verifying automotive software components using C model checkers</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77681</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2020.77681
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/15571
-
dc.description
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
-
dc.description.abstract
Softwaresysteme, die für die Automobilindustrie entwickelt werden, erleben derzeit einen enormen Anstieg der Komplexität, der mit einer Erhöhung der Sicherheitsanforderungen einhergeht. Die Sicherstellung ihrer Korrektheit ist eine herausfordernde und kostspielige Aufgabe, welcher die Forschung nach neuen technologischen Lösungen motiviert. Software-Verifikationswerkzeuge, die auf C-Code abzielen, sind zwar in der Industrie noch nicht weit verbreitet, zeigen aber jedes Jahr beeindruckende Leistungsverbesserungen, was sie zu guten Kandidaten für die Gewährleistung der Sicherheit eingebetteter Systeme macht. Das Ziel dieser Studie ist es, die Fähigkeit modernster Verifikationswerkzeuge zu bewerten, welche die Abwesenheit von Laufzeitfehlern bei vier Softwarekomponenten unterschiedlicher Komplexität nachzuweisen. Diese Komponenten aus der realen Welt werden von TTTech entwickelt, einer Firma, die auf sicherheitsbezogene Lösungen für die Automobilindustrie spezialisiert ist. Zunächst erstellen wir ein generisches Umgebungsmodell, das auf dem AUTOSAR-Standard basiert, der in der Automobilindustrie weit verbreitet ist. Dieses Modell zielt darauf ab, eine Komponente von der übrigen Software-Plattform für die Verifikation zu isolieren, und verwendet bereits existierende, durch den Standard definierte Spezifikationen. Anschließend prüfen wir den Code mit Ultimate Automizer, CPAChecker und CBMC, ergänzt durch Ideen wie z.B. k-Induktion oder Analyse des variablen Bereichs.Unsere Ergebnisse zeigen, dass Verifikationswerkzeuge in der Lage sind, die Fehlerfreiheit von drei von vier Komponenten erfolgreich nachzuweisen, jedoch für die komplexeste Komponente keine definitive Antwort geben können. Die leistungsfähigste Verifikationsmethode ergibt sich aus der Kombination der Ergebnisse verschiedener Code-Analysen, wobei CBMC das endgültige Urteil mittels k-Induktion feststellt. Für den problematischen Fall geben wir Einblicke in die Ursachen der Schwierigkeiten und die nächsten Schritte, die zu deren Überwindung erforderlich sind. Wir kommen zu dem Schluss, dass die Einführung von Verifikationswerkzeugen in den Entwicklungsprozess positive Veränderungen der allgemeinen Codequalität mit sich bringen kann.
de
dc.description.abstract
Software systems developed for the automobile industry are currently witnessing a tremendous increase in complexity, happening in concert with an escalation of safety requirements. Ensuring their correctness is a challenging and costly task, which motivates the research for new technological solutions. While not yet broadly adopted in industry, software verification tools targeting C code demonstrate impressive performance improvements every year, which makes them good candidates for ensuring the safety of embedded systems. This study aims at evaluating the capacity of state-of-the-art verification tools for proving the absence of run-time errors on four software components of various complexity. These real-world components are developed by TTTech, a firm specialized in safety-related automotive solutions. Firstly, we establish a generic environment model based on the AUTOSAR standard, which is broadly adopted in the automobile industry. This model aims at isolating a component from the rest of the software platform for verification, and uses already-existing specifications defined by the standard. We then check the code using Ultimate Automizer, CPAChecker and CBMC extended with several ideas, such as k-induction or variable range analysis. Our results show that verification tools are able to successfully prove the absence of errors in three out of four components, and cannot give a definite answer for the most complex one. The most capable verification method is obtained by combining the results of different code analyzes, with CBMC establishing the final verdict using k-induction. For the problematic case, we give insights into the causes of difficulties, and next steps required to overcome them. We conclude that introducing verification tools in the development process can bring positive changes to the general code quality.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Software-Verifizierung
de
dc.subject
Modellprüfung
de
dc.subject
Automobilindustrie
de
dc.subject
AUTOSAR
de
dc.subject
Software Verification
en
dc.subject
Model Checking
en
dc.subject
Automotive Industry
en
dc.subject
AUTOSAR
en
dc.title
Verifying automotive software components using C model checkers
en
dc.title.alternative
Model Checking von Softwarekomponenten in der Automobilindustrie
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2020.77681
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Timothée Durand
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Steiner, Wilfried
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC15750320
-
dc.description.numberOfPages
69
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
item.openaccessfulltext
Open Access
-
item.grantfulltext
open
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.languageiso639-1
en
-
item.openairetype
master thesis
-
item.fulltext
with Fulltext
-
crisitem.author.dept
E308 - Institut für Werkstoffwissenschaft und Werkstofftechnologie
-
crisitem.author.parentorg
E300 - Fakultät für Maschinenwesen und Betriebswissenschaften