The United States Air Force has become increasingly interested in the problem of verification of complex systems. Formal methods - mathematically based techniques and tools for designing, specifying, and verifying systems - offer a possible solution. One class of formal methods is model checking, in which a mathematical model of a system is checked or verified against a set of system specifications using automated tools. Here, we explore the use of model checking in UAV mission specification and planning. In this context, system specifications become mission specifications, system models become mission execution plans, and mission execution plans are verified against mission specifications. In particular, we focus on mission specification, planning, and verification in a VIP escort mission. Mission specifications are written in linear temporal logic, mission execution plans are modeled in Promela, and mission verification is performed using the model checker Spin.
展开▼
