Open AccessFormal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets
Author(s) -
Awais Qasim,
Syed Asad Raza Kazmi,
Ilyas Fakhir
Publication year - 2015
Publication title -
advances in electrical and computer engineering
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.254
H-Index - 23
eISSN - 1844-7600
pISSN - 1582-7445
DOI - 10.4316/aece.2015.03010
Subject(s) - petri net , computer science , formal methods , programming language , formal verification , formal specification , process architecture , stochastic petri net , temporal logic , model checking , real time computing , distributed computing
In this study we have formally specified and verified the actions of communicating real-time software agents (RTAgents). Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test cases coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability and predictability is expected from real-time software agents. In this research we have used Timed-Arc Petri Net's for formal specification and verification. Formal specification of e-agents has been done in the past using Linear Temporal Logic (LTL) but we believe that Timed-Arc Petri Net's being more visually expressive provides a richer framework for such formalism. A case study of Stock Market System (SMS) based on Real Time Multi Agent System framework (RTMAS) using Timed-Arc Petri Net's is taken to illustrate the proposed modeling approach. The model was verified used AF, AG, EG, and EF fragments of Timed Computational Tree Logic (TCTL) via translations to timed automata