Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets
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 pr...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Stefan cel Mare University of Suceava
2015-08-01
|
Series: | Advances in Electrical and Computer Engineering |
Subjects: | |
Online Access: | http://dx.doi.org/10.4316/AECE.2015.03010 |
Summary: | 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. |
---|---|
ISSN: | 1582-7445 1844-7600 |