Verification and controller synthesis for resource-constrained real-time systems: Case study of an autonomous truck

An embedded system is often subject to timing constraints, resource constraints, and it should operate properly no matter how its environment behaves. This paper proposes to use timed game automata to characterize the timed behaviors and the environment uncertainties, and use piece-wise constant integer functions to approximate the continuous resources in real-time embedded systems. Based on these formal models and techniques, we employ the realtime model checker UPPAAL to verify a system against a given functional and/or timing requirement. Furthermore, we employ the timed game solver UPPAAL-TIGA to check whether a given control objective can be enforced, and if so, we synthesize a controller for the system. We carry out a case study of this approach on a battery-powered autonomous truck. Experimental results indicate that the method is effective and computationally feasible.