Formalization and Verification for Mid-block Street Crossing Signal Control

Current methods, for modeling urban traffic controlling system, are lack of formal description of system behaviors and cannot verify the specifications. The process of mid-block street crossing is a typical course which involves human behavior, vehicle behavior, traffic control behavior, and safety issue of transportation. This process has the character of sequential process with concurrent event. Description method for concurrent event and communication by Communication Sequential Processes (CSP) and basic notation, axiom, theorem and deducing rules of Duration Calculus (DC) are used for modeling. On the basis of analysis of mid-block street crossing, a formal model of the process of signal control based on CSP and DC is established. Through verification, the model satisfies the safety requirements.