Secured software development has become a critical aspect in modern software engineering. This course aims at introducing formal modeling and verification techniques to ensure the correctness of software design. It covers the following topics:
- Introduction to Formal Methods : Knowledge of the roles and techniques of formal specification and verification in software Engineering.
- The B formal Specification Language : Set theory and predicate logic - quantifiers, sets, relations, functions, sequences, B language constructs - States, invariant, operations and machine composition, etc.
- The Object Constraint Language (OCL) of UML : Formal syntax of the OCL language - context, invariant, pre-/post- conditions, types, navigation, etc. The use of the UML Specification Environment (USE) for validating OCL models.
- The Event based Modelling Language : Communicating Sequential Processes (CSP) : Formal semantics and syntax of the Communicating Sequential Processes (CSP) language – events, processes, concurrency and real-time constructs.
Associated modeling tools are used to support the practical applications of the formal verification and simulation. The students will be expected to apply different formal description notations in documenting and analyzing their software designs.