Hybrid control and model-based assertions for autonomous intersection management system as a cyber-physical system

A cyber-physical system (CPS) consists of multiple physical components that collab- orate through a network during real-time operation according to system-level commands. A hybrid control, which generates discrete system-level commands and handles the low-level physical dynamics for each component, is of singular importance to a CPS. For a CPS, live- ness and safety require that the system is always eventually doing what is desirable without any undesirable behavior, and have to be carefully addressed. The advance in information technology and autonomous driving make it possible to establish an autonomous intersection management system (AIMS) for ground autonomous vehicles, which can potentially improve traffic efficiency and reduce intersection car accidents. This work presents a hybrid control and introduces model-based assertions for such an AIMS. System-level traffic requirements are expressed in the form of linear temporal logic (LTL) specifications in the generalized reactivity formulas with rank 1 (GR(1)) and a two-player game is solved to synthesize a discrete traffic network controller. DaNI, a motor-driven laboratory robot vehicle, is mod- eled using a bond-graph approach, and a nonlinear vehicle trajectory sliding-mode controller (SMC) is mathematically and numerically described. The discrete traffic controller instructs each robot vehicle to pass through the intersection of interest at a certain time and the vehicle’s trajectory within the intersection is controlled by the SMC. Using simulation, it is shown that the synthesized discrete controller is able to determine proper system actions in response to traffic data and environmental actions while maintaining liveness and safety specifications. A laboratory study on a simple AIMS is demonstrated to depict the basic design structure of a AIMS as a CPS. The results suggest that model-based assertions, which monitor and validate a CPS by assertions based on physical models, can be helpful in de- tecting physics-related abnormalities during operation of a CPS that may not be captured by a software-level analysis. Using simulations, it is shown how the accuracy of a continuous vehicle trajectory controller, such as a SMC, can provide informative guidance on the design of model-based assertions.