Model checking is a fully automatic approach to verify a finite state machine against its temporal specifications. However, its application is limited by the size of the system to be verified. Model reduction is one of the methods to tackle this problem.  In this paper, we proposed a model reduction approach which is based on syntactic analysis of programs.  The value domains of the state variables are extracted and analyzed based on the control flow diagram. The approach is sound based on the fact that the reduced system simulates the concrete system with respect to the properties. Throughout the analysis, we can find that the proposed approach is efficient on data-path heavy systems. We also made a simple case study in the paper to show its performance.

Download postscript file (PS File)

Send comments and suggestions to: tahar@ece.concordia.ca