Formal Validation of an Agent-based Location Guidance System (LGS)

Abstract

A multi-agent system has a number of design abstractions as compared to traditional distributed systems. As these systems are distributed, complex and often have a dynamic environment, the formal specification of these systems plays a fundamental role in system correctness. A user location guidance system, based on software agents is designed and verified using formal methods and techniques. In this system, multiple interacting agents work actively in a collaborative way to solve a complex problem. The agent-based location guidance system informs the user about its current location and guides him to find the desired location. We have analyzed the development process after classifying it in the major phases of architecture specification and formal verification. The emphasis is on mathematical based model checking to specify as well as verify agent’s behavior.