Modeling and Verification of Concurrent and Distributed Systems: From Reo to Mediator

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.