A Strategy and Tool Support to Motivate the Study of Formal Methods in Undergraduate Software Design and Modeling Courses

摘要

Proper design analysis is indispensable to assure quality and reduce emergent costs due to faulty software. Teaching proper design verification skills early during the pedagogical development of a software engineer is crucial, as such analysis is the only tractable way of resolving software problems early when they are easy to fix. The premise of the presented strategy is based on the observation that a fundamental component of any engineering discipline is the use of formal and sound techniques that facilitate analysis of produced artifacts. Yet, fundamental roadblocks exist in bringing the state of the art in formal design analysis to the undergraduate software engineering classroom due to the steep learning curve and quagmire of theoretical details involved in formal methods. This paper suggests a strategy and tool support to improve the attainment of software design verification skills. We illustrate how selective and pragmatic application of model-based verification methods can be used in software design education via tools that aim to bridge the gap between students' semi-formal design worldview and the formalism underlying formal methods.