University of Malta
 

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


CODE CPS5120

 
TITLE Runtime Verification

 
LEVEL 05 - Postgraduate Modular Diploma or Degree Course

 
ECTS CREDITS 5

 
DEPARTMENT Computer Science

 
DESCRIPTION This study-unit consists of six main parts:

1. Introduction - gives an overview of different verification techniques;
2. Runtime verification design space - outlines the main features of a runtime verification framework;
3. Instrumentation - this part focuses on the possible options for elicit events from a system for monitoring;
4. Architecture - there are various options of different monitoring architectures; these are treated in depth in this section;
5. Monitor compilation - the main advantage of runtime verification is that monitors are automatically compiled from formal specifications. This part presents a number of different logics and goes into detail regarding how these can be compiled;
6. Other issues - runtime verification is an active research area with various challenging aspects. A selection of these are treated in depth in this last section.

To assist the students in assimilating the advanced concepts presented in this unit, a number of tutorials are provided 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.

Study-unit Aims:

The main aims of the study-unit are to:
1. Expose students to real-life applications of formal methods, particularly the verification at runtime of complex software systems;
2. Enable students to understand a system’s requirements, formulate them in formal notation, and use mathematical techniques for generating executable monitors;
3. Give students a wide ranging set of skills which would better prepare them to approach real-life complex problems.

Learning Outcomes:

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

• Condense and express the main concepts underlying runtime verification;
• Characterise the differences, advantages and disadvantages of various runtime verification architectures;
• Appreciate a number of different compilation strategies to generate effective runtime monitors.

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

• Choose the appropriate formalisation logic for a given software system;
• Choose the appropriate instrumentation and compilation strategy for a given software system;
• Optimise and adapt runtime verification techniques for particular circumstances.

Main Text/s and any supplementary readings:

• P. O. Meredith, D. Jin, D. Gri th, F. Chen, and G. Rosu, “An overview of the MOP runtime verification framework,” JSTTT, vol. 14, no. 3, pp. 1433-2779, 2012
• E. Bodden, L. J. Hendren, P. Lam, O. Lhoták, and N. A. Naeem, “Collaborative runtime verification with tracematches,” J. Log. Comput., vol. 20, no. 3, pp. 707–723, 2010
• N. Delgado, A.Q. Gates, and Roach, S., "A taxonomy and catalog of runtime software-fault monitoring tools", IEEE Transactions on Software Engineering, vol. 30, no. 12, pp. 859-872, 2004
• C. Colombo, G. J. Pace, and G. Schneider, “Dynamic event-based runtime monitoring of real-time and contextual properties,” in FMICS, ser. LNCS, vol. 5596, 2008, pp. 135–149
• M. Leucker and C. Schallhart, “A brief account of runtime verification,” JLAP, vol. 78, no. 5, pp. 293–303, 2009
• Andreas Bauer, Martin Leucker, and Christian Schallhart. "Runtime verification for LTL and TLTL,"
Technical Report TUM-I0724, Institut fur Informatik, Technische Universitat Munchen, December 2007
• Marc Geilen, "On the Construction of Monitors for Temporal Logic Properties", Electr. Notes Theor. Comput. Sci., vol. 55, no. 2, pp. 181-199, 2001
• G. Rosu and K. Havelund, "Rewriting-Based Techniques for Runtime Verification", Automated Software Engg., vol. 12, no. 2, pp. 151-197, 2005

 
RULES/CONDITIONS Before TAKING THIS STUDY-UNIT YOU MUST TAKE CPS3225 OR TAKE CPS3233

 
STUDY-UNIT TYPE Lecture, Independent Study & Tutorial

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

 
LECTURER/S

 
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