TITLE:
Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study
AUTHORS:
Nadeem Akhtar, Muhammad Nauman
KEYWORDS:
Software Correctness, Formal Verification, Model Checking, Timed-Automata, Multi-Agent System, Timed Computation Tree Logic (TCTL)
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.8 No.2,
February
12,
2015
ABSTRACT: A multi-agent based transport system is
modeled by timed automata model extended with clock variables. The correctness
properties of safety and liveness of this model are verified by timed automata
based UPPAAL. Agents have a degree of control on their own actions, have their
own threads of control, and under some circumstances they are also able to take
decisions. Therefore they are autonomous. The multi-agent system is modeled as
a network of timed automata based agents supported by clock variables. The representation
of agent requirements based on mathematics is helpful in precise and
unambiguous specifications, thereby ensuring correctness. This formal
representation of requirements provides a way for logical reasoning about the
artifacts produced. We can be systematic and precise in assessing correctness
by rigorously specifying the functional requirements.