Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
Scania.
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics. Systems Development DivisionScania AB, Södertälje, Sweden.
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics. (Inbyggda kontrollsystem)ORCID iD: 0000-0002-9655-7326
2017 (English)In: Critical Systems: Formal Methods and Automated Verification, Cham: Springer, 2017, p. 3-18Conference paper, Published paper (Refereed)
Abstract [en]

This paper summarizes our experiences from an exercise in deductive verification of functional properties of automotive embedded Ccode in an industrial setting. We propose a formal requirements model that supports the way C-code requirements are currently written at Scania. We describe our work, for a safety-critical module of an embedded system, on formalizing its functional requirements and verifying its C-code implementation by means of VCC, an established tool for deductive verification. We describe the obstacles we encountered, and discuss the automation of the specification and annotation effort as a prerequisite for integrating this technology into the embedded software design process.

Place, publisher, year, edition, pages
Cham: Springer, 2017. p. 3-18
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10471
National Category
Mathematical Analysis Algebra and Logic
Identifiers
URN: urn:nbn:se:kth:diva-214853DOI: 10.1007/978-3-319-67113-0_1ISBN: 978-3-319-67113-0 (electronic)ISBN: 978-3-319-67112-3 (print)OAI: oai:DiVA.org:kth-214853DiVA, id: diva2:1143941
Conference
FMICS '17, AVoCS '17
Funder
VINNOVA
Note

QC 20170925

Available from: 2017-09-23 Created: 2017-09-23 Last updated: 2017-09-25Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Gurov, DilianNyberg, MattiasWestman, Jonas
By organisation
Theoretical Computer Science, TCSMechatronics
Mathematical AnalysisAlgebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 39 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf