Inserting Property Oracles: A property oracle is a program or a piece of code that says whether or not a property holds during model checking. The process of inserting this (often conditionally compiled code) in the program is called instrumentation.
While non-functional properties like deadlocks and memory leaks do not have to be expressed explicitly in the program sources, functional properties, describing application-specific functionality like state consistency and correctness of computations, needs explicit instrumentation.
For program model checking, this instrumentation takes the form of annotations and code extensions which are inserted in the source. You must be careful about where these are inserted. Do not insert them in the code at intermediate states where the property is not expected to hold, only where the program is in a consistent state. We call these places checkpoints. For example, the code for calculating some time interval value may span multiple statements. The checkpoints for verifying that the value is within some predefined range can be before the first and after the final statement involved in that calculation. Checking the code at any other point in between may lead to false positives or negatives, as the check may be using intermediate values.
You can use the requirements, the verification and validation matrix, the existing design models (if any), and the expertise of those with domain knowledge to identify these checkpoints. In the case of SAFM, for some properties we had to get confirmation from the domain experts to make sure that we were inserting our instrumentation at the right places.
There are different techniques for inserting property oracles into programs. Two of these mechanisms discussed here are Programming by Contract and Aspect-Oriented Programming. Note that these are complementary techniques, and may be used in combination.