1996-97 -- not offered|
Department of Computer Science
The course is split into three parts. The first part discusses a semiformal method, Jackson System Development (JSD) by Michael Jackson. JSD is used to build an understanding of what system development entails and to develop a basic method of constructing practical systems of interacting processes. JSD gives precise and useful guidelines for developing a system and is compatible with the object oriented paradigm. In particular, JSD is well suited to the following.
The second part of the course discusses the mathematical model CSP (Communicating Sequential Processes by C.A.R. Hoare). While CSP is not suitable to the actual design and development of a system of interacting processes, it can mathematically capture much of JSD. Consequently, it is possible to use formal methods in analyzing inter-process communication arising out of JSD designs.
The third part of the course discusses Z notation and its use in the specification of software systems. Z has been successfully used in many software companies -- such as IBM and Texas Instruments -- to specify and verify the correctness of real systems.
Prerequisites:general prerequisites, including COSC3311.03, and COSC3111.03 or COSC3321.03.