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
Contribution of the course to the overall degree programme goals
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 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.
Expected learning outcomes
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.
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.
Pre-requirements
Basic knowledge of mathematics and probabilities.
Contents
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.
- The PEPA language: syntax and semantics.
- Stationary distribution.
- Methods of aggegation and equivalence relations.
- Product forms.
- Applications to performance analysis.
Referral texts
- 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.
- Papers supplied by the teacher.
Assessment methods
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.
- 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.
Teaching methods
Theoretical lessons and exercises performed in class.
Teaching language
English
Further information
Sustainability:
Course with sustainable contents
Lecture notes, material for reference available online or as e-book
Use of virtual forum
E-learning, moodle platforms
Course with sustainable contents
Lecture notes, material for reference available online or as e-book
Use of virtual forum
E-learning, moodle platforms
Type of exam
written
Definitive programme.
Last update of the programme: 20/03/2023