Asee peer logo

Formal Methods In The Undergraduate Software Engineering Curriculum

Download Paper |


2008 Annual Conference & Exposition


Pittsburgh, Pennsylvania

Publication Date

June 22, 2008

Start Date

June 22, 2008

End Date

June 25, 2008



Conference Session

Software Engineering Course Content

Tagged Division

Software Engineering Constituent Committee

Page Count


Page Numbers

13.619.1 - 13.619.11



Permanent URL

Download Count


Request a correction

Paper Authors


Mark Sebern Milwaukee School of Engineering

visit author page

MARK J. SEBERN is a Professor in the Electrical Engineering and Computer Science Department at the Milwaukee School of Engineering (MSOE), and was the founding program director for MSOE's undergraduate software engineering program. He has served as an ABET program evaluator for software engineering, computer engineering, and computer science.

visit author page


Henry Welch Milwaukee School of Engineering

visit author page

HENRY L. WELCH is a Professor of computer and software engineering in the Electrical Engineering and Computer Science Department at the Milwaukee School of Engineering. He teaches a broad range of course in both the computer and software engineering programs ranging from embedded systems to computer graphics, artificial intelligence, and formal methods.

visit author page

Download Paper |

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract

Formal Methods in the Undergraduate Software Engineering Curriculum Mark J. Sebern, PhD, PE Henry L. Welch, PhD Milwaukee School of Engineering Milwaukee School of Engineering Abstract An informal survey of undergraduate software engineering curricula indicates that many such programs incorporate a course in formal methods. Feedback from industry partners and advisory committees, however, seems to suggest that formal modeling, analysis, and verification techniques are not routinely employed in many software development organizations. Software engineering educators, especially those focused on preparing undergraduate students for practice in the discipline, encounter a number of issues when they take on the task of teaching and applying formal methods, including lack of appreciation by undergraduate students of the potential value and applicability of these techniques, and lack of realistic industry examples or of textbooks and curricular materials that address real-world software engineering practice. In addition, reliable, capable, and well supported tools are difficult to find; some of those that are available do not integrate well into contemporary software development processes. This paper describes the definition and evolution of one such formal methods course in an undergraduate software engineering curriculum. The discussion includes available notations and languages, tool support, integration of other program outcomes, student feedback, and instructor preparation. Audience participation and discussion are encouraged. Introduction The term “formal methods” is generally understood to mean “mathematically based languages, techniques, and tools for specifying and verifying [software] systems” [3]. These approaches often incorporate modeling (functional behavior, timing behavior, performance, or structure), model checking, and theorem proving. Formal methods topics are included in the SEEK body of knowledge presented in the SE2004 curriculum guidelines [12], along with an outline for a model course (SE313) on the use of formal methods in software engineering. Beyond the mathematical foundations, the curricular guidelines focus on modeling, specification, validation, notation, and tools. A survey of published curricula for the fifteen ABET-accredited software engineering programs (as of January 2008) indicates that at least six programs require a separate course in formal methods. Some other programs offer an elective course or other courses with some formal methods content. At the Milwaukee School of Engineering (MSOE), the undergraduate software engineering curriculum has included a junior-level course in formal methods (initially SE-381, later SE- 3811) that has run every academic year since its initial offering in the fall quarter of 2000. The focus of this course has been on the use of formal modeling and specification, notation and tool usage, and (to the extent possible) the application of formal methods to practical software development. The details of this experience are discussed in the sections that follow.

Proceedings of the 2008 American Society for Engineering Education Annual Conference & Exposition Copyright © 2008, American Society for Engineering Education

Sebern, M., & Welch, H. (2008, June), Formal Methods In The Undergraduate Software Engineering Curriculum Paper presented at 2008 Annual Conference & Exposition, Pittsburgh, Pennsylvania. 10.18260/1-2--3519

ASEE holds the copyright on this document. It may be read by the public free of charge. Authors may archive their work on personal websites or in institutional repositories with the following citation: © 2008 American Society for Engineering Education. Other scholars may excerpt or quote from these materials with the same citation. When excerpting or quoting from Conference Proceedings, authors should, in addition to noting the ASEE copyright, list all the original authors and their institutions and name the host city of the conference. - Last updated April 1, 2015