Research On Model Checking For Multi-agent-system Based On AUML

Agent System, especially Multi-Agent-System(MAS) has became the focus ofresearch in the field of artificial intelligence nowadays. So how to ensure high reliablesoftware for MAS is very important. Due to the high automation and high accuracy, modelchecking as a formal description method has became a hotspot in the field ofsoftware-testing research. On the basis of a lot of references, this paper’s main research isin the consistency of formal description and model checking for MAS, in order to ensurethe correctness of software in the design period. The main contents and innovations forthis paper is as follows.Firstly, this paper overview the research statues of model checking and point out theexist problems about model checking for MAS based on AUML.Secondly, By the research on MAS modeling method.This paper propose a designmethod for MAS,which called FDMAS(Formal Description For MAS). In this method weextend and redefine some formal semantics of AUML based on DPMAS(Design Processfor MAS), in order to avoid the deficience of Agent-orient support in this exist modelingmethod.Thirdly, Based on the exist problem about this issue.we deeply research on modelchecking methods for MAS.And propose a consistency model checking framework forMAS based on AUML and MCMAS. Due to the difference syntax between AUML formalmodeling language and the input language for MCMAS which named ISPL(InterpretedSystem Programming Language).we focus on researching how to solve the differencesyntax and semantics between them,and we achieved the relate conversion rule betweenAUML formal description and ISPL language. In order to make AUML formal descriptiondocument transform automatically to ISPL program. we design and implement aconversion tool AUML2DIS to solve the incompatibilities problem between the AUMLlanguage and the input language for MCMAS.Finally, we design a case analysis based on Book_store_System,and use the methodof FDMAS to modeling this MAS, then run the relate programs to make a verification for the model to be checked. The experimental results prove the correctness of this model andthe feasibility of the MAS model checking method based on AUML and MCMASproposed in this paper.