| 3/2015 - 10 |
Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri NetsQASIM, A.   , KAZMI, S. A. R. , FAKHIR, I. |
Extra paper information in    |
| Click to see author's profile in SCOPUS, IEEE Xplore, Web of Science |
Download PDF  (1,146 KB) | Citation | Downloads: 801 | Views: 3,364 |
Author keywords
formal specifications, formal verification, multiagent systems, Petri nets, real time systems
References keywords
systems(13), agent(11), multi(8), petri(5), software(4), modeling(4)
Blue keywords are present in both the references section and the paper title.
About this article
Date of Publication: 2015-08-31
Volume 15, Issue 3, Year 2015, On page(s): 73 - 78
ISSN: 1582-7445, e-ISSN: 1844-7600
Digital Object Identifier: 10.4316/AECE.2015.03010
Web of Science Accession Number: 000360171500010
SCOPUS ID: 84940733873
Abstract
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. |
| References | | | Cited By |
Web of Science® Times Cited: 11 [View]
View record in Web of Science® [View]
View Related Records® [View]
Updated today
SCOPUS® Times Cited: 11
View record in SCOPUS® [Free preview]
View citations in SCOPUS® [Free preview]
Updated today
[1] Intelligent agent for formal modelling of temporal multi-agent systems, Qasim, Awais, Aziz, Zeeshan, Kazmi, Syed Asad Raza, Khalid, Adnan, Fakhir, Ilyas, Hassan, Jawad, International Journal on Smart Sensing and Intelligent Systems, ISSN 1178-5608, Issue 1, Volume 13, 2020.
Digital Object Identifier: 10.21307/ijssis-2020-003 [CrossRef]
[2] Formal Specification and Verification of Self-Adaptive Concurrent Systems, Fakhir, Muhammad Ilyas, Kazmi, Syed Asad Raza, IEEE Access, ISSN 2169-3536, Issue , 2018.
Digital Object Identifier: 10.1109/ACCESS.2018.2849821 [CrossRef]
[3] Agent systems verification : systematic literature review and mapping, Bakar, Najwa Abu, Selamat, Ali, Applied Intelligence, ISSN 0924-669X, Issue 5, Volume 48, 2018.
Digital Object Identifier: 10.1007/s10489-017-1112-z [CrossRef]
[4] Formal Modelling of Real-Time Self-Adaptive Multi-Agent Systems, Qasim, Awais, Raza Kazim, Syed, Intelligent Automation and Soft Computing, ISSN 1079-8587, 2018.
Digital Object Identifier: 10.31209/2018.100000012 [CrossRef]
[5] SMACS: A framework for formal verification of complex adaptive systems, Fakhir, Ilyas, Kazmi, Asad Raza, Qasim, Awais, Ishaq, Atif, Open Computer Science, ISSN 2299-1093, Issue 1, Volume 13, 2023.
Digital Object Identifier: 10.1515/comp-2022-0275 [CrossRef]
[6] Handling temporal constraints in interaction protocols for intelligent multi-agent systems, Qasim, Awais, Iqbal, Sobia, Aziz, Zeeshan, Kazmi, Syed Asad Raza, Munawar, Adeel, Gilani, Basit Ali, Qasim, Neelam, International Journal on Smart Sensing and Intelligent Systems, ISSN 1178-5608, Issue 1, Volume 13, 2020.
Digital Object Identifier: 10.21307/ijssis-2020-020 [CrossRef]
[7] MAPE-K Interfaces for Formal Modeling of Real-Time Self-Adaptive Multi-Agent Systems, Qasim, Awais, Kazmi, Syed Asad Raza, IEEE Access, ISSN 2169-3536, Issue , 2016.
Digital Object Identifier: 10.1109/ACCESS.2016.2592381 [CrossRef]
[8] Formal modeling and verification of cloudâbased web service composition, Raza Kazmi, Syed Asad, Qasim, Awais, Khalid, Adnan, Assad, Ruttaba, Shahbaz, Muhammad, Concurrency and Computation: Practice and Experience, ISSN 1532-0626, Issue 21, Volume 32, 2020.
Digital Object Identifier: 10.1002/cpe.5249 [CrossRef]
[9] Efficient Performative Actions for E-Commerce Agents, Qasim, Awais, Ameen, Hafiz Muhammad Basharat, Aziz, Zeeshan, Khalid, Adnan, Applied Computer Systems, ISSN 2255-8691, Issue 1, Volume 25, 2020.
Digital Object Identifier: 10.2478/acss-2020-0003 [CrossRef]
Updated today
Disclaimer: All information displayed above was retrieved by using remote connections to respective databases. For the best user experience, we update all data by using background processes, and use caches in order to reduce the load on the servers we retrieve the information from. As we have no control on the availability of the database servers and sometimes the Internet connectivity may be affected, we do not guarantee the information is correct or complete. For the most accurate data, please always consult the database sites directly. Some external links require authentication or an institutional subscription.
Web of Science® is a registered trademark of Clarivate Analytics, Scopus® is a registered trademark of Elsevier B.V., other product names, company names, brand names, trademarks and logos are the property of their respective owners.
Copyright ©2001-2024
Faculty of Electrical Engineering and Computer Science
Stefan cel Mare University of Suceava, Romania
All rights reserved: Advances in Electrical and Computer Engineering is a registered trademark of the Stefan cel Mare University of Suceava. No part of this publication may be reproduced, stored in a retrieval system, photocopied, recorded or archived, without the written permission from the Editor. When authors submit their papers for publication, they agree that the copyright for their article be transferred to the Faculty of Electrical Engineering and Computer Science, Stefan cel Mare University of Suceava, Romania, if and only if the articles are accepted for publication. The copyright covers the exclusive rights to reproduce and distribute the article, including reprints and translations.
Permission for other use: The copyright owner's consent does not extend to copying for general distribution, for promotion, for creating new works, or for resale. Specific written permission must be obtained from the Editor for such copying. Direct linking to files hosted on this website is strictly prohibited.
Disclaimer: Whilst every effort is made by the publishers and editorial board to see that no inaccurate or misleading data, opinions or statements appear in this journal, they wish to make it clear that all information and opinions formulated in the articles, as well as linguistic accuracy, are the sole responsibility of the author.
Faculty of Electrical Engineering and Computer Science
Stefan cel Mare University of Suceava, Romania
All rights reserved: Advances in Electrical and Computer Engineering is a registered trademark of the Stefan cel Mare University of Suceava. No part of this publication may be reproduced, stored in a retrieval system, photocopied, recorded or archived, without the written permission from the Editor. When authors submit their papers for publication, they agree that the copyright for their article be transferred to the Faculty of Electrical Engineering and Computer Science, Stefan cel Mare University of Suceava, Romania, if and only if the articles are accepted for publication. The copyright covers the exclusive rights to reproduce and distribute the article, including reprints and translations.
Permission for other use: The copyright owner's consent does not extend to copying for general distribution, for promotion, for creating new works, or for resale. Specific written permission must be obtained from the Editor for such copying. Direct linking to files hosted on this website is strictly prohibited.
Disclaimer: Whilst every effort is made by the publishers and editorial board to see that no inaccurate or misleading data, opinions or statements appear in this journal, they wish to make it clear that all information and opinions formulated in the articles, as well as linguistic accuracy, are the sole responsibility of the author.
