| Here we present a formal verification technique for the correctness of the design models of the component-based distributed applications where the inter-process communications are realized via general middleware layers.; We give a suitable extension of UML statechart diagrams. With this extension, the components and the communications among them in a middleware-based distributed application can be clearly expressed, and the software developers can actually the distributed application is given in such notations using any UML tool capable of saving the design in the standard XMI format. Two specially formatted deployment files are used to set up a concrete system from the design specification. The verification of its correctness is achieved by converting the design model, together with the deployment details, into a formal verification model in specification language PROMELA. (Abstract shortened by UMI.)... |
