Program Design Guidelines for Model Checking: Most of the significant software development projects use some kind of design and coding guidelines. There exist many such guidelines, some including tens or even hundreds of rules covering almost all aspects of development—from the use of white spaces, naming conventions, and comments to recommendations on what specific language features to use or avoid (MISRA 2004; Meyers 2005; Sutter 1999; Sutter 2004). The choice of language and also the type of application that is developed obviously play an important part in the set of rules that are applicable in practice. Some rules may contradict or be inconsistent with other rules within the same guideline document. Therefore developers are often forced to follow some of the rules and ignore others. With no automated checking of compliance, many violations of these guidelines often go unnoticed.
There does not seem to be a consensus on what makes a good guideline in common. Even less obvious is the effect of some of these guidelines on software verifiability. (Holzmann 2006) proposes 10 rules that could have measurable effect on software reliability and verifiability. He argues that although the proposed small set of rules cannot be all-encompassing, setting an upper bound can increase the effectiveness of the guideline. In this section we describe a number of recommended design and coding guidelines which can be used effectively to tame the state explosion problem and also to decrease the amount of effort that is needed to use a model checker to verify properties of interest.