FORMAL METHODS FOR SYSTEM VERIFICATION

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 taken in two ways:
1. A written test with the possibility of an oral exam as an additional assessment if deemed necessary by the instructor or upon the student’s request. The written test consists of open questions on the course topics and exercises. The oral exam is conducted only if the written test is deemed sufficient. In case of a negative outcome in the oral exam, the written test must be retaken.
2. A project and an oral exam. The oral exam involves discussing the project and answering questions on the course material.

Description of the written test:
The written test aims to assess the student’s problem-solving skills, knowledge of fundamental concepts, and ability to solve exercises and prove theorems. It consists of open exercises covering the main topics of the course. The use of notes, books, or electronic devices is not allowed during the written test.
The written test may be followed by an oral exam, should the instructor deem it necessary or the student wish to improve the result. The oral exam includes a discussion of the written work, an evaluation of problem-solving abilities, and an assessment of theoretical knowledge and expressive skills. The oral exam is only conducted if the written test is deemed sufficient. In case of a negative outcome in the oral exam, the written test must be retaken.

If the student chooses option 2), the exam evaluation will take into account the quality of the project (30%), the quality of the report describing it (20%), and the student’s ability to explain the fundamental concepts of the discipline (50%).

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

This subject deals with topics related to the macro-area "Cities, infrastructure and social capital" and contributes to the achievement of one or more goals of U. N. Agenda for Sustainable Development