| Software testing techniques include peer code reviews, code walkthroughs and testing. Subject to human error, these testing techniques are not ideal testing resources. An alternative approach to verify programs for model correctness is to use model verification tools such as Simple Promela Interpreter (SPIN) and Process Meta-Language (Promela). State explosion is a major drawback of model checking tools. In the case of state explosion, the verification of the model cannot be completed. This thesis attempts to understand the reasons for state explosion and studies proctypes and do loops in Promela. This thesis also checks whether the user can introduce any complexity or state explosion. |
