dc.contributor.author | Klev, Henrik Torland | |
dc.date.accessioned | 2020-09-21T23:46:55Z | |
dc.date.available | 2020-09-21T23:46:55Z | |
dc.date.issued | 2020 | |
dc.identifier.citation | Klev, Henrik Torland. Verifying EVA: Formal verification of the software for deciding Norwegian governmental elections. Master thesis, University of Oslo, 2020 | |
dc.identifier.uri | http://hdl.handle.net/10852/79576 | |
dc.description.abstract | EVA 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.iso | eng | |
dc.subject | EVA | |
dc.subject | JDL | |
dc.subject | electoral software | |
dc.subject | formal methods | |
dc.subject | Elektronisk Valg Administrasjon | |
dc.subject | JML | |
dc.subject | Java Dynamic Logic | |
dc.subject | deductive verification | |
dc.subject | Java Modeling Language | |
dc.subject | KeY | |
dc.subject | Formal verification | |
dc.title | Verifying EVA: Formal verification of the software for deciding Norwegian governmental elections | eng |
dc.type | Master thesis | |
dc.date.updated | 2020-09-22T23:45:48Z | |
dc.creator.author | Klev, Henrik Torland | |
dc.identifier.urn | URN:NBN:no-82770 | |
dc.type.document | Masteroppgave | |
dc.identifier.fulltext | Fulltext https://www.duo.uio.no/bitstream/handle/10852/79576/20/Verifying_EVA.pdf | |