报告题目：A Theory for the Composition of Concurrent Processes: Can we implement/automatize this methodology?

主持人：Eric Madelaine 教授

主持人：张敏 副教授

报告时间：5月24日（周三）13:30-14:30

报告地点：中北校区理科大楼B1002室

报告摘要：

We provide a theory for the operators composing concurrent processes. Open pNets (parameterized networks of synchronized automata) are new semantic objects that we propose for defining the semantics of composition operators. We define the operational semantics of open pNets, using “open transitions” that include symbolic hypotheses on the behavior of the pNets “holes”. We discuss when this semantics can be finite and how to compute it symbolically. We also define a bisimulation equivalence between open pNets, and shows its decidability. We have implemented a prototype algorithm for building the semantics of an Open pNet, and we are starting building a tool checking that a given relation between open automata is a bisimulation. Both the semantics (the state-generation algorithm) and the bisimulation algorithm contain a classical part based on finite-state automata, but also a SMT solver (here Z3), used to check satisfiability and inclusion of predicates over action expressions. We illustrate the approach on examples taken from various process languages, and propose a number of challenges as perspectives.

报告人简介：

Eric Madelaine is a senior researcher at INRIA in Sophia-Antipolis, France. He has a diploma from Ecole Polytechnique, Paris, a PhD thesis from University of Paris 7, and a Habilitation from University of Nice. His research interests range from semantics of programming languages, distributed and cloud computing, component-based software, formal methods, methods and tools for specification and verification of complex programs. He has served in many international conferences committees, including Euromicro, FESCA, SEAA, FMCO, and he is chair of the steering committee of the FACS symposium. He has been collaborating for several years now with the Software Engineering Institute at ECNU on formal techniques and theoretical models for distributed systems.