Resumé
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 |
|---|
| Udgivelses sted | Roskilde |
|---|---|
| Forlag | Roskilde Universitet |
| Antal sider | 201 |
| Status | Udgivet - 2007 |
| Navn | Datalogiske Skrifter |
|---|---|
| Nummer | 117 |
| ISSN | 0109-9779 |
Note vedr. afhandling
Ph.D.-afhandling, 2008, Roskilde UniversitetscenterCiter dette
}
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/rapport › Ph.d.-afhandling › Forskning
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 -