Ensuring reliability in electronic examinations through UPPAAL-based trustworthy design

Area of Science:

• Computer Science
• Educational Technology
• Formal Methods

Background:

• Electronic examinations offer efficiency in assessing learning outcomes.
• Integrating computers into exams can introduce unreliability and security concerns.
• Formal verification methods are needed to ensure the integrity of digital assessments.

Purpose of the Study:

• To propose a formal model for electronic examinations using timed automata.
• To address the complexities and potential unreliability in computer-based testing.
• To enhance the trustworthiness of digital education through verifiable assessment models.

Main Methods:

• Developed a formal model for electronic examinations utilizing UPPAAL timed automata.
• Defined four UPPAAL templates representing key roles: candidate, administrator, invigilator, and examiner.
• Encoded critical electronic examination properties as specifications within UPPAAL for verification.

Main Results:

• The proposed UPPAAL model successfully represents the electronic examination process.
• Verification against encoded properties demonstrated the model's validity and reliability.
• The model provides a structured approach to managing complexities in electronic assessments.

Conclusions:

• The modelable and verifiable electronic examination system using UPPAAL shows significant promise.
• This approach can contribute to building more trustworthy digital education environments.
• Further exploration of formal methods in digital assessment is warranted.