报告题目：BIP Architectures revisited: encoding and verification using parameterized networks of automata (pNets)
报 告 人：Eric Madelaine (INRIA Sophia Antipolis)
主 持 人：张敏 副教授
报告时间：2018年6月5日 周二 10:00-11:30
报告地点：中北校区理科大楼B1102

报告人简介：

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.

报告摘要：

BIP Architectures have been defined as a method to specify in a compositional way large BIP systems, proving properties of architecture patterns independently of their context, then deriving properties of composed systems from those of the small components. We show how we can extend BIP Architectures to handle "data-sensitive"

interactions, and preserve their compositionality properties.

Instead of developing from scratch a verification method for the extended architectures, we encode them into Open pNets (parameterized networks of synchronized automata),

and show how we can use open pNet tools to prove properties of the extended architectures.

We illustrate this approach on a use-case specifying a part of the onboard software of micro-satellites of ESA.