J. Chen and F. Li (Canada)
Concurrency, Nondeterminism, Formal Specification, Fi nite State Machines, SPIN, Model Checking
With the availability of many concurrent programming lan guages nowadays and the increasing need for applications in a multithreaded and/or distributed environment, design and implement concurrent systems is getting more and more popular among ordinary software developers. How ever, concurrent systems are usually much more complex to analyze statically or test dynamically mainly due to their internal nondeterminism. In the present work, we apply model checking technique to statically detect in a design specification, potential errors caused by improper control of interprocess synchronization. We assume that the de sign specification is FSM-based: the behavior of each pro cess is expressed via a finite state machine and the design specification is composed of a multiset of finite state ma chines together with an environment shared by all of the processes. Transitions on the state machines may contain information about process synchronization. In this paper, we consider the process synchronization mechanism from Java monitors. The formal verification of the correctness in this context is realized by an automated translation from given design specifications into Promela descriptions, so that we can reuse existing model checking tool SPIN to for mally verify certain properties which may be hard to detect by applying general testing techniques on final code.
Important Links:
Go Back
