A programmable controller (PC) programming technique using SFC (sequential function chart) has been adopted in sequential control system design because SFC can graphically represent the sequence how of control logic. However, when we design an SFC program, we must verify the program with the design specifications. For this purpose, we can use scenario simulation and exhaustive simulation. In this paper, we propose to model both the controlled object and the SFC program by a Petri net for verification by both types of simulations.