kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0009-0006-1101-3271
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-3719-7682
Show others and affiliations
2024 (English)In: Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, Springer Nature, 2024Chapter in book (Other academic)
Place, publisher, year, edition, pages
Springer Nature, 2024.
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-343806OAI: oai:DiVA.org:kth-343806DiVA, id: diva2:1840257
Note

QC 20240226

Available from: 2024-02-23 Created: 2024-02-23 Last updated: 2024-02-26Bibliographically approved
In thesis
1. Automated Deductive Verification of Safety-Critical Embedded Software
Open this publication in new window or tab >>Automated Deductive Verification of Safety-Critical Embedded Software
2024 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Embedded systems are everywhere in society, and in many industries, such as the automotive industry, embedded systems are safety-critical. Embedded systems are today also increasingly controlled by software, with advances in, for example, autonomous driving. Because of this, there is naturally a need for methods that can ensure the correctness of such software, and for processes and frameworks to deal with the ever-increasing size and complexity of the software. Contract-based design is a well-established design methodology within embedded system design, where the complexity of an embedded system is managed through the use of contracts, for dividing the responsibilities to the different components of a system. 

This thesis presents a formal contract framework, or theory, following the principles of contract-based design. The theory is developed for procedural software, and is defined at the semantic level, allowing it to be instantiated with different languages for defining the contracts and components, depending on what is appropriate for different uses. The theory is parametric on the semantic domain, allowing different types of behaviours to be reasoned about. The thesis also presents different instantiations of the theory, showing both how low-level properties can be specified using Hoare logic or ACSL, as well as high-level temporal properties using temporal logics such as TLA+. The theory also allows different semantic domains to be combined. Within the theory, low-level components can be verified against their contracts in such a way that more abstract, high-level properties can be ensured, when the components are composed.

A common method for verifying the correctness of low-level software is deductive verification, and Frama-C is a well-known framework in which deductive verification of C code can be performed. This thesis also presents work in the area of contract inference, in the form of a tool in which intermediary contracts to be used in verification can be automatically generated. The method uses the C model checker TriCera as a back-end and infers contracts for use in Frama-C. Finally, the thesis also presents a framework for program instrumentation, which makes certain properties easier to verify. Here, programs with assertions over properties that are typically hard to verify are transformed into new programs with assertions not containing those properties, in such a way that if the new program is correct, then the original program is also correct. The thesis presents concrete instrumentations for so-called extended quantifiers, which are a type of aggregation over arrays, such as finding the sum of all values, or the maximum value, in an array.

Abstract [sv]

Inbyggda system finns överallt i samhället, och i många industrier, exempelvis fordonsindustrin, är inbyggda system säkerhetskritiska. Inbyggda system är idag också alltmer säkerhetskritiska, med framsteg inom till exempel autonoma fordon. På grund av detta finns det ett behov av metoder som kan tillse korrekthet av sådan mjukvara, och av processer och ramverk för att tackla den ökande storleken och komplexiteten hos mjukvaran. Konktraktbaserad design är en väletablerad metodologi inom design av inbyggda system, där komplexiteten i inbyggda system hanteras genom användande av konktrakt för att dela upp ansvar bland de olika komponenterna i systemet.

Denna avhandling presenterar ett formellt kontraktsramverk, eller teori, som följer principerna inom kontraktbaserad design. Teoring är utvecklad för mjukvara med funktioner, och endast definierad semantiskt, vilket tillåter den att instantieras med olika språk för att definiera kontrakt och komponenter, beroende på vad som är lämplig för olika användningsområden. Teorin är parametrisk i den semantiska domänen, vilket möjliggör att olika typer av beteende kan resoneras kring. Avhandlingen presenterar också olika instantieringar av teorin, vilket visar hur både lågnivåegenskaper kan specificeras med Hoarelogik eller ACSL, samt temporala högnivåegenskaper med temporala logiker som exempelvis TLA+. Teoring tillåter också att olika semantiska domäner kombineras. Inom teorin kan lågnivåkomponenter verifieras gentemot deras kontrakt på ett sådant sätt att de mer abstrakta högnivåegenskaperna kan visas vara uppfyllda när komponeterna sätts samman.

En vanlig metod för att verifiera korrekhet hos lågnivåmjukvara är deduktiv verifikation, och Frama-C är ett välkänt verktyg i vilket mjukvara skriven i C kan deduktivt verifieras. Avhandlingen presenterar också arbete inom kontraktgenerering, i form av ett verktyg i vilket funktionskontrakt kan genereras och användas för verifiering. Metoden bygger på TriCera, en modellprovare för C-program, och genererar kontrakt som kan anvädnas i Frama-C. Slutligen presenterar avhandlingen också ett ramverk för programinstrumentation, för att förenkla verifiering av vissa egenskaper. I detta ramverk omvandlas program med specfikationer innehållandes egenskaper som vanligtvis är svåra att verifiera till program med specifikationer utan dessa egenskaper, på ett sätt som säkerställer att om det nya programmet är korrekt, så är också originalprogrammet korrekt. Avhandlingen presenterar konkreta instrumentation för så kallade utökade kvantifikatorer, vilka är en typ av aggregering över fält, till exempel summan av alla värden, eller det maximala värdet, i ett fält.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2024. p. 67
Series
TRITA-EECS-AVL ; 2024:17
Keywords
software sontracts, contract-based design, formal verification, deductive verification, contract inference, program instrumentation, embedded software, embedded systems, Frama-C
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-343807 (URN)978-91-8040-846-2 (ISBN)
Public defence
2024-03-15, https://kth-se.zoom.us/j/61999411575, Kollegiesalen, Brinellvägen 6, Stockholm, 13:00 (Swedish)
Opponent
Supervisors
Note

QC 20240223

Available from: 2024-02-23 Created: 2024-02-23 Last updated: 2024-02-27Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records

Amilon, JesperGurov, DilianLidström, Christian

Search in DiVA

By author/editor
Amilon, JesperGurov, DilianLidström, Christian
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 134 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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