Change search
ReferencesLink to record
Permanent link

Direct link
Verification of Functional Requirements of Embedded Automotive C Code
KTH, School of Computer Science and Communication (CSC).
2016 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Verifiering av funktionella krav på inbyggd C-kod i motorfordon (Swedish)
Abstract [en]

Today's vehicles are increasingly controlled by embedded computer systems. Such systems are of safety-critical nature, where an error in the computation could have dire consequences. A common way to ensure that software works is testing, but as the complexity of these systems grows larger it gets harder to ensure enough coverage in the tests.

Another way to ensure that software fulfills its requirements is formal verification, where properties of the code are proven mathematically to hold under certain conditions. Formal verification gives a higher level of confidence in the correctness of code than testing alone, but it is not as widely used within the industry. This project has examined whether current state-of-the-art tools for formal verification are ready to be used to verify real-life safety-critical code.

To answer this, a case study on a module running in Scania's vehicles was performed. Several of the requirements were successfully verified. The thesis also identifies for what type of code and requirements this is possible, and describes a process for how it can be done.

Abstract [sv]

Idag kontrolleras fordon allt mer av inbyggda datorsystem. Sådana system är säkerhetskritiska, där ett fel kan ha ödesdigra konsekvenser. Ett vanligt sätt att försäkra sig om att mjukvaran fungerar är testning, men när komplexiteten av dessa system växer blir det allt svårare att försäkra sig om att testen har tillräcklig täckning.

Ett annat sätt att försäkra sig om att mjukvaran uppfyller dess krav är formell verifiering, där egenskaper hos koden bevisas matematiskt att hålla under vissa villkor. Formell verifiering ger ett högre förtroende för kods korrekthet än vad enbart testning skulle göra, men används ännu inte i lika stor utsträckning inom industrin. Detta projekt har undersökt huruvida moderna verktyg för formell verifiering är mogna att användas för att verifiera riktig säkerhetskritisk kod.

För att svara på detta har en fallstudie av en modul i Scanias fordon genomförts. Flera av dess krav lyckades verifieras. Rapporten identifierar också för vilka typer av kod och krav detta är möjligt, och beskriver en process för hur det kan utföras.

Place, publisher, year, edition, pages
2016.
Keyword [en]
formal verification, verification, functional requirements, embedded, automotive, c
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-191566OAI: oai:DiVA.org:kth-191566DiVA: diva2:957404
External cooperation
Scania CV AB
Educational program
Master of Science in Engineering - Computer Science and Technology
Supervisors
Examiners
Available from: 2016-09-08 Created: 2016-09-01 Last updated: 2016-09-08Bibliographically approved

Open Access in DiVA

fulltext(640 kB)4 downloads
File information
File name FULLTEXT01.pdfFile size 640 kBChecksum SHA-512
6a59c9cf76c2ff3c67160929803da302eb9a29845f980d588ce845201037497c5676e448d2da7930ac2c51c4bd8a0007f6fd3479b18ac9d767840fef4ea003d4
Type fulltextMimetype application/pdf

By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 4 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

Total: 28 hits
ReferencesLink to record
Permanent link

Direct link