(:notitlegroup:)
@inproceedings{hongliu2016, title = {Model Checking for the Fault Tolerance of Collaborative AUVs}, booktitle = {2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE)}, author = {Hong Liu and Tianyu Yang and Jing Wang}, pages = {244-245}, month = {January}, year = {2016}, keywords = {artificial intelligence;autonomous underwater vehicles;control engineering computing;formal verification;hardware-software codesign;middleware;software architecture;software fault tolerance;Eco-Dolphin;UPPAAL;autonomous underwater vehicles;collaborative AUV;collaborative AUV fleet;concurrent subsystems;fault tolerance;formal method;intractable AI-inspired algorithms;middleware MOOS-IvP;model checking tool;software architecture;software design patterns;software-hardware codesign;state explosion problem;system design;Computational modeling;Computers;Fault tolerance;Fault tolerant systems;Model checking;Software;Unified modeling language;Autonomy Software Architecture;Collaborative AUVs;Fault Tolerance;Model Checking}, abstract = {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.}}