Abstract
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.
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.
| Originalsprog | Engelsk |
|---|
| Udgivelsessted | Roskilde |
|---|---|
| Forlag | Roskilde Universitet |
| Antal sider | 201 |
| Status | Udgivet - 2007 |
| Navn | Datalogiske Skrifter |
|---|---|
| Nummer | 117 |
| ISSN | 0109-9779 |