• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学 ›› 2020, Vol. 42 ›› Issue (08): 1367-1373.

• 软件工程 • 上一篇    下一篇

Mediator的概率扩展

薛骁勇,孙猛   

  1. (北京大学数学科学学院,北京 100871)

  • 收稿日期:2020-01-02 修回日期:2020-04-07 接受日期:2020-08-25 出版日期:2020-08-25 发布日期:2020-08-29
  • 基金资助:
    国家自然科学基金(61772038,61532019);广东省重点领域研发计划(2018B010107004)

Probabilistic extension of Mediator

XUE Xiao-yong,SUN Meng   

  1. (School of Mathematical Sciences,Peking University,Beijing 100871,China)
  • Received:2020-01-02 Revised:2020-04-07 Accepted:2020-08-25 Online:2020-08-25 Published:2020-08-29

摘要: Mediator是一种基于组件的形式化建模语言,它提供了分层的模块化结构,从而可以方便地对复杂系统进行建模。它以自动机为其底层单位,自动机连接成的系统作为高级结构,能在对模型进行形式化描述的同时让其本身简单易用。为了使Mediator具有更强的表达能力,可对具有概率行为的系统进行形式化建模,对Mediator做了概率方面的扩展,并对扩展后的语言给出了基于马尔可夫决策过程的语义。同时还介绍了由Mediator模型自动生成PRISM代码的方法,能够使用PRISM工具对Mediator模型的相关性质进行验证。

关键词: Mediator, 概率扩展, 基于组件建模, 代码生成

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