COURSE TOPICS AND SYNOPSIS

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

“Foundations of Software Engineering”
Dr Jeff Sanders
United Nation University/Institute of Software Technology, Macao

Synopsis: The Object-Z notation is introduced and used as a vehicle to teach the specification of discrete systems. A discrete system is viewed as having states on which named operations are performed: as a so-called abstract machine. Z provides a way of describing both the state of the machine and its operations in a structured, modularised way that respects object orientation. In order to be successful, such a notation must apply across all levels of abstraction,from rather abstract specification to realistically detailed design. This Z does by incorporating nondeterminism in its descriptions and by facilitating designs over arbitrary (i.e. either abstract or concrete) data structures. Laws are given to verify that an implementation meets its specification; they can also be used in the stepwise derivation of an implementation from it specification. Together those techniques constitute the topic of system refinement, the last topic of this half of the course. An important feature of Z is that in using it to perform reasoning about systems, no modification is required to the laws of standard Mathematics.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

"Formal Methods and their Applications"
Dr Antonio Cerone
United Nation University/Institute of Software Technology, Macao

Synopsis: The course will start discussing the motivation and the importance of introducing formal methods in the design and verification of systems. It will present how to encorporate formal methods within software engineering methodologies, especially for those applications which are critical for safety and security. The course will then introduce 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 will illustrate how to use formal notations and automatic tools within the system design process.Finally, the course will investigate 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 will be illustrated through examples of increasing complexity from different application domains.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~