Compositional Verification of Timed Systems

Title:Compositional Verification of Timed Systems
Speaker:Prof. Wang Yi, Uppsala University
Time: 10:30am, Wednesday June 27
Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:
In this talk, I’ll present some technical results on verification of communicating timed systems with unbounded buffers, that are classical channel systems where the senders and receivers must follow given timing constraints. The main message is that channel systems are more difficult to verify due to the global synchronization on time. We show that several decidable problems in the untimed setting will be undecidable in the timed setting. This motivates our recent work on compositional verification using approximation techniques, covered in the second part of this talk in which I’ll present the CATS tool developed recently in Uppsala (CATS stands for Compositional Analysis of Timed Systems).