Model Checking for the Fault Tolerance of Collaborative AUVs
Hong Liu, Tianyu Yang, Jing Wang · 2016
This concept paper presents the preliminary work on the application of formal method to verify the correctness of software-hardware co-design. A model checking tool called UPPAAL is used to check the fault-tolerance of the system design. The paper briefly describes the hardware platform, a fleet of collaborative AUVs (autonomous underwater vehicles) named Eco-Dolphin, and its software architecture based on the middleware MOOS-IvP. Because many autonomy software systems have large sets of state variables and are associated with intractable AI-inspired algorithms, the practice of model checking for autonomy software is severely hindered by the state explosion problem. Our work is to demonstrate how software design patterns and architecture styles can be utilized to decompose a system with intractable large state space into several concurrent subsystems with tractable state spaces.