Property Identification: In order to perform model checking, you need to specify a number of properties that the application under analysis must satisfy. JPF detects certain generic properties by default—for example, “no assertion violations” and certain concurrency-related properties such as “no deadlocks” and “no race conditions.” The other type of properties that can be checked by JPF are application-specific properties. Since SAFM was a single-threaded application which by default did not contain any assertions, the only properties that we could concentrate on were application-specific properties that required domain knowledge. We worked closely with the SAFM developers, particularly the SAFM test personnel, and identified a number of those properties. The properties werethen tested using the existing SAFM test suite. In some cases, this revealed violations of the initial properties so that iteration with the developers was necessary to correctly formulate the properties. In the more interesting cases, it revealed implementation defects in SAFM.