Formal analysis of an urban road traffic model

Abstract

The paper proposes a method based on timed automata to validate different road traffic control scenarios. In order to estimate the current traffic state, a strategy in which a special attention was given to information collected from the streets converging to main crossroads was elaborated. Then, the up to dated information was used by a complex road traffic model to improve the traffic flow. The validation and verification of the road traffic model was realized using UPPAAL model-checker. A representative area of Cluj Napoca city center was modeled and simulated in order to determine the right parameters for traffic control. The proposed model, validated in UPPAAL, can be extended to any road structure for analysis purposes.