CISC422: Formal Methods in Software Engineering (Fall 2009)
Home page
[Home] [Content] [Schedule] [Readings] [Assignments] [Tools] [Messages]
|
CISC422: Formal Methods in Software Engineering (Fall 2009)
Home page[Home] [Content] [Schedule] [Readings] [Assignments] [Tools] [Messages] |
Instructor
Ernesto Posse,
Goodwin Hall 631, eposse at cs dot queensu dot ca
Time and place
Mondays 12:30-1:30, Wednesdays 11:30-12:30, and Thursdays 1:30-2:30.
Ellis Hall 321.
Audience
The course is most suitable for students
interested in the theory and practice of software
development.
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.
Indeed, in Model-Driven Development (MDD), a development methodology
advocated by, for instance, the OMG and IBM, formal models of the
software and its requirements form the primary artifacts from which
the code is automatically generated.
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 checking, animation, model checking) using existing commercial and research tools (Jape, Z/Eves, 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.
Material
Prerequisites
(CISC201/202 or 203/204) and CISC223 and CISC327
Evaluation
Last modified: Fri Aug 28 16:42:20 EDT 2009