Specification and verification of multi-agent applications using temporal Z

This work suggests a formal approach for specifying and verifying multi-agent applications. This approach provides a specification language which integrates temporal logic in the Z notation allowing, in this way, to cover static, behavioural, as well as dynamic aspects of a multi-agent application....

Full description

Saved in:
Bibliographic Details
Main Authors: Regayeg, A., Hadj Kacem, A., Jmaiel, M.
Format: Conference Proceeding
Language:English
Subjects:
Application software
Formal specifications
Intelligent agent
Laboratories
Logic
Multiagent systems
Protocols
Software engineering
Specification languages
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This work suggests a formal approach for specifying and verifying multi-agent applications. This approach provides a specification language which integrates temporal logic in the Z notation allowing, in this way, to cover static, behavioural, as well as dynamic aspects of a multi-agent application. Then, we present the syntax and the semantics of the proposed language, particularly, we provide a temporal model according to the framework of Z. Our approach allows us to rigourously reason about interesting properties of multi-agent systems. Finally, we illustrate our approach by verifying an agent based specification for the pursuit problem. We make use of the Z/EVES tools to analyse and reason about our specifications.
DOI:10.1109/IAT.2004.1342953