relation: https://khub.utp.edu.my/scholars/2006/
title: Formal verification for interaction protocol in agent-based e-learning system using model checking toolkit - MCMAS
creator: Latif, N.A.
creator: Hassan, Mohd.F.
creator: Hasan, Mohd.H.
description: 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.
date: 2011
type: Article
type: PeerReviewed
identifier:   Latif, N.A. and Hassan, Mohd.F. and Hasan, Mohd.H.  (2011) Formal verification for interaction protocol in agent-based e-learning system using model checking toolkit - MCMAS.  Communications in Computer and Information Science, 180 CC (PART 2).  pp. 412-426.  ISSN 18650929     
relation: https://www.scopus.com/inward/record.uri?eid=2-s2.0-79960356884&doi=10.1007%2f978-3-642-22191-0_36&partnerID=40&md5=2794dcc460bdf6f1f4d3930570b4c70e
relation: 10.1007/978-3-642-22191-0₃₆
identifier: 10.1007/978-3-642-22191-0₃₆