DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles

Lennon Chaves, Iury Bessa, Hussama Ismail, Adriano Frutuoso, Lucas Cordeiro, Eddie B. de Lima Filho

Research output: Contribution to journalArticlepeer-review

196 Downloads (Pure)


During the last decades, model checking techniques have been applied to improve overall system reliability, in unmanned aerial vehicle (UAV) approaches. Nonetheless, there is little effort focused on applying those methods to the control-system domain, especially when it comes to the investigation of low-level implementation errors, which are related to digital controllers and hardware compatibility. The present study addresses the mentioned problems and proposes the application of a bounded model checking tool, named as Digital System Verifier (DSVerifier), to the verification of digital-system implementation issues, in order to investigate problems that emerge in digital controllers designed for UAV attitude systems. A verification methodology to search for implementation errors related to finite word-length effects (e.g., arithmetic overflows and limit cycles), in UAV attitude controllers, is presented, along with its evaluation, which aims to ensure correct-by-design systems. Experimental results show that low-level failures in UAV attitude control software used in aerial surveillance are identified by DSVerifier, which can also be used for developing sound and correct implementations, through its integration into development processes. Finally, given that the proposed approach handles C code and takes into account hardware specifications, it is suitable for verifying final controller implementations, which is a more practical scenario.
Original languageEnglish
Pages (from-to)1420-1441
JournalIEEE Transactions on Reliability
Issue number4
Early online date24 Oct 2018
Publication statusPublished - 24 Oct 2018


  • Unmanned Aerial Vehicle
  • Symbolic Model Checking
  • Fixed-Point Digital Controllers
  • Formal verification
  • Embedded systems


Dive into the research topics of 'DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles'. Together they form a unique fingerprint.

Cite this