CISC422/CMPE422: Formal Methods in Software Engineering (Fall 2017)
Nicolas Hili, Goodwin Hall 734, hili at cs dot queensu dot ca
Karim Jahed, Goodwin Hall 624, jahed at cs dot queensu dot ca
Reza Ahmadi, Goodwin Hall 624, ahmadi at cs dot queensu dot ca
David Andrews, Goodwin Hall 621, dandrews at cs dot queensu dot ca
Time and place
Time: Mon 8:30-9:20, Tue 10:30-11:20, and Thu 9:30-10:20 in JEFFERY (Jeffery Hall) 126
The course is most suitable for students interested in the theory and practice of software development.
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.
CISC204 and CISC223