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 additional oral exam if deemed necessary by the professor or upon student request. The written test consists of open-ended questions on the course topics and exercises. The oral exam is conducted only if the written test is passed. In case of failure in the oral exam, the written test must be retaken.
2) A project to be presented at the end of the lectures, followed by an oral exam. The oral exam includes a discussion of the project, solving exercises related to the project topic, and open-ended questions on the course subjects.

Description of the exam:
The exam, whether in the form of a written test or a project with oral exam, aims to assess the student's problem-solving skills, knowledge of the fundamental concepts, ability to solve exercises, and to prove theorems. It consists of exercises and open-ended questions covering the main topics addressed during the course.
The written test may be followed by an oral exam if considered appropriate by the professor or if the student wishes to improve the result. The oral exam is conducted only if the written test has been passed. In case of failure in the oral exam, the written test must be repeated.

written

The lecturer has a duty to ensure that the rules regarding the authenticity and originality of exam tests and papers are respected. Therefore, if there is suspicion of irregular conduct, an additional assessment may be conducted, which could differ from the original exam description.

The exam assessment will be structured as follows: quality of the submitted work (written exam or project): 30%, ability to explain the fundamental concepts of the discipline, both in written and oral form: 30%, ability to solve problems by applying the techniques presented during the course: 40%.

Theoretical lessons and exercises performed in class.

Sustainability:

Course with sustainable contents
Lecture notes, material for reference available online or as e-book
Use of virtual forum
E-learning, moodle platforms