eprintid: 2006
rev_number: 2
eprint_status: archive
userid: 1
dir: disk0/00/00/20/06
datestamp: 2023-11-09 15:50:10
lastmod: 2023-11-09 15:50:10
status_changed: 2023-11-09 15:41:48
type: article
metadata_visibility: show
creators_name: Latif, N.A.
creators_name: Hassan, Mohd.F.
creators_name: Hasan, Mohd.H.
title: Formal verification for interaction protocol in agent-based e-learning system using model checking toolkit - MCMAS
ispublished: pub
keywords: Agent based; Inter-action protocols; ISPL; Logics; MCMAS; Reachability, Ada (programming language); Computation theory; Computer programming languages; E-learning; Intelligent agents; Learning systems; Multi agent systems; Software agents; Software engineering; Temporal logic, Model checking
note: cited By 3; Conference of 2nd International Conference on Software Engineering and Computer Systems, ICSECS 2011 ; Conference Date: 27 June 2011 Through 29 June 2011; Conference Code:85603
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.
date: 2011
official_url: 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
id_number: 10.1007/978-3-642-22191-0₃₆
full_text_status: none
publication: Communications in Computer and Information Science
volume: 180 CC
number: PART 2
place_of_pub: Kuantan
pagerange: 412-426
refereed: TRUE
isbn: 9783642221903
issn: 18650929
citation:   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