Model checking distributed objects
W. Emmerich, Nima Kaveh · 2000
We demonstrate how the use of synchronization primitives and threading policies in object middleware can lead to deadlocks. We identify that object middleware only has a few built-in synchronization and threading primitives and suggest to express them as stereotypes in UML models. We define the semantics of these stereotypes by a mapping to a process algebra. Finally, we apply model checkers to this process algebra notation and show that we are able to detect the possibility of deadlocks that can then be related back to the UML models. 1 Introduction The increasing demand for distributed applications in a wide variety of fields has increased the commercial attention to middleware. Like so many other technologies, middleware has grown from being a research topic into a maturing commercial technology. A large number of distributed systems are built using middleware, which shields the use of networking protocols from the application programmer. There are different categories of mid...