Formal Specification And Modeling Of Intelligent Traffic Light

Along with the continuing growth of the social productivity and the consistent improvement of human society, the urbanization level is higher and higher and the urban transport problem is becoming more serious every day in many developing nations like our country, the traffic jam is obvious to each of us. There are basically three main reasons. One: The capacity of intersection is insufficient. Two:the directional network is unreasonable. Three :the management and control of traffic flow is weak. There are two general ways to resolve the urban transport problem: enhancing the construction of urban transportation infrastructure facilities and reinforcing traffic control. But the build and extension of urban roads still fall far short of rapid growth in automobiles,so the rational utilization to existing roads and effective management to traffic signals are important ways to improve traffic condition. Therefore studying traffic control system have important significance in theory and practice.The paper focuses on the modeling method to urban traffic signal control,the main work includes the following:(1) Giving a formal description to traffic signal control, describing the model and analysis using Petri nets in design. Giving the formal description and analysis conclusion to a concrete traffic signal lights control system.(2) Establishing timed Petri net model of traffic signal light using Petri nets, realizing the incidence matrix using C language, analysising the model using informed analysis tools, final giving the flow of traffic signal timing optimal design procedure based on Petri nets.