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
Automated Deductive Verification of Safety-Critical Embedded Software
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-3719-7682
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 [en]
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: urn:nbn:se:kth:diva-343807ISBN: 978-91-8040-846-2 (print)OAI: oai:DiVA.org:kth-343807DiVA, id: diva2:1840268
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
List of papers
1. An Abstract Contract Theory for Programs with Procedures
Open this publication in new window or tab >>An Abstract Contract Theory for Programs with Procedures
2021 (English)In: Fundamental Approaches to Software Engineering (FASE 2021) / [ed] Guerra, E Stoelinga, M, Springer Nature , 2021, Vol. 12649, p. 152-171Conference paper, Published paper (Refereed)
Abstract [en]

When developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated contract theories formalise the notion of contract and the operations on contracts in a manner that supports best the development of systems in that area. At the other end, contract meta-theories attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract metatheory of Benveniste et al. [5], which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer's design-by-contract methodology [18]. At the core of this gap appears to be the notion of procedure: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components. In this paper, we provide a first step towards a contract theory that takes procedures as the basic building block, and is at the same time an instantiation of the meta-theory. To this end, we propose an abstract contract theory for sequential programming languages with procedures, based on denotational semantics. We show that, on the one hand, the specification of contracts of procedures in Hoare logic, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, we also show our contract theory to fulfil the axioms of the meta-theory. In this way, we give further evidence for the utility of the meta-theory, and prepare the ground for combining our instantiation with other, already existing instantiations.

Place, publisher, year, edition, pages
Springer Nature, 2021
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 12649
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-306349 (URN)10.1007/978-3-030-71500-7_8 (DOI)000720079700008 ()
Conference
24th International Conference on Fundamental Approaches to Software Engineering (FASE) held as part of the 24th Annual Joint European Conferences on Theory and Practice of Software (ETAPS), Mars 27-April 01, 2021, ELECTR NETWORK
Note

QC 20211215

Part of proceeding: ISBN 978-3-030-71500-7; 978-3-030-71499-4

Available from: 2021-12-15 Created: 2021-12-15 Last updated: 2024-03-18Bibliographically approved
2. Contract Based Embedded Software Design
Open this publication in new window or tab >>Contract Based Embedded Software Design
2023 (English)In: Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Proceedings, Springer Nature , 2023, p. 77-94Conference paper, Published paper (Refereed)
Abstract [en]

In embedded systems development, contract based design is a design paradigm where a system is divided hierarchically into components and developed in a top-down manner, using contracts as a means to divide responsibilities and manage the complexity of the system. Contract theories provide a formal basis for reasoning about the properties of the system, and of the contracts themselves. In previous work, we have developed a contract theory for sequential, procedural programs, that is defined abstractly, at the semantic level. The theory fulfils well-established, desired properties of system design. In this paper, we present a methodology for applying the contract theory in real embedded software design. We show how to instantiate the contract theory with concrete syntaxes for defining components and contracts, and how the contract theory enables formal reasoning about the resulting objects. In order to cope with the need for different behavioural models at different levels of abstraction in an embedded system, we extend the contract theory through parametrisation on the semantic domain. We illustrate the application of the proposed methodology on a small, but realistic example, where the temporal logic TLA is used for reasoning at the system level, while lower level components are specified using pre- and post-conditions in the form of ACSL, a specification language for C.

Place, publisher, year, edition, pages
Springer Nature, 2023
National Category
Computer Sciences Embedded Systems
Identifiers
urn:nbn:se:kth:diva-334440 (URN)10.1007/978-3-031-35257-7_5 (DOI)2-s2.0-85164908794 (Scopus ID)
Conference
17th International Symposium on Theoretical Aspects of Software Engineering, TASE 2023, Bristol, United Kingdom of Great Britain and Northern Ireland, Jul 4 2023 - Jul 6 2023
Note

Part of ISBN 9783031352560

QC 20230821

Available from: 2023-08-21 Created: 2023-08-21 Last updated: 2024-02-23Bibliographically approved
3. Deductive Verification Based Abstraction for Software Model Checking
Open this publication in new window or tab >>Deductive Verification Based Abstraction for Software Model Checking
2022 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature , 2022, Vol. 13701 LNCS, p. 7-28Conference paper, Published paper (Refereed)
Abstract [en]

