Enhancing the Dependability of Complex Missions Through Automated Analysis
Abstract
The increasing complexity of current uninhabited aerial vehicle (UAV) missions is overwhelming human mission developers, and automated mission planning systems and simulation environments. The objective of this project was to enhance the dependability of complex UAV missions with the application of modern automated program analysis techniques. The key insight supporting this project was the treatment of a mission plan as a type of software or software representation, which could be analyzed with software verification methods, including model checking and probabilistic model checking, to detect potential errors before mission execution. The key contribution of this work is a novel method for domain-specific model checking called "cascading verification." The method uses composite reasoning over high-level system specifications and formalized domain knowledge to synthesize both low-level system models and the behavioral properties that need to be verified with respect to those models. In particular, model builders use a high-level domain-specific language (DSL) to encode system specifications that can be analyzed with model checking. Domain knowledge is encoded in the Web Ontology Language (OWL), the Semantic Web Rule Language (SWRL) and Prolog, which are combined to overcome their individual limitations. Synthesized models and properties are analyzed with the probabilistic model checker PRISM. Cascading verification is illustrated with a prototype system that verifies the correctness of UAV mission plans. An evaluation of this prototype reveals non-trivial reductions in the size and complexity of input system specifications compared to the artifacts synthesized for PRISM.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2013
- Accession Number
- ADA590643
Entities
People
- David S. Rosenblum
- Fokion Zervoudakis
Organizations
- University College London