Dr. Axel Legay (2008 IBM Belgian Prize Winner) held positions at University of Liège and CMU (under the supervision of Ed Clarke). He is now full-time researcher at INRIA where he leads the ESTASE team (8 researchers), and a part-time Reader at the Royal Holloway University of London. His main research interests are in developing formal specification and verification techniques for Software Engineering. Axel Legay is a major contributor in the areas of CPS, embedded systems, and Systems of Systems. Axel Legay is a founder and major contributor of statistical model checking (a statistical variant of model checking effectively used in industry). He also provided the first generic techniques for the verification of infinite-state systems and for dealing with variability. Recently, he has introduced new theories to deal with quantitative problems and reason on energy-centric systems. Axel Legay supervised 3 PhD theses and authored more than 150 peer-reviewed publications. He is a referee for top journals and conferences in formal verification and simulation, and program co-chair of INFINITY'09, FIT'10, Runtime Verification 2013, Splat 2014, and FORMATS 2014. He is also workshop chair at ETAPS'14. He is principal investigator on 3 national and 5 European research projects.
In this short presentation we will first introduce the basic ingredients of Cyber-Physical Systems (CPS) and outline the main challenges and actions needed to make smart CPS happen. This includes new social aspects (adoption by humans), and new challenges in terms of safety/security/privacy. We will also insist on the green CPS challenge. In the second part of the presentation, we will present our vision on the rigorous design of CPS. This vision extends the one from Joseph Sifakis with new simulation-based techniques coupled with smart models and tools used to learn and anticipate systems dynamic. In conclusion, we will outline the main research priorities for the coming years.