Author(s)

Nadeem Akhtar, Muhammad Nauman

Department of Computer Science and IT, The Islamia University of Bahawalpur, Baghdad-ul-Jadeed Campus, Bahawalpur, Pakistan.

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.

Software Correctness, Formal Verification, Model Checking, Timed-Automata, Multi-Agent System, Timed Computation Tree Logic (TCTL)

Akhtar, N. and Nauman, M. (2015) Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study. Journal of Software Engineering and Applications, 8, 43-50. doi: 10.4236/jsea.2015.82006.