This Is AuburnElectronic Theses and Dissertations

Exploring the Integration of Model-based Formal Methods into Software Design Education




Wang, Shuo

Type of Degree



Computer Science and Software Engineering


Proper design analysis is indispensable to assure quality and reduce emergent cost due to faulty software. Teaching proper design verification skills early during the pedagogical development of a software engineer is crucial, as much analysis is the only tractable way of resolving software problems early when they are easy to fix. Besides, fundamental component of any engineering discipline, including software engineering, is the use of formal and sound techniques that facilitate analysis of artifacts produced by students. Yet, the impact of formal methods in software engineering practice, as well as education, is minuscule. The fundamental reasons why formal methods are not effectively utilized are attributed to (1) the impedance mismatch between the underlying mathematical underpinning of formal methods and students’ semi-formal, if not informal, view of the design problem and (2) the lack of tool support for seamless and transparent integration of formal methods into software design education. This thesis suggests a strategy and tool support to improvement attainment of software design verification skills. The strategy illustrates 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 world-view and the formalism underlying formal methods.