Paper Infomation
Formalization and Verification for Mid-block Street Crossing Signal Control
Full Text(PDF, 285KB)
Author: Xiangjun Cheng, Peng Du
Abstract: 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.
Keywords: Formal Methods,Mid-block Street Crossing, Communication Sequential Processes,Duration Calculus; Safety Analysis
References:
[1] Antonio Cerone,Simon Connelly,Peter Lindsay. Formal Analysis of Human Operator Behavioral Patterns in Interactive Surveillance Systems. SoftwSystModel (2008)7:273–286
[2] Lindsay, P. and Connelly, S.. Modeling Erroneous Operator Behaviors for an Air-Traffic Control Task. In J. Grundy and P. Calder, editors, Third Australasian User Interfaces Conference (AUIC2002), volume 7 of Conferences in Research and Practice in Information Technology, pages 43–54. Australian Computer Society, Inc, 2002
[3] Aleksandra, Veljko. Formal Specification and Preliminary Design of an Asynchronous Traffic Light Controller. PROC. 23nd International Conference on Microelectronics (MIEL 2002): 679-682
[4] Yasunori Shiono, etc. Efficiency of concurrent processing of sort using CSP[C]. 2012 13th ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing. Pp:524-529
[5] Ryo Mizutani, Kenji Ohmori. A Design and Implementation Method for Embedded Systems using Communicating Sequential Processes with an Event-Driven and Multi-Thread Processor[C]. 2012 International Conference on Cyberworlds. Pp:221-225
[6] Touta Hayashi, Kenji Ohmori. An Autonomous Vehicle Using a Multi-Thread and Event-Driven Processor[C]. 2011 International Symposium on Integrated Circuits. Pp:305-308
[7] C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
[8] Zhou Chaochen.Michael R. Hansen. Duration Calculus: A Formal Approach to Real-Time Systems [M]. Springer-Verlag Berlin Heidelberg, 2004
[9] 承向军，应志鹏，杜鹏。高速列车ATP控制模式的形式化模型与安全性分析[J]。中国安全科学学报，2008年第3期，pp：28-32。[Cheng Xiangjun, Ying Zhipeng, Du Peng. Formalization Model of High Speed Train in ATP Control and Its Safety Analysis[J]. China Safety Science Journal, Vol. 18, No.3, 2008:28-32.]