Modular consistency analysis of component-based designs

In this article, we present a practical analysis approach that makes use of the modular nature of component-based designs to alleviate the state space explosion problem, a well-known obstacle to system verification. The key is to specify interaction protocols for components using a lightweight formal language and then to utilise these protocols as contracts for independent analysis of the components and their interactions. These protocols are often missing or informally documented. It is demonstrated how consistency properties of closed and open component-based designs can be verified using this divide-and-conquer approach.