A comparative study of a tool-based approach for teaching formal specifications

The use of formal methods in software engineering has been shown to be an effective way to improving the dependability of developed systems. The difficulty of writing, reading, and understanding formal specifications, which is an essential component of formal verification, remains one of the main obstacles in the adoption of formal methods in industry. It is, thus, essential that undergraduate students in computing programs learn how to specify formal system properties. This paper outlines an instructive component that uses a tool to support the teaching of formal approaches and languages, and it presents educational outcomes from using such a component in undergraduate courses. The component uses a model checking-based tool LTLV to teach Linear Temporal Logic (LTL), a well-known specification language. In addition, this paper describes two experiments that compare the effectiveness of the new approach to that of the traditional lecture-based approach. The results of the experiments show promise that the tool-based approach can be effective in teaching formal specifications. The paper provides analysis of the results of the studies, as well as lessons learned from the experiments.