Behavior Specification of a Red-Light Violation Warning Application - An Approach for Specifying Reactive Vehicle-2-X Communication Applications

Current intelligent transportation systems are based on Vehicle-2-X communication. They accomplish the next level of cooperative advanced driver assistance systems. Since these Vehicle-2-X communication applications are often located in the safety critical areas, high quality demands arise. One part of these requirements is the correct functional behavior. For its validation, a formal specification is required. In this paper, the Red-Light Violation Warning application is used. To specify all the functionality, Continuous-Time State Machines (CTSM) are introduced. Such, a formal specification of a Vehicle-2-X application is given and, consequently, no unintended ambiguities exist furthermore.