Modelling an E-Voting Domain for the Formal Development of a Software Product Line: When the Implicit Should Be Made Explicit

There has been much recent interest in the development of electronic voting (e-voting) systems, but there remain many outstanding research challenges for software and system engineers. Software product line (SPL) techniques offer many advantages for the practical development of reliable and trustworthy e-voting systems, but the composition of system features poses significant problems that can be addressed satisfactorily only through the use of formal methods. When such systems are used in government elections, then they are obliged to follow legal standards and/or recommendations written in natural language. For the formal development of e-voting systems, it is necessary to build a domain model which is consistent with the legal requirements. We have already demonstrated that Event-B models can be used to verify critical requirements for e-voting system components. However, the refinement-based approach needs to be applied to the engineering of a complete e-voting system. We report on our approach, using Event-B contexts to model an e-voting ontology, and its integration with an e-voting features model tree which formally specifies the SPL. During this work, we identified the importance of making the implicit explicit in two different ways-domain experts need to explicitly model implicit knowledge, and Event-B modellers need to explicitly communicate the semantics of the formal model constructs to the domain experts. If either of these tasks is not adequately carried out, then this compromises validation of the requirements model (instance of the SPL).