Prof. Wang Yi

Title: Model-Based Desgin of Real-Time Systems:
from Timed Automata to Di-Graph and Back

Biography

Bio of Wang Yi: PhD in Computer Science, Chalmers Univ of Tech. 1991. Professor of Embedded Systems, Uppsala University, 2000. Distinguished Professor, North Eastern Univerisity, China, 2007. Fellow of IEEE. Member of Academy of Europe. Interests include Embedded Systems and Formal Verification. Receipent of CAV 2013 Award for the deveopment of UPPAAL, Best Paper Awards of RTSS17, RTSS15, RTSS09, ECRTS15, DATE13 and Outstanding Paper Award of ECRTS12. Board member of ACM SigBed and Award Committee Chair of ACM SigBed Caspi Dissertation Award. Steering Sommittee coChair of EMSOFT, SC member of ESWEEK, FORMATS, LCTES and SETTA. Editor for journals: ACM Transactions on Embedded Computing and Systems, IEEE Embedded Systems Letters, IEEE Design and Test, Journal of Computer Science and Technology. Recent keynotes include ETAPS15, SIES16, APSEC17 and ICFEM17.

Abstract

The first part of my lectures will focus on modeling and verification of real-time systems in the framework of timed automata, covering the theoretical foudation, modelling and specification languages as well as the central algorithms of UPPAAL, a tool developed jointly by Uppsala and Aalborg University. The second part of my lectures will be based on our recent work on real-time scheduling and timing analysis. I will present a new graph-based model for timed systems, that allows us to precisely capture the timing behavior of real-time software and yet keep the analysis problems tractable. For the theoretically intractable cases of interest, we present a refinement technique, which allows for effective guidance to significantly prune away the global search space and to efficiently verify the desired timing properties in real applications.