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
object-oriented systems
interactive systems
real-time distributed systems
concurrent reactive systems
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.
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:
A single person project is preferred
(no more than two persons in one group project).
Project report is about 20 pages (single spaced 11/12pt).
here is an example
Report can be written in Latex (preferred, see guidelines below)
or XML (see guidelines below) or other formats (no guidelines).
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:
Z schema calculus (course notes part 2)
Object-Z inheritance (course notes part 3)
Relations between formal modeling techniques with UML (course notes part 6)
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:
R. Duke and G. Rose,
Formal Object Oriented Specification Using Object-Z .
Cornerstones of Computing Series (editors: R. Bird, C.A.R. Hoare),
Macmillan Press, March 2000. (main text book with many good examples,
can be found at the Science Library)
G. Smith, The Object-Z Specification Language
Kluwer Academic Publishers, 2000.
(a wonderful Object-Z reference manual, can be found at the
Science and CS Libraries)
J. Woodcock and J. Davies , Using Z: Specification, Refinement, and Proof. Prentice-Hall, 1996 (you can find everything about Z, a great book.
on line)
J.M. Spivey, The Z Notation: A Reference Manual. Prentice-Hall,
(2nd edition) 1992. (on line)
I. Hayes, Specification Case Studies. Prentice-Hall, (2nd edition) 1993.
S. Schneider. Concurrent and Real-time Systems: The CSP Approach, Wiley, 1999. (a wonderful book on both CSP and Timed CSP)
A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.
J. Davies, Specification and Proof in Real-Time CSP, Cambridge University Press, 1993. (an excellent phd thesis (on TCSP) which has won
the best UK phd thesis award)
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985. (the classical book on CSP.
on line)
Papers:
R. Duke, G. Rose and G. Smith. Object-Z: a Specification Language Advocated for the
Description of Standards . Computer Standards and Interfaces 17:511-533, 1995.
(ps)
J. Davies and S. Schneider. A Brief History of Timed CSP.
Theoretical Computer Science, vol 138, 1995.
(ps)
B. Mahony and J.S. Dong. Timed Communicating Object Z.
IEEE Transactions on Software Engineering, Feb 2000.
(pdf)
B. Mahony and J.S. Dong. Sensors and Actuators in TCOZ.
World Congress on Formal Methods (FM'99),
Lecture Notes in Computer Science, Vol 1709,
Springer-Verlag, Toulouse, France, Sep 1999. pdf
J.S. Dong and R. Duke. The Geometry of Object Containment. Object-Oriented
Systems (OOS) journal 2(1):41-63, Chapman Hall, 1995.
(ps)
default project . Project reports requirements: