FORMAL METHODS FOR SYSTEM VERIFICATION

The course is one of the foundational educational activities of the study program: [CM90] Computer Science and Information Technology. The objective of the course is to provide the theoretical and logical-mathematical foundations for using formal modeling, analysis, and verification tools for both software and complex information systems. In particular, the course aims to introduce the main formal tools for specifying and analyzing the behavior of a system of interacting processes, with a particular focus on performance analysis. This knowledge is then used to introduce a specific stochastic calculus that enables the description and analysis of 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. More in detail:

1. Knowledge and understanding
● Knowledge of formal methods for software verification
● Knowledge of formal methods for performance analysis of concurrent and distributed systems
● Knowledge of the basics of dynamic system modeling

2. Ability to apply knowledge and understanding
● Ability to use formal tools for software analysis
● Ability to use methodologies for modeling complex systems
● Ability to apply basic knowledge to define a model for the analysis of a real information system

3. Judgment skills
● Ability to choose the most suitable methodology based on the system to be analyzed

4. Communication skills
● Ability to describe the reliability and performance requirements to be analyzed
● Ability to interact critically and respectfully with peers and the tutor, both in person and on the forum

5. Learning skills
● Ability to take notes and share them collaboratively on the online platform
● Ability to critically consult the reference texts and the bibliography contained within them

Basic knowledge of mathematics and probabilities. An understanding of written and spoken English is also required in order to comprehend the material provided by the instructor.

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%).

written

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

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