A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software

Kim Steen Henriksen

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

Resumé

Abstract interpretation er en overordnet referenceramme for statisk programanalyse. I de seneste år har abstract interpretation vundet udbredelse uden for det akademiske miljø, hvor det er blevet anvendt til verifikation af indlejrede og tidskritiske systemer.

Logikprogrammering er et programmeringsparadigme der har et solidt matematisk fundament. Et af dets karakteristika er adskillelsen af logik (betydningen af et program) og kontrol (hvordan programmet udføres), hvilket gør logikprogrammering til et meget anvendeligt sprog hvad angår programanalyse.

I denne afhandling bliver logikprogrammering anvendt til at analysere programmer udviklet til indlejrede systemer. Et givet indlejret system modelleres som en emulator skrevet i en variant af logikprogrammering kaldet constraint logic programming (CLP). Emulatoren specialiseres med hensyn til et givet program, hvilket resulterer i et nyt program i skrevet i sproget CLP der samtidig er isomorft med programmet skrevet til det indlejrede system. Anvendes abstract interpretation baserede analysatorer på det specialiserede program, kan resultater fra denne analyse direkte
overføres til den indlejrede program, da dette program og den specialiserede emulator holdes isomorft.

To abstract interpretation baserede analysatorer for logikprogrammering er udviklet i denne afhandling. Den første er en convex polyhedron analysator for CLP programmer, der implementerer et sæt af em widening-teknikker der giver forbedret præcision af analysen. Den anden analysator er en type-analysator for logikprogrammering,
der automatisk udleder en pre-interpretation fra et sæt af regulære type-definitioner.

Sidst i afhandlingen vises det hvorledes en udvidelse af emulatorens semantik kan benyttes til at opnå, for eksempel, en fuldautomatisk Worst Case Execution Time analyse, ved at anvende det convex polyhedron baserede analyseværktøj på den udvidede og specialiserede emulator.

Alle analyseværktøjer udviklet i forbindelse med denne afhandling er gjort tilgængelige online.

OriginalsprogEngelsk
Udgivelses stedRoskilde
ForlagRoskilde Universitet
Antal sider201
StatusUdgivet - 2007
NavnDatalogiske Skrifter
Nummer117
ISSN0109-9779

Note vedr. afhandling

Ph.D.-afhandling, 2008, Roskilde Universitetscenter

Citer dette

Henriksen, K. S. (2007). A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software. Roskilde: Roskilde Universitet. Datalogiske Skrifter, Nr. 117
Henriksen, Kim Steen. / A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software. Roskilde : Roskilde Universitet, 2007. 201 s. (Datalogiske Skrifter; Nr. 117).
@phdthesis{0c18c9e0a4d611dc9a76000ea68e967b,
title = "A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software",
abstract = "Abstract interpretation er en overordnet referenceramme for statisk programanalyse. I de seneste {\aa}r har abstract interpretation vundet udbredelse uden for det akademiske milj{\o}, hvor det er blevet anvendt til verifikation af indlejrede og tidskritiske systemer.Logikprogrammering er et programmeringsparadigme der har et solidt matematisk fundament. Et af dets karakteristika er adskillelsen af logik (betydningen af et program) og kontrol (hvordan programmet udf{\o}res), hvilket g{\o}r logikprogrammering til et meget anvendeligt sprog hvad ang{\aa}r programanalyse.I denne afhandling bliver logikprogrammering anvendt til at analysere programmer udviklet til indlejrede systemer. Et givet indlejret system modelleres som en emulator skrevet i en variant af logikprogrammering kaldet constraint logic programming (CLP). Emulatoren specialiseres med hensyn til et givet program, hvilket resulterer i et nyt program i skrevet i sproget CLP der samtidig er isomorft med programmet skrevet til det indlejrede system. Anvendes abstract interpretation baserede analysatorer p{\aa} det specialiserede program, kan resultater fra denne analyse direkteoverf{\o}res til den indlejrede program, da dette program og den specialiserede emulator holdes isomorft.To abstract interpretation baserede analysatorer for logikprogrammering er udviklet i denne afhandling. Den f{\o}rste er en convex polyhedron analysator for CLP programmer, der implementerer et s{\ae}t af em widening-teknikker der giver forbedret pr{\ae}cision af analysen. Den anden analysator er en type-analysator for logikprogrammering,der automatisk udleder en pre-interpretation fra et s{\ae}t af regul{\ae}re type-definitioner.Sidst i afhandlingen vises det hvorledes en udvidelse af emulatorens semantik kan benyttes til at opn{\aa}, for eksempel, en fuldautomatisk Worst Case Execution Time analyse, ved at anvende det convex polyhedron baserede analysev{\ae}rkt{\o}j p{\aa} den udvidede og specialiserede emulator.Alle analysev{\ae}rkt{\o}jer udviklet i forbindelse med denne afhandling er gjort tilg{\ae}ngelige online.",
keywords = "abstract interpretation, logic programming, program analysis, program specialisation, program transformation",
author = "Henriksen, {Kim Steen}",
year = "2007",
language = "English",
publisher = "Roskilde Universitet",

}

