The primary role of the formal specification is to provide a precise and unambiguous description 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 modelling (1) object-oriented systems, (2) real-time distributed systems, and (3) concurrent reactive systems. The course will focus on the state-based notations Z/Object-Z, event-based notation CSP/Timed-CSP. Graphical modelling notations, such as StateChart and UML (Unified Modelling Language) will also be addressed.