Teaching Formal Methods in Application Domains

In this paper, we report on our experience of teaching formal methods as part of an introductory computer and network security module. This module is part of an applied undergraduate computer science degree. As a consequence, we neither can rely on strong theoretical or mathematical foundations of the students, nor can we focus the whole term on applying formal methods in security. We address these challenges by integrating formal methods into a three-week-long section on security protocols. In these three weeks, we use a holistic approach for teaching the security objectives of security protocols, their analysis of actual implementations using a network sniffer, their formal verification using a model checker (and comparing it to an approach based on interactive theorem proving). Our approach has been proven successful in teaching (both, in-person and remotely) the benefits of formal methods to numerous students. The students do perform well in the corresponding assessments, and each year we are able to attract students for final year projects (i.e., their B.Sc. thesis) in the area of formal methods.