Automated analysis of consensus protocol in specifcation of multi-agents coordination - Binh, Trinh Thanh; Thuan, Truong Ninh; Ha, Nguyen Viet (VNU Journal of Science: Natural Sciences and Technology; Vol 28 No 1, 2012)
Abstract . Formal specification and reasoning techniques in software modelling are needed to ensure the correctness of the system at the design phase. Event-B is a formal method with support tools that allows the specifcation and verifcation of reactive systems. In this article, we propose an approach to specify capabilities of a number of software agents. We also verify whether these capabilities help the agents to accomplish a task using a support tool of  Event-B. In our previous paper, we have presented about the specifcation and verifcation of sequential protocols. We extend in this article the one of combination between the sequential and parallel protocols of multi-agents software.