Date of Award


Publication Type

Master Thesis

Degree Name



Computer Science

First Advisor

Chen, X.


Computer Science.




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 view the middleware as a black box. We assume that the abstract behavior of 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.) Paper copy at Leddy Library: Theses & Major Papers - Basement, West Bldg. / Call Number: Thesis2003 .C85. Source: Masters Abstracts International, Volume: 42-02, page: 0613. Adviser: Xiaojun Chen. Thesis (M.Sc.)--University of Windsor (Canada), 2003.