报告题目： A Theory for the Composition of Concurrent Processes: Towards algorithms and tools

报告人：Eric Madelaine 教授

主持人：张敏

报告时间：2017年11月7日13:30—14:30

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

Abstract:

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 have implemented a prototype algorithm for building the semantics of an Open pNet. This state-generation algorithm contains 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. We show a new case study based on a BIP specification of the onboard software of nano-satellites.