The behaviour of a distributed system is largely determined by the use of synchronization primitives and threading policies of the underlying middleware. The inherent parallel nature of distributed systems may cause liveness problems, such as deadlocks and livelocks. An increasing number of distributed systems is built using object middleware. We exploit the fact that modern object middleware offers only a few built-in synchronization and threading primitives by suggesting UML stereotypes to represent each of these primitives in distributed object design. We define the semantics of the stereotypes using a process algebra. We use that semantics to translate UML diagrams into behaviourally equivalent process algebra representations and can then use model checking techniques to find potential deadlocks. The paper also shows how the model checking results can be related back to the original UML diagrams.
展开▼
