Formal specification of software critical systems with agents

This paper presents a method called I²AM (interaction and intention-based agent method), which is an attempt to bridge the gap between system analysis and its formal specification. The method integrates the agent ontology and timed Petri net, an extension of the colored Petri net. The agent ontology allows expressive elicitation and representation of knowledge. An agent is an entity considered to be subject of interactions and intentions. An interaction is a collective action wherein one agent takes an action or a decision influenced by other agents. An intention characterizes some attitudes such as belief, knowledge, desire, commitment, or choice. Modeling such an intentional system provides an abstraction useful in requirement analysis. The I²AM method allows one to prove non-functional properties expressed with temporal logic on such multi-agent systems