CISC/CMPE422, CISC835: Formal Methods in Software Engineering (Fall 2019)

Home page

[Home] [Content] [Schedule] [Readings] [Assignments] [Projects]

Instructor
Juergen Dingel, Goodwin Hall 723, dingel at cs dot queensu dot ca

Teaching Assistants
Anika Anwar
Karim Jahed
Lama Moukahal
Liam Walsh

Lecture Time and Location
Time: Mon 12:30pm, Wed 11:30am, and Thurs 1:30pm
Location: Stirling Hall B

Anika Anwar: Tue, 2:30 - 3:30pm in Goodwin Hall 636

Juergen Dingel: Mon, 2-3pm in Goodwin Hall 723

Karim Jahed: Wed, 2 - 3pm in Goodwin Hall 624

Lama Moukahal: Mon, 10 - 11am in Goodwin Hall 636

Liam Walsh: Thurs, 9:30 - 10:30am in Goodwin Hall 636

Audience
The course is most suitable for students interested in the theory and practice of software development.

Syllabus
The course syllabus with information on, e.g., learning outcomes, late policy, grading scheme and method, academic integrity, accommodations, and academic consideration for students in extenuating circumstances can be found here.

General Description
Modern software development inevitably requires the design and analysis of a number of different artifacts. Formal methods allow the mathematically precise formulation of some of these artifacts. For instance, formulas in predicate logic capture operational requirements, state machines describe the behaviour of code fragments and protocols, and object models capture static designs. The advantage of using these formal notations is that they typically improve the overall quality of the artifacts by removing ambiguities and imprecisions, and enabling automatic analyses that establish desirable properties or uncover undesirable properties. Consequently, the use of formal methods is indicated in domains in which the software has to meet very high quality standards and failure cannot be tolerated such as air-traffic control. Moreover, the abstraction and automation capabilities of some formal techniques present a powerful weapon against the ever-increasing complexity of software.

CISC422 is an introduction to the use of formal methods for the specification, design, and automatic analysis of software systems. The course will present a variety of specification notations (propositional and predicate logic, Z, Alloy, UML/OCL, temporal logic), and discuss corresponding analysis techniques (theorem proving, constraint solving, animation, model checking) using existing commercial and research tools (Jape, Alloy, USE, SMV). The course is most suited for students with a general background in computer science or electrical engineering and in interest in the theory and practise of software development.

Courseware package available at the bookstore.

There is no required text book. The recommended supplementary reading is:

M. Huth and M. Ryan. Logic in Computer Science: Modeling and reasoning about systems. Cambridge University Press. 2nd Edition. 2004.

Additional supporting material such as sample specifications used in class will be made available on the Readings page.

OnQ
The course will use OnQ for assignment submission and discussion forums. Students should monitor the course's OnQ pages, because important information, e.g., regarding assignments, might be communicated through them.

Prerequisites
CISC223 (and, by transitivity, CISC204)

Evaluation
Please see the course syllabus.