FORMAL METHODS FOR SYSTEM VERIFICATION

Academic year
2023/2024 Syllabus of previous years
Official course title
FORMAL METHODS FOR SYSTEM VERIFICATION
Course code
CM0474 (AF:451549 AR:245280)
Modality
On campus classes
ECTS credits
6
Degree level
Master's Degree Programme (DM270)
Educational sector code
INF/01
Period
1st Semester
Course year
1
Where
VENEZIA
Moodle
Go to Moodle page
The course aims to provide the theoretical basis for the use of formal modeling, analysis and verification tools for both software and complex systems.
The course presents the main formal tools for specifying and analyzing the behavior of a system of processes that interact with each other with particular attention to performance analysis.
In particular, a stochastic calculus will be introduced that allows one to describe and analyze the dynamic behavior of distributed and concurrent systems.
The student will acquire knowledge and skills on the fundamental aspects to consider in the design of software with reliability and performance requirements.
In particular, it will acquire knowledge on formal methods for the verification and evaluation of the performance of concurrent and distributed systems.
It will also be able to use formal tools and methodologies for modeling systems, as well as techniques for designing and analyzing software and systems that meet certain reliability and performance requirements.
Basic knowledge of mathematics and probabilities.
The stochastic process algebra, called PEPA (acronym of Performance Evaluation Process Algebra) will be introduced and some performance analysis techniques will be presented.
- The PEPA language: syntax and semantics.
- Stationary distribution.
- Methods of aggegation and equivalence relations.
- Product forms.
- Applications to performance analysis.
- J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996. http://www.dcs.ed.ac.uk/pepa/book.pdf
- Papers supplied by the teacher.
The exam can be done in two ways:
- carrying out a modeling and analysis project of a simple IT system and supporting an oral test on the project and on the course program in order to verify the student's skills and ability in applying the knowledge learned during the course
or
- carrying out a written exam consisting of exercises of modelling and analysis of simple computer systems in order to verify the skills and abilities of the student in applying the knowledge learned during the course.
Theoretical lessons and exercises performed in class.
English
Sustainability:

Course with sustainable contents
Lecture notes, material for reference available online or as e-book
Use of virtual forum
E-learning, moodle platforms
written
Definitive programme.
Last update of the programme: 20/03/2023