The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.

Place, publisher, year, edition, pages
Springer Nature, 2022
Keywords
Contracts, Deductive verification, Model checking
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-329628 (URN)10.1007/978-3-031-19849-6_2 (DOI)2-s2.0-85142704037 (Scopus ID)
Conference
11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22-30 October 2022
Note

QC 20230622

Available from: 2023-06-22 Created: 2023-06-22 Last updated: 2024-03-15Bibliographically approved
4. Constraint-Based Contract Inference for Deductive Verification
Open this publication in new window or tab >>Constraint-Based Contract Inference for Deductive Verification
2020 (English)In: Deductive Software Verification: Future Perspectives, Springer Nature , 2020, p. 149-176Chapter in book (Refereed)
Abstract [en]

Assertion-based software model checking refers to techniques that take a program annotated with logical assertions and statically verify that the assertions hold whenever program execution is at the corresponding control point. While the associated annotation overhead is relatively low, these techniques are typically monolithic in that they explore the state space of the whole program at once, and may therefore scale poorly to large programs. Deductive software verification, on the other hand, refers to techniques that prove the correctness of a piece of software against a detailed specification of what it is supposed to accomplish or compute. The associated verification techniques are modular and scale well to large code bases, but incur an annotation overhead that is often very high, which is a real obstacle for deductive verification to be adopted in industry on a wider scale. In this paper we explore synergies between the two mentioned paradigms, and in particular, investigate how interpolation-based Horn solvers used for software model checking can be instrumented to infer missing procedure contracts for use in deductive verification, thus aiding the programmer in the code annotation process. We summarise the main developments in the area of automated contract inference, and present our own experiments with contract inference for C programs, based on solving Horn clauses. To drive the inference process, we put program assertions in the main function, and adapt our TriCera tool, a model checker based on the Horn solver Eldarica, to infer candidate contracts for all other functions. The contracts are output in the ANSI C Specification Language (ACSL) format, and are then validated with the Frama-C deductive verification tool for C programs.

Place, publisher, year, edition, pages
Springer Nature, 2020
Series
Lecture Notes in Computer Science, ISSN 03029743 ; 12345
Keywords
Logic programming, Specification languages, Specifications, Constraint-based, Corresponding control points, Deductive verification, Inference process, Program execution, Software model checking, Software verification, Verification techniques, Model checking
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-290389 (URN)10.1007/978-3-030-64354-6_6 (DOI)2-s2.0-85097583578 (Scopus ID)
Note

QC 20210301

Available from: 2021-03-01 Created: 2021-03-01 Last updated: 2024-02-23Bibliographically approved
5. An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
Open this publication in new window or tab >>An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
Show others...
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:nbn:se:kth:diva-343806 (URN)
Note

QC 20240226

Available from: 2024-02-23 Created: 2024-02-23 Last updated: 2024-02-26Bibliographically approved
6. Automatic Program Instrumentation for Automatic Verification
Open this publication in new window or tab >>Automatic Program Instrumentation for Automatic Verification
Show others...
2023 (English)In: Computer Aided Verification: 35th International Conference, CAV 2023, Proceedings, Springer Nature , 2023, p. 281-304Conference paper, Published paper (Refereed)
Abstract [en]

In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

Place, publisher, year, edition, pages
Springer Nature, 2023
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-336732 (URN)10.1007/978-3-031-37709-9_14 (DOI)2-s2.0-85169431034 (Scopus ID)
Conference
35th International Conference on Computer Aided Verification, CAV 2023, Paris, France, Jul 17 2023 - Jul 22 2023
Note

Part of ISBN 9783031377082

QC 20231123

Available from: 2023-09-19 Created: 2023-09-19 Last updated: 2024-02-23Bibliographically approved

Open Access in DiVA

fulltext(1633 kB)98 downloads
File information
File name FULLTEXT01.pdfFile size 1633 kBChecksum SHA-512
11c426d05b20468d6392a37fcc0c3abf5ccfc753683dbf342e9d04e23665a59ebe2aeac9a8a03e8081a643fc303f4d597eda204f4c19b325fef57bb25f09b5de
Type fulltextMimetype application/pdf

Authority records

Lidström, Christian

Search in DiVA

By author/editor
Lidström, Christian
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 98 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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1072 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