LAUSR

The difficulty of finding resources race is well known. Such errors are hard to be detected, because they often happen irregularly and reproduce difficultly. Especially, the kind race conflicts exist among processes, threads, and interrupts. This paper provided a novel approach to detect the resources race, namely software model checking. It constructed Boolean program and Promela models for resources race. Furthermore, the Promela models have been tested by using the model checker, SPIN. Software model checking can detect resources race in concurrent program without running, although the program had used timing control or mutual exclusion lock to avoid the race. Furthermore, it can find deadlock also, if the program use the mutual locks in a wrong way.