Aims
The aims of this part of the course are:
- to introduce students to fundamental principles of state-based and object-oriented formal specifications in software development
- enable students to acquire skills necessary to develop logic-based specifications of software-based systems.
Upon completion of these 6 lecture hours the students will have acquired an in-depth knowledge of basic concepts of formal specifications, including state, operation and class schemas, and more generally the role that logical theories play in specifying (large) computer systems. Students will also develop a range of skills necessary for the definition of formal specifications from informal system requirements. These formal specifications will be written using conventional classical logic and some of the notation features of the Z specification language.
Prerequisites
This part of the course builds upon the 1st year logic course.
Books
- The Way of Z, by J. Jacky, Cambridge University Press, 1997.
A good book that explains well (see first three chapters) what formal specifications are for.
- Formal Specification Using Z, by L. Bottaci and J. Jones, International
Thomson Publishing, 1995.
A very simple and easy book. It is mainly suggested as a first reading to grasp the basic understanding of mathematical modeling and formal specification. Some of the examples might be useful in order to understand how to proceed in defining a formal specification of a computer system from some given user requirements.
- Z in Practice, by R. Barden, S. Stepney and D. Cooper, Prentice Hall, 1994.
- Safeware: System Safety and Computers, by N. Leveson, Addison-Wesley, 1995.
This book provides a nice collection of interesting real examples of computer-based system failures that could have been avoided if formal specifications had been used during the development cycle. It is listed here for your own general interest.
- Formal Methods on-line Publications here.
Lecture Notes
Tutorials
