University of Malta
 

Study-Unit Description
UOM Main Page
 
 
 
Apply - Admissions 2016
Newspoint
Campus Map button
Facebook
Twitter


CODE CPS3233

 
TITLE Verification Techniques

 
LEVEL 03 - Years 2, 3, 4 in Modular Undergraduate Course

 
ECTS CREDITS 5

 
DEPARTMENT Computer Science

 
DESCRIPTION This study-unit consists of three main parts:

1. The first part deals with formally defining the semantics of a software system;
2. The second part focuses on different formalisms which can be used to specify properties of a software system. These can be loosely classified under:
   a) Finite-trace logics;
   b) Infinite-trace logics;
   c) Other logics.
3. After having covered a plethora of formalisms, the study-unit focuses on how these can be used to check the correctness of a software system. In this section we focus on three such techniques:
   a) Model-based testing;
   b) Runtime verification;
   c) Model checking.

To assist the students in assimilating the mathematical content, the unit is supported by a number of tutorials, and the attendance of the tutorials and lectures is obligatory. Students who fail to attend a session will be expected to perform extra work to prove sufficient understanding of the missed topic. Furthermore, given that the assessment is fully based on an assignment, students may be called in for an interview.

Study-unit Aims:

The main aims of the study-unit are to:
a) Introduce students to concepts of formal methods and their application to software verification;
b) Expose students to real-life applications of formal methods.

Learning Outcomes:

1. Knowledge & Understanding:
By the end of the study-unit the student will be able to:

a) Appreciate the differences, advantages and disadvantages of various verification techniques;
b) Reason with logical notations about the requirements of a software system;
c) Enable students to extract a system’s requirements and formulate them in formal notation;
d) Become aware of different software verification techniques and recognize suitable scenarios when to apply them.

2. Skills:
By the end of the study-unit the student will be able to:

a) Apply a number of software verification techniques to software systems;
b) Formalise the requirements of a software system using one of a number of specification formalisms;
c) Choose the appropriate formalisation logic for a given software system;
d) Choose the appropriate verification technique for a given software verification requirement.

Main Text/s and any supplementary readings:

a) Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, ISBN: 978-0262032704, M.I.T. Press, 1999
b) http://www.amazon.com/Practical-Model-Based-Testing-Tools-Approach/dp/0123725011

 
RULES/CONDITIONS Before TAKING THIS STUDY-UNIT YOU MUST TAKE CPS3222 OR TAKE CPS3230

 
ADDITIONAL NOTES Students taking this study-unit are assumed to have knowledge of the material covered in CPS2005.

 
STUDY-UNIT TYPE Lecture, Independent Study & Tutorial

 
METHOD OF ASSESSMENT
Assessment Component/s Resit Availability Weighting
Assignment Yes 100%

 
LECTURER/S Christian Colombo
Gordon J. Pace

 
The University makes every effort to ensure that the published Courses Plans, Programmes of Study and Study-Unit information are complete and up-to-date at the time of publication. The University reserves the right to make changes in case errors are detected after publication.
The availability of optional units may be subject to timetabling constraints.
Units not attracting a sufficient number of registrations may be withdrawn without notice.
It should be noted that all the information in the study-unit description above applies to the academic year 2017/8, if study-unit is available during this academic year, and may be subject to change in subsequent years.
Calendar
Notices
Study-unit Registration Forms 2017/8

Register

For Undergraduate (Day) and Postgraduate students.

 

Faculty of ICT Timetables

Timetables

ICT Timetables are available from Here.

Health and Safety Regulations for Laboratories Form

The Faculty of ICT Health and Safety Regulations for Laboratories form can be found here

 HealthAndSafety

13th Edition of EY’s Annual Attractiveness Event

 Logo

 

 

The 13th Edition of EY’s Annual Attractiveness event will be held on 25th October 2017 at the InterContinental Hotel,

St. Julians. It is titled "Thinking without the box: disruption, technology and FDI".

 

The  students' invitation and more information can be found here

The conference programme can be found here

 

 
 

Log In back to UoM Homepage