For Multi-agent Design And Analysis Of Formal Methods

With the development of applications in various kinds of agent-based systems, agents are regarded as the next generation software engineering paradigm. Along with this trend, study on formal methods for the purposes of specifying complexity and open systems using agent technology has become one of the hot research issues for the last few years. Agent-Oriented G-Nets proposed by Haiping Xu are a kind of multi-methodology combining the object-oriented conceptions, such as encapsulation and inheritance, and existing Petri-net analysis tools. The approach takes effect in formal design and analysis of systems.This thesis uses agent-oriented G-Nets to describe communication interrelationships among subsystems in the train group operation simulation system, and construct the agent-oriented G-Net model for train/station communication. The interrelationship between train agents and station agents has been denoted clearly in the model. In order to validate the process of communication between trains and stations, this dissertation uses one Petri-nets analysis approach to analyze the simplified Petri-nets form of the model. And the result shows the model is L3-liveness which means communication behaviors among sub-systems of the system will not cause deadlocks and blocks in system.The study on the model in the thesis is one important part of the train group operation simulation system based on the essential characteristics, and provides a good basis for future work on description of agents' interactions.