Design of telecommunication services based on software agent technology and formal methods

We propose an approach based on software agent technology and formal methods for designing telecommunication services. This approach aims to identify agent and interaction-oriented design patterns and to describe them with a formalism enabling one to prove their quality. These patterns are based on a classification of agents interactions using the interaction model of the Reference Model of Open Distributed Processing (RM-ODP). The formalism offers a methodology for validation and verification based on Petri nets. With such an approach, it is possible to specify some components with proven properties that guarantee their quality. We illustrate it with an example: a multi-agent system of a contract monitoring