Agent-based model checking verification framework

Model checking is an automated formal verification technique that takes formal system design model and formal properties specifications as input to perform verification and produce system correctness result and counterexamples. Although a system has been formally verified to be correct using model checking, end users still want to know how correct the system is. As flawless system is rarely feasible, an approach for verifying the verifier is needed to measure the completeness and accuracy levels of the verification implementation. In this research, we propose a framework for evaluating agent-based model checking results with the Universiti Teknologi Malaysia on-line graduate student application system. We have designed multi-agent runtime verification and validation (MARVV) architecture that incorporates a runtime system profiles to perform the evaluation. Finally, we evaluate the applicability of the proposed model using MCMAS model checking.