Verifying EVA: Formal verification of the software for deciding Norwegian governmental elections

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.