Formal methods application: An empirical tale of software development

The development of an elevator scheduling system by undergraduate students is presented. The development was performed by 20 teams of undergraduate students, divided into two groups. One group produced specifications by employing a formal method that involves only first-order logic. The other group used no formal analysis. The solutions of the groups are compared using the metrics of code correctness, conciseness, and complexity. Particular attention is paid to a subset of the formal methods group which provided a full verification of their implementation. Their results are compared to other published formal solutions. The formal methods group's solutions are found to be far more correct than the nonformal solutions.