Formal verification of concurrent systems

Prof. Antonella Santone
Dipartimento di Ingegneria, Università degli Studi del Sannio, Benevento

15 hours, 4 credits

June 20 - June 24, 2011

Dipartimento di Ingegneria dell'Informazione: Elettronica, Informatica, Telecomunicazioni, Largo Lucio Lazzarino, meeting room

Contacts: Prof. Gigliola Vaglini

Abstract

In industrial projects, verification of systems usually relies on techniques such as simulation and testing. Nevertheless, these techniques may prove inadequate, since such methods verify the correct behaviour of a system only on a sub-set of all possible computations. Therefore, an error of a system could be hidden just in one of those behaviours that has not been verified. These lectures aim to introduce some formal verification techniques that have gained great interest in recent years especially in those industrial sectors where it is important to guarantee the correctness of systems: production sectors of computer-controlled critical systems (avionic, space, railway, telecommunications, …).

Syllabus

• Specification language for concurrent systems
• Temporal logic to express properties
• Automated verification techniques
• Artificial intelligence techniques for improved formal verification
• Verification of Java multithreaded programs
• Automated formal verification tools