The paper shares an experience in using the Systems Modeling Language (SysML) for the design and formal verification of UAVs. In particular, the paper shows how our approach helps detecting early design errors. A UAV in charge of taking pictures serves as educational and running example throughout the paper. 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 the paper an opportunity to draw lessons from teaching SysML.