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.

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.