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 is very related but not required.
Lecture Time: Mon 1830-2030 Room: LT19
CA breakdown:
40% project (presentation date 11 April. Report deadline is on 22 April (before 5pm) to SE lab (Com2-01-9))
60% final exam (open book, 29-Apr-2016 Morning)
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 or CSP-PAT, then you can choose the default project (details will be release in later Feb)
default projects . Project reports requirements:
A single person project is preferred
(no more than 4 persons in one group project).
Project report is about 20 pages (single spaced 11/12pt) with PAT code if the project is in PAT.
Part 1 & 2, Introduction/Background and Z/Schema Calculus,
(~4 weeks lectures)
pdf
An exercise (test questions) on Z basics,
pdf
One more exercise on sequence and Z schema is available
(with solution pdf),
Presentation slides on Z specification and introduction on Event-State based reasoning pdf,
(linking Part-2 with Part-3)
Part 3, Event Based Modeling Techniques and PAT, (~4 weeks lectures)
available ( csp1,
csp-pat-extra,
csp2,
csp3)
Some notes are based on the CSP-PAT tool.
Part 4, Object-Z, (~2 weeks lectures)
pdf
Part 5, Advanced Object Modeling Techniques,
(this is the extra reading on Object-Z advanced topics, not covered in 2016)
pdf
Part 6, Timed CSP and Integrated Formal Modeling Techniques, (~3 weeks lectures)
available pdf,
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. (Object-Z 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)
