This course presents how to incorporate formal methods within software engineering methodologies, especially for those applications which are critical for safety and security. The course introduces some specific formal notations, such as the CSP process algebra and Temporal Logics, as well as automatic tools for system modeling and verification. Finally, the course investigates the use of formal methods in the analysis of safety and security properties of systems.

Course Objectives:

To teach formal methods within software engineering for safety and security. To describe the algorithms used within software engineering for safety and security and to improve ability to implement these algorithms. To form acquaintance with the applications of this research area. To improve the ability of written and oral presentation.

Recommended or Required Reading:

B. Bérard et al.. Systems and Software Verification, Model Checking Techniques and Tools, Springer-Verlag, 2001

Learning Outcomes:

1. Describe the fundamental concepts in formal methods within software engineering for safety and security

2. Identify state-of-the-art formal methods used in software engineering for safety and security

3. Construct programs that implement algorithms for safety and security of software systems

4. Prepare written and oral presentation for the performed work

Grading:

Midterm: 30%

Homework: 10%

Research Presentation: 30%

Final: 30%