Property Based Design Testing

FSMs play an important role in protocol design. Current techniques of FSM testing are statistical which rely on simulation. These techniques often fail to find some critical cases in the FSMs. Using formal verification,FSM validation can be done independent of the number of inputs and the actual transition data. In this paper we explain formal properties for validation of FSM machines. We show that four groups of properties can test an FSM for all state transition faults.

Keywords:

Verification , Model Checking , Protocol , FSM , BDD , MDD , CTL , Image Computation , Reachability Analysis.