Bounded Model Checking of Traffic Light Control System

Traffic Light Control System (TLCS) is widely used in our daily life. It is of great importance to ensure the correctness of TLCS. In this paper, bounded model checking (BMC) is chosen to verify a simple but practical TLCS. To this end, Propositional Projection Temporal Logic (PPTL) used as the property specification language and the process of BMC for PPTL are briefly introduced. Then, a TLCS is described and its corresponding Kripke structure is given. Finally, two related properties specified by PPTL formulas are verified for the system using the BMC approach. The verification result using our bounded model checker, BMC4PPTL, shows that the behavior of TLCS is consistent with the specification.