Formal verification for interaction protocol in agent-based e-learning system using model checking toolkit - MCMAS

Abstract

This paper presents a formal verification done for interaction protocol in agent-based e-learning system using a model checking toolkit - MCMAS (Model Checking Multi-Agent System). The goal of this interaction protocol is to automate the document downloading and notification in e-learning on behalf of the students. The specification of the interaction protocol for each agents are translated into Interpreted Systems Programming Language (ISPL) file as the programming language for MCMAS and a combination of temporal logic operators like Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) are used to verify the formula for each tested reachable property. The purpose of executing this formal verification is to convince that this interaction protocol is sound and reachable for each state. Overall, this paper describes the idea of agent-based e-learning system, MCMAS toolkit - used as a model checker, CTL and LTL - logics in verification used, ISPL - programming language used under MCMAS platform and the results derived from the running verification. © 2011 Springer-Verlag.