Abstract: Mediator is a component-based formal modeling language. With its hierarchical and modular structure, it can easily model complex systems. It takes automaton as its underlying unit. Automatons are connected to form a system, which is a high-level architecture and easy to use while formalizing the model. In order to make Mediator have stronger expressive ability and formally model the system with probabilistic behavior, Mediator is extended in terms of probability, and the semantics based on Markov decision process are given to the extended language. In addition, an automatic PRISM code generation method is introduced, which can use PRISM to verify the relevant properties of Mediator models.

Key words: Mediator, probabilistic extension, component-based modeling, code generation