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. / 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.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-191566 |
| Date | January 2016 |
| Creators | Lidström, Christian |
| Publisher | KTH, Skolan för datavetenskap och kommunikation (CSC) |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | Swedish |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0023 seconds