Behavioural Verification of Distributed Components
Published：2018-10-28
Title: Behavioural Verification of Distributed Components
Time： 15:00-16:30, Octomber 29 Monday,2018
Location: Room 1102, Science BuildingB
Lecturer： Prof.Eric Madelaine INRIA
Abstract:
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.
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.
Biography:
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.
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.
