(: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.}}