Runtime verification is concerned with the analysis of software or hardware at execution time. It is based on extracting information from a running system and monitoring if the observed behaviors satisfy or violate the properties of interest. These techniques are critical for system correctness, reliability, security, and robustness. They are more practical than exhaustive formal verification and more versatile than conventional testing. During the last decade, many important tools and techniques have been developed and successfully employed in several application domains that go beyond the program verification: mixed-signal analysis, falsification analysis of cyber-physical and biological systems, signal processing and music detection. This course offers an introduction to both the theory and practice about monitoring techniques for software and hardware.
The course will start with an introduction on the areas where the verification should be preferable addressed at runtime. We will then discuss some techniques of software system instrumentation. We will then explore different specification languages to specify the properties to be monitored and the related available monitoring techniques.
Real case studies will expose students to the potential applications of these technologies. A final project will give them the possibility to make a concrete experience of the concepts taught. This is the list of the main topics of the course:
Monitoring techniques (state machines, rewriting logics, dynamic programming)
Monitoring software programs
Monitoring Mixed-Analog Signals
ECTS-Breakdown: 3 ECTS = 75 Hours
Not necessary
