Model Checking for Verification in UAV Cooperative Control Applications

You are here: Homepage > Search

Model Checking for Verification in UAV Cooperative Control Applications

Humphrey, Laura R.

Recently, there has been an increased interest in verification techniques for complex, autonomous systems. Consider for instance a scenario in which individual autonomous agents must work together to complete a series of constrained tasks. In cases such as this, there is a need for techniques to verify that the agents interact correctly, i.e. that they are able to cooperatively complete the required tasks while satisfying the constraints. Current research suggests that standard software modeling and verification techniques such as model checking can be extended to meet this need. Here, we explore the use of model checking for verification in three scenarios that include a team of unmanned aerial vehicles. The first scenario involves a centralized cooperative control scheme, the second involves a decentralized cooperative control scheme, and the third involves high-levelmission planning. For these scenarios, tasks and constraints are written in linear temporal logic, scenario models are coded in Promela, and the models are verified using the model checker Spin .