This course starts discussing the motivation and the importance of
introducing formal methods in the design and verification of systems.
It presents how to incorporate formal methods within software engineering
methodologies, especially for those applications which are critical for safety
and security.

The course then introduces some specific formal notations, such as the CSP
process algebra and Temporal Logics, as well as automatic tools for system
modelling and verification. Practical examples illustrate how to use
formal notations and automatic tools within the system design process.

Finally, the course investigates the use of formal methods in the analysis
of safety and security properties of systems and on the relationship of those
properties with the system usability. This part of the course is illustrated
through examples of increasing complexity from different application domains.