'Too Theoretical and Nowhere Near Interesting': Using a Tool to Increase Student Motivation for Formal Methods

Using formal methods to evaluate software and hardware enhances system reliability, which is crucial for safety-critical applications such as airplanes and autonomous vehicles. Formal methods are mathematical modeling techniques that can be used to verify the safety of systems. The use of formal methods is limited in industry due to a shortage of trained engineers. Educators in formal methods often report that many students do not see the benefit of formal methods and perceive the involved math as not worth the effort for their future careers as software engineers. This study aims to understand the current state of student beliefs and how using a formal verification tool affects student motivation to learn about formal methods. We used an Expectancy Value Cost Lite survey to measure student motivation. Students completed this survey multiple times while designing algorithms to control vehicles in different scenarios, both with and without a formal verification tool. We found that students in an autonomy class are motivated to use formal methods. Although the findings are not statistically significant, we observed a slight increase in motivation after using the tool. Additionally, using a formal verification tool solely for modeling may contribute to increased motivation. These results suggest that incorporating tools into coursework may be a useful step in motivating more students to study formal methods and enter the workforce with these skills.