Ensuring reliability in electronic examinations through UPPAAL-based trustworthy design

Electronic examination serves as an efficient method for assessing learning outcomes, yet the integration of computers into exam processes introduces potential for unreliability. In this article, we propose a formal model for electronic examinations using timed automata, providing a structured approach to understanding and managing the complexities. The electronic examination process is modeled by defining four UPPAAL templates, <i>i.e</i>., candidate, administrator, invigilator, and examiner. Crucial properties specific to electronic examination are encoded as specifications in UPPAAL. Verification against these properties demonstrates the validity and reliability of this model. The modelable and verifiable electronic examination designed with UPPAAL suggests great potential for deeper exploration in trustworthy digital education.