Henriksen, KS 2007, A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software. Datalogiske Skrifter, nr. 117, Roskilde Universitet, Roskilde.

A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software. / Henriksen, Kim Steen.

Roskilde : Roskilde Universitet, 2007. 201 s. (Datalogiske Skrifter; Nr. 117).

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

TY - BOOK

T1 - A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software

AU - Henriksen, Kim Steen

PY - 2007

Y1 - 2007

N2 - Abstract interpretation er en overordnet referenceramme for statisk programanalyse. I de seneste år har abstract interpretation vundet udbredelse uden for det akademiske miljø, hvor det er blevet anvendt til verifikation af indlejrede og tidskritiske systemer.Logikprogrammering er et programmeringsparadigme der har et solidt matematisk fundament. Et af dets karakteristika er adskillelsen af logik (betydningen af et program) og kontrol (hvordan programmet udføres), hvilket gør logikprogrammering til et meget anvendeligt sprog hvad angår programanalyse.I denne afhandling bliver logikprogrammering anvendt til at analysere programmer udviklet til indlejrede systemer. Et givet indlejret system modelleres som en emulator skrevet i en variant af logikprogrammering kaldet constraint logic programming (CLP). Emulatoren specialiseres med hensyn til et givet program, hvilket resulterer i et nyt program i skrevet i sproget CLP der samtidig er isomorft med programmet skrevet til det indlejrede system. Anvendes abstract interpretation baserede analysatorer på det specialiserede program, kan resultater fra denne analyse direkteoverføres til den indlejrede program, da dette program og den specialiserede emulator holdes isomorft.To abstract interpretation baserede analysatorer for logikprogrammering er udviklet i denne afhandling. Den første er en convex polyhedron analysator for CLP programmer, der implementerer et sæt af em widening-teknikker der giver forbedret præcision af analysen. Den anden analysator er en type-analysator for logikprogrammering,der automatisk udleder en pre-interpretation fra et sæt af regulære type-definitioner.Sidst i afhandlingen vises det hvorledes en udvidelse af emulatorens semantik kan benyttes til at opnå, for eksempel, en fuldautomatisk Worst Case Execution Time analyse, ved at anvende det convex polyhedron baserede analyseværktøj på den udvidede og specialiserede emulator.Alle analyseværktøjer udviklet i forbindelse med denne afhandling er gjort tilgængelige online.

AB - Abstract interpretation er en overordnet referenceramme for statisk programanalyse. I de seneste år har abstract interpretation vundet udbredelse uden for det akademiske miljø, hvor det er blevet anvendt til verifikation af indlejrede og tidskritiske systemer.Logikprogrammering er et programmeringsparadigme der har et solidt matematisk fundament. Et af dets karakteristika er adskillelsen af logik (betydningen af et program) og kontrol (hvordan programmet udføres), hvilket gør logikprogrammering til et meget anvendeligt sprog hvad angår programanalyse.I denne afhandling bliver logikprogrammering anvendt til at analysere programmer udviklet til indlejrede systemer. Et givet indlejret system modelleres som en emulator skrevet i en variant af logikprogrammering kaldet constraint logic programming (CLP). Emulatoren specialiseres med hensyn til et givet program, hvilket resulterer i et nyt program i skrevet i sproget CLP der samtidig er isomorft med programmet skrevet til det indlejrede system. Anvendes abstract interpretation baserede analysatorer på det specialiserede program, kan resultater fra denne analyse direkteoverføres til den indlejrede program, da dette program og den specialiserede emulator holdes isomorft.To abstract interpretation baserede analysatorer for logikprogrammering er udviklet i denne afhandling. Den første er en convex polyhedron analysator for CLP programmer, der implementerer et sæt af em widening-teknikker der giver forbedret præcision af analysen. Den anden analysator er en type-analysator for logikprogrammering,der automatisk udleder en pre-interpretation fra et sæt af regulære type-definitioner.Sidst i afhandlingen vises det hvorledes en udvidelse af emulatorens semantik kan benyttes til at opnå, for eksempel, en fuldautomatisk Worst Case Execution Time analyse, ved at anvende det convex polyhedron baserede analyseværktøj på den udvidede og specialiserede emulator.Alle analyseværktøjer udviklet i forbindelse med denne afhandling er gjort tilgængelige online.

KW - abstract interpretation

KW - logic programming

KW - program analysis

KW - program specialisation

KW - program transformation

M3 - Ph.D. thesis

BT - A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software

PB - Roskilde Universitet

CY - Roskilde

ER -

Henriksen KS. A Logic Programming Based Approach to Applying Abstract Interpretation to Embedded Software. Roskilde: Roskilde Universitet, 2007. 201 s. (Datalogiske Skrifter; Nr. 117).