Module Specification

The information contained in this module specification was correct at the time of publication but may be subject to change, either during the session because of unforeseen circumstances, or following review of the module at the end of the session. Queries about the module should be directed to the member of staff with responsibility for the module.
1. Module Title Formal Methods
2. Module Code COMP313
3. Year Session 2023-24
4. Originating Department Computer Science
5. Faculty Fac of Science & Engineering
6. Semester Second Semester
7. CATS Level Level 6 FHEQ
8. CATS Value 15
9. Member of staff with responsibility for the module
Dr Q Tang Computer Science Qiyi.Tang@liverpool.ac.uk
10. Module Moderator
11. Other Contributing Departments  
12. Other Staff Teaching on this Module
Mrs J Birtall School of Electrical Engineering, Electronics and Computer Science Judith.Birtall@liverpool.ac.uk
13. Board of Studies
14. Mode of Delivery
15. Location Main Liverpool City Campus
    Lectures Seminars Tutorials Lab Practicals Fieldwork Placement Other TOTAL
16. Study Hours 30

          30
17.

Private Study

120
18.

TOTAL HOURS

150
 
    Lectures Seminars Tutorials Lab Practicals Fieldwork Placement Other
19. Timetable (if known)            
 
20. Pre-requisites before taking this module (other modules and/or general educational/academic requirements):

COMP109 Foundations of Computer Science; COMP111 Introduction to Artificial Intelligence
21. Modules for which this module is a pre-requisite:

 
22. Co-requisite modules:

 
23. Linked Modules:

 
24. Programme(s) (including Year of Study) to which this module is available on a mandatory basis:

25. Programme(s) (including Year of Study) to which this module is available on a required basis:

26. Programme(s) (including Year of Study) to which this module is available on an optional basis:

27. 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 w ithin 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.

 
28. Learning Outcomes
 

(LO1) Understand the principles of standard formal methods, such as Z;

 

(LO2) Understand the basic notions of temporal logic and its use in relation to reactive systems;

 

(LO3) Understand the use of model checking techniques in the verification of reactive systems;

 

(LO4) Be aware of some of the current research issues related to formal methods.

 
29. Teaching and Learning Strategies
 

Teaching Method 1 - Lecture
Description:

Standard on-campus delivery
Teaching Method 1 - Lecture
Description: Mix of on-campus/on-line synchronous/asynchronous sessions

 
30. Syllabus
   

1 1  State-Based Formal Methods (3.5 weeks): classical logic transformational systems traditional approaches; Z specification; formal development cycle case studies 2  Temporal Specification (3 weeks): reactive systems syntax and semantics of temporal logic; examples temporal specification of reactive systems (safety, liveness, fairness) 3  Model Checking (3.5 weeks): generating finite models;  analysis of a simple model checking algorithm symbolic model checking;  overview of reduction methods “on the fly”model checking; Spin and Promela case study and practical verification of properties; advanced topics

 
31. Recommended Texts
  Reading lists are managed at readinglists.liverpool.ac.uk. Click here to access the reading lists for this module.
 

Assessment

32. EXAM Duration Timing
(Semester)
% of
final
mark
Resit/resubmission
opportunity
Penalty for late
submission
Notes
  (313) Written exam Assessment Schedule (When) :2 150 100
33. CONTINUOUS Duration Timing
(Semester)
% of
final
mark
Resit/resubmission
opportunity
Penalty for late
submission
Notes