TY  - JOUR
SN  - 18650929
EP  - 426
AV  - none
TI  - Formal verification for interaction protocol in agent-based e-learning system using model checking toolkit - MCMAS
SP  - 412
N1  - 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
Y1  - 2011///
VL  - 180 CC
UR  - 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
A1  - Latif, N.A.
A1  - Hassan, Mohd.F.
A1  - Hasan, Mohd.H.
JF  - Communications in Computer and Information Science
CY  - Kuantan
KW  - Agent based; Inter-action protocols; ISPL; Logics; MCMAS; Reachability
KW  -  Ada (programming language); Computation theory; Computer programming languages; E-learning; Intelligent agents; Learning systems; Multi agent systems; Software agents; Software engineering; Temporal logic
KW  -  Model checking
ID  - scholars2006
N2  - 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.
IS  - PART 2
ER  -