Abstract
This paper proposes an approach to producing a verified design of a complex intelligent system. The system is modeled using a hierarchical structure based on a coordination protocol. The coordination protocol and the system architecture are described using a state machine representation. The Clarke-McMillan Symbolic Model Checker based on branching time temporal logic is used to verify some of the desired formal properties of the protocol such as completeness, boundedness and termination. This work shows that the model checker helps to bring the automatic verification of complex intelligent systems closer to a practical proposition.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Thomas, J. Design and verification of a coordination protocol for cooperating systems. Soft Computing 4, 130–140 (2000). https://doi.org/10.1007/s005000000047
Issue Date:
DOI: https://doi.org/10.1007/s005000000047