A comprehensive survey of UPPAAL-assisted formal modeling and verification

UPPAAL is a formal modeling and verification tool based on timed automata, capable of effectively analyzing real-time software and hardware systems. In this article, we investigate research on UPPAAL-assisted formal modeling and verification. First, we propose four research questions considering tool characteristics, modeling methods, verification means and application domains. Then, the state-of-the-art methods for model specification and verification in UPPAAL are discussed, involving model transformation, model repair, property specification, as well as verification and testing methods. Next, typical application cases of formal modeling and verification assisted by UPPAAL are analyzed, spanning across domains such as network protocol, multi-agent system, cyber-physical system, rail traffic and aerospace systems, cloud and edge computing systems, as well as biological and medical systems. Finally, we address the four proposed questions based on our survey and outline future research directions. By responding to these questions, we aim to provide summaries and insights into potential avenues for further exploration in this field.