FORMAL SPECIFICATION AND ANALYSIS OF AN AGENT-BASED MEDICAL IMAGE PROCESSING SYSTEM

A mobile agent system is a special distributed system with moving programs in networks. Mobile agent systems provide a powerful and flexible paradigm for building high performance distributed systems. Due to dynamic configuration property, assuring quality of a mobile agent system is a challenge work. Formal specification and analysis of a mobile agent system provides one of the best approaches to ensure the correctness of a system design. However, it is difficult to find a formal specification tool for modeling a mobile agent system with an easy to understand and concise model. In addition, it is a challenge but also important work to provide an automatic formal analysis approach for verifying whether a system specification correctly meets certain requirements in a mobile agent system. In this paper, a framework for specification and analysis of mobile agent systems is defined. First, Predicate/Transition nets are extended with dynamic channels for modeling mobile agent systems. The formalism has the expressive power to naturally model the software architecture of a mobile agent system, and easily capture the properties especially the mobility, mobile communication and dynamic configuration of a mobile agent system. Then, model checking is instrumented to the framework for automatically verifying the correctness of the specification of a mobile agent system. In order to illustrate the capability of the formalism and the verification strategy, a medical image processing system using mobile agents is modeled using the extended Predicate/Transition nets and system properties are verified using the SPIN model checker.