Beijing-Saint Petersburg Mathematics Colloquium (online)
Abstract
In this talk I will introduce the channel-based coordination language Reo and the component-based modeling language Mediator, and show how to formalize and verify component-based concurrent and distributed system models in them. Reo provides a channel-based model which focuses on complex interactions among system components. Mediator supports a two-step hierarchical modeling approach: Automata, which provide an interface of ports, are the basic behavior units; Systems declare components or connectors through automata, and glue them together. With the help of Reo and Mediator, both components and systems can be modeled separately and precisely.
Bio
Meng Sun received his BSc and PhD degrees in applied mathematics from Peking University, in 1999 and 2005, respectively. He then spent one year as a postdoctoral researcher in National University of Singapore. From 2006 to 2010, he worked as a scientific staff member at CWI, the Netherlands. He has been a faculty member at Peking University since 2010 and became a full professor in 2017. Currently, his research interests mainly lie in software theory and formal methods. His recent work includes coordination models and languages, coalgebra theory, model checking, theorem proving, software testing, cyber-physical systems, service-oriented and cloud computing, modeling and verification of blockchain and smart contracts, big data analysis, theoretical foundations of machine learning, deep learning and their application in formal verification.
