APPLICATION OF MODEL CHECKING TO THE VERIFICATION OF DIGITAL SYSTEMS
Daniela Kotmanová, Milan Kolesár · 2009
The article presented here deals with the verification of a digital design using temporal logic and model checking. Temporal logic has been used as a specification language to catch the behaviour of the system design and model checking has been chosen as a verification method to evaluate the design accuracy. As a digital system to be modelled and verified we have chosen the sequence detector; the detected string is 010. To compare the way how to establish temporal model and its properties and to see better coincidences and differences in describing their behaviour we made up the model of the sequence detector in two variants: without and with overlapping. We took, as finite state machine (FSM), the both automata, the Moore as well as the Mealy, each considered without and with overlapping. After the temporal properties of the four drawn models had been defined we wrote respective programs corresponding to each of models, in SMV language, to pass them as input files into the SMV model checker. Finally, we tested the correctness of the models without and with overlapping also by submitting temporal properties of the weaker sequence detector to the stronger – the result was satisfying because all the fundamental properties of the Moore FSM without overlapping were verified also by the weaker Moore FSM with overlapping. Given the limited space available we made only this experiment, the other- with the Mealy FSM, could not be performed.