An Educational Case Study of Using SysML and TTool for Unmanned Aerial Vehicles Design

This article shares an experience in using the systems modeling language (SysML) for the design and formal verification of unmanned aerial vehicles (UAVs). In particular, this article shows how our approach helps detecting early design errors. A UAV in charge of taking pictures serves as an educational and running example throughout this article. The SysML model of the UAV is simulated and formally verified using the free and open-source tool named TTool. This educational case study gives the authors of this article an opportunity to draw lessons from teaching SysML.