In this chapter a formal agent based approach for the modeling and verification of intelligent information systems using Coloured Petri Nets is presented. The use of a formal method allows analysis techniques such as automatic simulation and verification, increasing the confidence on the system behavior. The agent based modelling allows separating distribution, integration and intelligent features of the system, improving model reuse, flexibility and maintenance. As a case study an intelligent information control system for parking meters price is presented.
TopIntroduction
Intelligent information systems (IIS) have been used in several different domains such as communication, sensor networks, decision-making processes, traffic control, business, and manufacturing systems, among others. Most IIS are distributed because the data is collected, processed, and used at different locations by different entities. These entities are autonomous and communicate among them to perform specific tasks. This scenario of an integrated IIS (IIIS) gives rise to several problems and difficulties to be addressed by the development team. Communication, scheduling, synchronization, databases, workflow, and real-time systems are some of the fields that usually have to be addressed in the development of an IIIS.
The agent-based development has been successfully applied to develop information systems with the characteristics mentioned (Jennings, 2001). Agents are intelligent entities, which are distributed and integrated to other agents. Therefore, developing information systems using the agent abstraction is quite convenient.
On the other hand, there are some features related to IIIS which are not explicitly addressed by the agent approach, such as dependability. Within this context, formal methods have been successfully used to promote confidence on the system behavior. More specifically, the coloured Petri nets (CPN) formal method (Jensen 1992, 1997) is pointed out as suitable for distributed and concurrent systems, which are inherent features of IIIS.
This chapter presents an agent-based approach for formal specification and verification of IIIS using coloured Petri nets. A generic agent-based skeleton CPN model comprising integration and distribution functionalities has been defined. Using this model, it is possible to model and verify agent-based IIIS by only modeling the intelligent functionalities. Distribution, integration and intelligent features are well encapsulated in CPN sub models. Thus, the proposed approach simplifies the IIIS modeling activity and improves its flexibility and maintenance. In order to illustrate the usage of the proposed approach, the modeling and verification of a control parking system is presented.
The remainder of the chapter is organized as follows. In the Background, some related works are discussed and background concepts are presented informally. After, the agent-based formal approach for modeling and verifying IIIS is presented. Next, the modeling and verification of a parking meter control system is presented and some verification results are discussed. In Future Trends, there are some insights and suggestions for future work. In the last section, the chapter is concluded and summarized.