Hide metadata

dc.contributor.authorKlev, Henrik Torland
dc.date.accessioned2020-09-21T23:46:55Z
dc.date.available2020-09-21T23:46:55Z
dc.date.issued2020
dc.identifier.citationKlev, Henrik Torland. Verifying EVA: Formal verification of the software for deciding Norwegian governmental elections. Master thesis, University of Oslo, 2020
dc.identifier.urihttp://hdl.handle.net/10852/79576
dc.description.abstractEVA er hovedstøttesystemet for valggjennomføring for kommunene og fylkeskommunene i Norge. Som sådan er det kritisk for samfunnet at systemet oppfører seg som forventet. Ved å bruke formelle metoder kan det påvises at systemet oppfører seg som forventet, og også at det ikke kan unnlate å oppføre seg som forventet. Dette arbeidet vil presentere EVA og dets sentrale aspekter, spesifisere de kritiske egenskapene ved bruk av spesifikasjonsspråket Java Modeling Language, og bevise disse egenskapene ved å bruke en formell teknikk kjent som automated theorem proving med assistanse fra KeY Systemet. I tillegg vil Java Modelling Language og KeY-systemet bli tilstrekkelig presentert slik at de mest fremtredende funksjonene og teoriene kan implementeres i andre verifiseringsinnsatser, og begrensningene til KeY-systemet vil bli presentert og diskutert. Den sekvensielle, ikke-distribuerte karakteren av implementeringen av EVA gjør systemet til et utmerket mål for å vise deduktiv verifisering i et miljø der bibliotekmetoder og eksterne rammeverk blir mye brukt. I det store og hele kan dette arbeidet fungere som en veiledning for andre som er ute etter å starte sitt eget verifiseringsprosjekt, eller ute etter å fortsette og utvide det presenterte arbeidet.eng
dc.language.isoeng
dc.subjectEVA
dc.subjectJDL
dc.subjectelectoral software
dc.subjectformal methods
dc.subjectElektronisk Valg Administrasjon
dc.subjectJML
dc.subjectJava Dynamic Logic
dc.subjectdeductive verification
dc.subjectJava Modeling Language
dc.subjectKeY
dc.subjectFormal verification
dc.titleVerifying EVA: Formal verification of the software for deciding Norwegian governmental electionseng
dc.typeMaster thesis
dc.date.updated2020-09-22T23:45:48Z
dc.creator.authorKlev, Henrik Torland
dc.identifier.urnURN:NBN:no-82770
dc.type.documentMasteroppgave
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/79576/20/Verifying_EVA.pdf


Files in this item

Appears in the following Collection

Hide metadata