In previous works, Hierarchical Hybrid Automata (HHA) have been proposed as a combination of UML state machine diagrams and hybrid automata to model complex and in particular multi-agent systems. This approach enables formal system specification on different levels of abstraction and expresses realtime system behavior. A prototype was implemented using constraint logic programming (CLP) as a framework to specify and verify these HHA. However, it still requires the user to write a CLP program in order to specify the HHA, which is a tedious and error-prone work. Therefore, this paper aims at simplifying the verification process by introducing a tool environment where a HHA model together with requirements are entered graphically and the process of verification is achieved automatically.
展开▼
