Verifying EVA. Formal Verification of the Software Deciding Norwegian Governmental Elections
EVA is the main support system used by municipalities and counties in Norway to hold and implement elections. As such, it is critical to society that the system behaves as expected. By using formal methods it can be proven that the system behaves as expected, and that it cannot fail to behave as expected. This work will present EVA and its central aspects, specify the critical properties using the speciﬁcation language Java Modeling Language, and prove those properties using a formal technique known as automated theorem proving with the assistance of the KeY System. In addition, the Java Modeling Language and the KeY System will be suffciently presented such that the most prominent features and theories can be implemented into other veriﬁcation efforts, whereas the limitations of the KeY System will be presented and discussed. The sequential, non-distributed nature of the implementation of EVA makes this system a prime target for using deductive veriﬁcation in an environment were library methods and external frameworks are extensively used. En masse, this work may serve as a guide for others who seek to start a veriﬁcation project of their own, or to continue and extend the presented work.
Published June 16, 2020 3:46 PM - Last modified July 1, 2020 9:46 AM