Abstract
In this paper, we present our study on statically analyzing design artifacts in multithreaded systems to check the correctness with respect to the nondeterministic behavior of the systems. The description of an abstract behavior of a multithreaded system on design stage can be naturally decomposed into the descriptions of the behavior of each thread and the description of the interactions among these threads. We assume that the behavior of each thread is described in terms of synchronizing finite state machine, a special finite state machine whose transitions may contain information about thread synchronization. Such information is expressed by way of some well-known synchronization mechanism from implementation languages. For the moment, we consider synchronization among multiple threads via shared objects, governed by Java monitors. The operational semantics for a network of such synchronizing finite state machines is provided in terms of labeled transition systems. The defined formal model is the basis for formally reasoning about the correctness of the design against certain properties that, due to the nondeterminism involved, may be hard to detect by testing final code.