期刊名称：Journal of Software Engineering and Applications
印刷版ISSN：1945-3116
电子版ISSN：1945-3124
出版年度：2015
卷号：08
期号：02
页码：43-50
DOI：10.4236/jsea.2015.82006
语种：English
出版社：Scientific Research Publishing
摘要：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)
