Change search
ReferencesLink to record
Permanent link

Direct link
Formal Requirement Models for Automotive Embedded Systems
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
Formella kravmodeller för inbäddade fordonssystem (Swedish)
Abstract [en]

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.

Abstract [sv]

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.

Place, publisher, year, edition, pages
2016.
Keyword [en]
automotive, system, formal, verification, static analysis, specification
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-191558OAI: oai:DiVA.org:kth-191558DiVA: diva2:957386
External cooperation
Scania 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(692 kB)16 downloads
File information
File name FULLTEXT01.pdfFile size 692 kBChecksum SHA-512
185b2fa54319d5b85c3822298222295e016bf1b9cbf659c7e765798aa1af1cb9292bd9efef11108251ea2baf64f72e240378c10bb91ce9470658d59e99440ad5
Type fulltextMimetype application/pdf

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 16 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: 168 hits
ReferencesLink to record
Permanent link

Direct link