Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Combining Inlining and Contracting for Human Efficient Deductive Verification
KTH, Skolan för elektroteknik och datavetenskap (EECS).
2019 (Engelska)Självständigt arbete på avancerad nivå (masterexamen), 20 poäng / 30 hpStudentuppsats (Examensarbete)
Abstract [en]

A function is functionally correct when it behaves according to a specification that describes its input-output behaviour. With deductive verification, it is possible to prove whether a function conforms to its specification or not. The specification is provided in the form of a source code annotation and describes the function’s input-output behaviour using first-order logic. The function and specification are then used to generate logic formulas that, if proven valid, ensure that the function follows the specification.Creating these source annotations, also called contracts, can be difficult, time-consuming and hence, costly. Therefore, reducing the cost by decreasing the human workload would be a significant step toward large scale deductive verification. One way to do so is to use inlining, which eliminates function definitions by replacing all call sites with the function body instead.This thesis explores if and how inlining can be combined with contracting to reduce the human workload by reducing the number of contracts to be written. For this to be possible, a method to estimate the machine effort required to prove an inlined version is needed. In other words, we need to be able to estimate the verification time for a code module. To this end, two Scania code modules and five categories of artificial programs have been measured.By using function metrics and the verification times of the artificial programs, a heuristic was created using regression. This heuristic was then tested on the Scania modules. The results suggest that the artificial modules were not complex enough to accurately predict the Scania modules. However, it was possible to fit the heuristic to the Scania modules so that no estimate of a Scania module was severely off target. In other words, the Scania modules and their inlined versions were similar enough to be roughly estimated with the same function.If this similarity extends to other industry modules, then creating a general heuristic for estimating verification time would be possible

Abstract [sv]

En funktion är funktionellt korrekt när dess beteende överenstämmer med en specifikation. Med deduktiv verifikation är det möjligt att bevisa om en funktion följer sin specifikation. Specifikationen ges i form av en källkodsannotering och beskriver förhållandet mellan indata och utdata med hjälp av första ordningens logik. Implementationen och specifikationen används sedan för att generera logiska formler som, om bevisade valida, försäkrar att implementationen följer specifikationen.Skapandet av dessa källkodsannoteringar, som även kallas kontrakt, kan vara svårt, tidskrävande och kostsamt. Att reducera kostnaden genom att minska den mänskliga arbetsbördan vore ett stort steg mot storskalig deduktiv verifikation. Ett sätt att uppnå detta är genom inlining, med inlining kan man byta ut alla anrop till en funktion mot dess funktionskropp istället.Den här uppsatsen utforskar om och hur inlining kan kombineras med kontrakt för att minska den mänskliga arbetsinsatsen genom att reducera antalet kontrakt som måste skrivas. För att detta ska vara möjligt krävs en metod för att approximera maskinarbetsbördan som krävs för att genomföra ett bevis av en version med inlining. Med andra ord behöver vi kunna estimera verifikationstiden för en kodmodul. Mot detta ändamål, så har två Scania-moduler och fem kategorier av artificiella program mätts upp.Med funktionsmetriker och verifikationstider för de artificiella programmen, så skapades en heuristik med hjälp av regression. heuristiken testades sedan på Scania-modulerna. Resultaten antyder att de artificiella programmen inte är komplexa nog för att tillräckligt estimera Scania-modulerna. Däremot var det möjligt att anpassa heuristiken till Scania-modulerna så att ingen version hade ett överdrivet estimeringsfel.Med andra ord så är Scania-modulerna och deras olika versioner lika nog för att grovt estimeras av samma funktion. Om denna likhet sträcker sig till andra industrimoduler, borde det vara möjligt att konstruera en mer generell heuristik som kan estimera verifikationstiden.

Ort, förlag, år, upplaga, sidor
2019. , s. 62
Serie
TRITA-EECS-EX ; 2019:218
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:kth:diva-254971OAI: oai:DiVA.org:kth-254971DiVA, id: diva2:1337066
Utbildningsprogram
Teknologie masterexamen - Datalogi
Handledare
Examinatorer
Tillgänglig från: 2019-07-11 Skapad: 2019-07-11 Senast uppdaterad: 2019-07-11Bibliografiskt granskad

Open Access i DiVA

fulltext(2964 kB)13 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 2964 kBChecksumma SHA-512
6337ba99bb1f505cc7ba8ff988404d82b78b477d5fe63bc2956f5e6adeb10cc224c49ff84761bc04d9edf5e3157a9a571c686ab428ec01f85e007f5450aaed59
Typ fulltextMimetyp application/pdf

Av organisationen
Skolan för elektroteknik och datavetenskap (EECS)
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 13 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 104 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf