报告题目：Behavioural Verification of Distributed Components
报告人： Eric Madelaine 教授 法国国家信息与自动化研究所
主持人： 刘静 教授
报告时间：10月29日 周一15:00-16:30
报告地点：理科大楼B1102
报告摘要：
Component models provide a structured programming paradigm, and ensure a very good re-usability of programs.the In our approach, we write only synchronisation vectors corresponding to the semantics of the ProActive library. Our specification language is more independent from the middleware, it allows us to express complex synchronisations that cannot happen in ProActive. This allows us to reason on efficient, expressive, and proved communication mechanisms. Overall, even if pNets formalism is approximately at the same level of abstraction as STS, in our approach, the programmer is rather exposed to a higher-level composition framework, closer to his/her usual programming and composition concerns. We are able to generate a finite behavioural model that can be model-checked to verify the correct behaviour of a GCM application.
报告人简介：
Dr. Eric Madelaine has an engineer diploma from Ecole Polytechnique de Paris, a PhD in computer science in 1983 from university of Paris 7, and an HdR from university of Nice Sophia-Antipolis in 2011. He is a researcher at INRIA since 1983, and he is currently member the Kairos research-team at INRIA Sophia-Antipolis. His research domains range from programming language semantics and process algebras, formal methods and model-checking, to specification and verification techniques for distributed applications. He has been member of 20+ program committees, and he is chair of the steering committee of the FACS symposium. He has been participating in many French and European projects, and he was PI in various bilateral projects, including Chile, Argentina, and China.
