School of Computing


National University of Singapore

Overview of CS5232: Formal Specification and Design Techniques

Complex large software systems often have intricate system states and process control structures involving concurrency and real-time interactions. A major problem in developing such large software systems is to be able to initially characterise precisely what is to be built. Recently developed methods for tackling this problem are based on mathematics and logic (so-called formal specification, a critical part of formal methods). In essence a high-level mathematical model of the desired system is built. The aim is to try to construct the model of the system that is in the designer's mind; this has the dual benefits of forcing the designer to clarify their intentions & providing a communication medium between the interested parties.

The primary role of the formal specification is to provide a precise and unambiguous description of state, process and timing properties of a computer system. A formal specification allows the system designer to verify important properties and detect design error before system development begins. The objective of this course is to study various formal specification and design techniques for modeling The course will focus on the state-based notations Z/Object-Z, event-based notations CSP/Timed-CSP and their integrated notations. Note that both CSP and Z have been developed at Oxford University and the application of CSP won Oxford the First Queen's Award for Technological Achievement in 1990; and the application of Z won Oxford the Second Queen's Award in 1992 on the basis of the Oxford's long-term collaboration with IBM UK Ltd on the CICS transaction processing system (saved 5 million dollars, claimed by IBM).
Formal methods have been increasingly used in developing safety/security/mission critical systems. Even Microsoft has recently realised the importance of formal methods, For example, in 2002, Bill Gates pointed out Microsoft's use of formal methods, saying that, "For things like software verification, this has been the Holy Grail of computer science for many decades. But now, in some very key areas for example driver verification we're building tools that can do actual proofs of the software and how it works in order to guarantee the reliability. " .
The course is more research-oriented, but also suitable for coursework.

Pre-req: some basic knowledge in Discrete Mathematics (set and logic) is preferred. CS4211 (Advanced Software Engineering) is related but not required.

Lecturer: Dr. DONG Jin Song office: SoC1-4-18, ext:4353,

Year 2008 Lecture Time: Tue 1830-2030 Room: COM1/212
CA breakdown:
40% project (the deadline is on 30 April 2008 (before 5pm) to my office SoC1-4-18, hardcopies are preferred )
60% final exam (open book, 06 MAY 2008 Evening)

Project

The mathematical modeling techniques of this course are very general, expressive and applicable to many research fields. For example, by applying those techniques, you can add rigorous, precise and mathematical foundations to your Honours/Master/PhD thesis. In the 40% project, you are highly encouraged to choose a topic (application of formal specifications) which relates to your Honours/Master/PhD main research area or your current industry project (for course master students). If you think that your own research/work is not suitable for formal modeling techniques Object-Z/TCOZ, then you can choose the default project . Project reports requirements:

The project will be assessed for



Latex for Z/Object-Z/TCOZ

Download this zip file for latex examples and sty files for Z/Object-Z/TCOZ. Note that Object-Z guide file is very useful. P.S. no good Word format, but you can try our own new web tool:

XML Web tools support: Z family on the web with their UML photos

We applied the XML/XSL approach to the development of a web environment (can be used as an educational tool) for Z/Object-Z/TCOZ. the projection techniques and tools from Object-Z/TCOZ (in XML) to some UML (in XMI) diagrams are developed using XSL Transformations (XSLT). For more details, see ZML
Note that this (educational) tool can help you to understand: Some remarks about the display: Use IE5 for browsing, it supports XSL; For the display of mathematical symbols, please install Unicode font (Arial Unicode MS, also provided in the Office 2000/XP), after the installation make sure to set the Unicode font as your Web page font.

Course notes (ps version is more clear than pdf)

Part 1 & 2, Introduction/Background and Z/Schema Calculus,
(4 weeks lectures) available (postscript or pdf)
An exercise (test questions) on Z basics, available ( postscript or pdf)
One more exercise on sequence and Z schema is available (with solution pdf ),
Part 3, Object-Z, (3 weeks lectures) available ( postscript or pdf)
Part 4, Advanced Object Modeling Techniques (Class Union and Containment), (2 weeks lectures) available ( postscript or pdf)
Part 5, Real-Time Modeling Techniques, (1.5 weeks lectures) available ( postscript or pdf)
Additional Lecture on the new CSP Tool PAT pdf
Part 6, Integrated Formal Modeling Techniques, (2.5 weeks lectures) available ( postscript or pdf)

One slide per page versions can be found in this zip file

References (books and papers):

Books:

Papers: