@article{scholars2006,
            year = {2011},
           pages = {412--426},
         journal = {Communications in Computer and Information Science},
             doi = {10.1007/978-3-642-22191-0{$_3$}{$_6$}},
          volume = {180 CC},
            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},
          number = {PART 2},
           title = {Formal verification for interaction protocol in agent-based e-learning system using model checking toolkit - MCMAS},
         address = {Kuantan},
        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},
             url = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-79960356884&doi=10.1007\%2f978-3-642-22191-0\%5f36&partnerID=40&md5=2794dcc460bdf6f1f4d3930570b4c70e},
        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. {\^A}{\copyright} 2011 Springer-Verlag.},
            issn = {18650929},
          author = {Latif, N. A. and Hassan, Mohd. F. and Hasan, Mohd. H.},
            isbn = {9783642221903}
}