Finite State Verification of Intelligent Transportation Systems

Intelligent transportation systems (ITS) represent a major initiative to improve roadway and travel conditions, not by building roads, but by drawing on new technologies in computing, sensing, and communications. However, these technologies are extremely complex and, while some demonstration projects have tested stand-alone systems, the broader architectural and standardization issues are still under development. The use of complex technologies in a safety-critical system such as ITS and at the scale envisioned requires a very careful study of the interaction between its various subsystems. This paper describes an approach for modeling the temporal aspects of ITS systems as well as their logical coordination using finite state verification tools. The approach is demonstrated by verifying safety properties of an automated traffic signal at a road intersection.