Embedded systems are a crucial part of modern vehicles today and are used widely by the automotive industry to control safety-critical functions. To verify that the software will work correctly, formal verification can be used to prove that the code will always behave correctly according to some specification. This report will look into how to formulate the specification in such a way that it is easy to use, consistent and can be used efficiently for code verification. Two different models are looked into in the report, and applied to real automotive embedded code. From this, conclusions are made about the different models. / Inbäddade system är en viktig del av moderna motorfordon idag, och används av stora delar av fordonsindustrin för att kontrollera säkerhetskritiska funktioner. För att verifiera att mjukvaran fungerar korrent, kan man använda formell verifiering för att bevisa att koden alltid fungerar korrekt enligt en specifikation. Den här rapporten kommer att studera hur man bäst formulerar en sådan specifikation så att den är lätt att använda, konsekvent och kan användas effektivt för kodverifiering. Två olika modeller används i rapporten, och appliceras till en riktig kodmodul från fordonsindustrin. Från detta görs sedan slutsatser om de olika modellerna.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-191558 |
| Date | January 2016 |
| Creators | Eriksson, John |
| 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.0018 seconds