Module Catalogues, Xi'an Jiaotong-Liverpool University   
 
Module Code: CSE307
Module Title: Formal Methods
Module Level: Level 3
Module Credits: 5.00
Academic Year: 2017/18
Semester: SEM1
Originating Department: Computer Science and Software Engineering
Pre-requisites: N/A
   
Aims
As more complex computational systems are used within critical applications, it is becoming essential that these systems are formally specified.

Such specifications are used to give a precise and unambiguous description of the required system.

While this is clearly important in criticial systems such as industrial process management and air/spacecraft control, it is also becoming essential when applications involving E-commerce and mobile code are developed. In addition, as computational systems become more complex in general, formal specification can allow us to define the key characteristics of systems in a clear way and so help the development process.


Formal specifications provide the basis for verification of properties of systems. While there are a number of ways in which this can be achieved, the model-checking approach is a practical and popular way to verify the temporal properties of finite-state systems. Indeed, such temporal verification is widely used within the design of critical parts of integrated circuits, has recently been used to verify parts of the control mechanism for one of NASA's space probes, and is now beginning to be used to verify general Java programs.
Learning outcomes 
Upon completing this module, a student will:

1.understand the principles of standard formal methods, such as Z;

2.understand the basic notions of temporal logic and its use in relation to reactive systems;

3.understand the use of model checking techniques in the verification of reactive systems;

4.be aware of some of the current research issues related to formal methods
Method of teaching and learning 
Students will be expected to attend three hours of formal lectures in a typical week. Lectures will introduce students to the academic content. In addition, students will be expected to devote unsupervised time to private study. Two class tests during the semester will be used to assessed how well students keep up with the material presented in the lectures.
Syllabus 
1 State-Based Formal Methods (5 weeks):

classical logic

transformational systems

traditional approaches; Z specification; formal development cycle

case studies


2 Temporal Specification (4 weeks):

reactive systems

syntax and semantics of temporal logic; examples

temporal specification of reactive systems (safety, liveness, fairness)


3 Model Checking (5 weeks):

generating finite models; analysis of a simple model checking algorithm

generating finite models; analysis of a simple model checking algorithmon the fly"" model checking; Spin and Promela

case study and practical verification of properties; advanced topics
Delivery Hours  
Lectures Seminars Tutorials Lab/Prcaticals Fieldwork / Placement Other(Private study) Total
Hours/Semester 42     14      94  150 

Assessment

Sequence Method % of Final Mark
1 Written Examination 80.00
2 Assessment Task 10.00
3 Assessment Task 10.00

Module Catalogue generated from SITS CUT-OFF: 10/22/2017 9:24:07 PM