Using Model Checking to Detect Deadlocks in Distributed Object Systems

Abstract. We demonstratehow the use of synchronizationprimitives and threading policies in distributed object middleware can lead to deadlocks. We identify that objectmiddleware only hasa few built-in synchronizationandthreading primitives. We suggest to express them as stereotypes in UML models to allow designers to model synchronization and threading of distributed object systems at ate levels of abstraction. We define the semantics of these stereotypes by a mapping to a process algebra. This allows us to use model checking techniques that are available for process algebras to detect the presence or absence of deadlocks. We also discuss how the results of these model checks can be related back to the UML diagrams.

• Type: Conference
• Year: 2000
• Where: EDO
• Authors: Nima Kaveh
• Keywords: Built-in Synchronizationandthreading Primitives, Distributed And Parallel Computing, Distributed Object, EDO 2000, Process Algebras