The main objective of my research was to enhance the dependability of complex uninhabited aerial vehicle (UAV) missions with the application of modern automated program analysis techniques. The resulting thesis describes a novel method for domain-specific model checking called cascading verification. The method uses composite reasoning over high-level system specifications and formalized domain knowledge to synthesize both low-level system models and the behavioral properties that need to be verified with respect to those models. Synthesized models and properties are analyzed with the probabilistic model checker PRISM. Cascading verification is illustrated with a prototype system that verifies the correctness of UAV mission plans. Research was funded by the European Office of Aerospace Research & Development (EOARD), a detachment of the Air Force Office of Scientific Research (AFOSR). I was supervised by Prof. David S. Rosenblum and Prof. Anthony Finkelstein, and I collaborated with Prof. Sebastian Elbaum.

My CV can be downloaded here.


Message Automation Ltd.
Warnford Court
29 Throgmorton Street
London EC2N 2AT
United Kingdom

Tel: +44 (0)20 7947 4111
Email: fokion.zervoudakis@messageautomation.com

DBLP: Fokion Zervoudakis
GitHub: fokionzervoudakis
LinkedIn: Fokion Zervoudakis
Twitter: @flawedgenesis


Software Systems Engineering