Mediator: A component-based modeling language for concurrent and distributed systems

摘要

In this paper we propose a new language Mediator to formalize component-based concurrent and distributed system models. 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 Mediator, components and systems can be modeled separately and precisely. The distributed Mediator and its semantics can be used to capture the inherent real-time and asynchronous behavior in distributed systems. Properties of Mediator models can be specified through CTL* formulae that support various families of properties such as safety and liveness, which can be verified using the nuXmv model checker. A leader election example is presented to show that this language is capable for modeling practical scenarios.