The following course description is excerpted from the Graduate Course Catalog:
Advanced topics related to techniques, methods, procedures, and paradigms in software engineering. May be repeated for credit when topic varies.
The fundamental goal of this course is to raise the competence of software developers to create reliable software by improving the ability of students in precisely modeling, specifying, and reasoning about the correctness of computer programs. Considering the ubiquitousness of software and the frequency of software failures, the area of software correctness is an important part of the education of computer scientists and software engineers. However, there is a real concern with the lack of rigor and accountability in computer programming and software engineering, and the research agenda for software engineering states the need for strengthened mathematical foundation in the work force. The problem is not new, as shown by the following observation made in 1990 (Cherniavsky, J. C. Software failures attract congressional attention (Computing Research News, 2(1):4-5, January 1990).
[there is] a fundamental difference between software engineers and other engineers. Engineers are well trained in the mathematics necessary for good engineering. Software engineers are not trained in the disciplines necessary to assure high quality software. ... The problem is not so much not having the mathematics necessary to solve the software problem, but instead having the trained software engineers.
Parnas once said that "Professional engineers are expected to use discipline, science, and mathematics to assure that their products are reliable and robust. We should expect no less of anyone who produces programs professionally." This course will provide a small step toward realizing Parnas's by introducing formal methods---mathematically based techniques---and formal program verification---proving, mathematically, that a program agrees with its specification. It is essential for developers to employ these methods that offer high degree of assurance that the system's requirements are accurately capture the user's critical requirements and that an implementation in software is an accurate realization of the design. The specific topics to be covered in this course include:
- Concepts of formal methods
- Representative formal specification languages: OCL, Z, Larch, JML, and CSP.
- Application of formal methods
The prerequisite of CS 4390 is CS 2302 with a grade of C or better.
There is no required textbook. Tutorials, introductory articles and research papers, reference manuals, and various on-line documents will be used as course material (refer to the suggested readings at the Schedule page). Hard copies of required readings will be provided.
In this course we will study the concepts of formal methods and a few representative formal specification languages with the goal of acquiring the tools necessary for the comparisions and applictions of them. To this end, the specific learning outcomes include:
- Understand the concepts of formal methods.
- Know representative formal specification languages.
- Precisely model and specify small software systems using formal specification languages.
- Compare and evaluate different formal methods to choose a suitable one for a given application.
- Apply formal verification techniques to code with low complexity to reason about its correctness.
Last modified by Yoonsik Cheon: $Id: about-content.html,v 1.3 2016/08/19 05:36:45 cheon Exp $