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
Constraint-Based Contract Inference for Deductive Verification
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-8682-6804
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
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. p. 149-176
Series
Lecture Notes in Computer Science, ISSN 03029743 ; 12345
Keywords [en]
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: urn:nbn:se:kth:diva-290389DOI: 10.1007/978-3-030-64354-6_6Scopus ID: 2-s2.0-85097583578OAI: oai:DiVA.org:kth-290389DiVA, id: diva2:1532270
Note

QC 20210301

Available from: 2021-03-01 Created: 2021-03-01 Last updated: 2024-02-23Bibliographically 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

Other links

Publisher's full textScopus

Authority records

Alshnakat, AnoudGurov, DilianLidström, Christian

Search in DiVA

By author/editor
Alshnakat, AnoudGurov, DilianLidström, Christian
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 278 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