• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>12th International Conference on CONCUR 2001 - Concurrency Theory, 12th, Aug 20-25, 2001, Aalborg, Denmark >Performance Evaluation := (Process Algebra + Model Checking) X Markov Chains
【24h】

Performance Evaluation := (Process Algebra + Model Checking) X Markov Chains

机译：性能评估：=（过程代数+模型检查）X马尔可夫链

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (ⅰ) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ⅱ) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (ⅰ) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ⅱ) automated means to quantify these measures over CTMCs, and (ⅲ) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.
机译：马尔可夫链在实践中广泛用于确定系统性能和可靠性特征。绝大多数应用程序都考虑连续时间马尔可夫链（CTMC）。本教程文件展示了如何将并发理论中成功的模型规范和分析技术应用于性能评估。 CTMC的规范由随机过程代数支持，而这些模型的定量分析则通过模型检查来解决。过程代数提供：（ⅰ）以精确，模块化和面向约束的方式描述CTMC的高级规范形式，以及（ⅱ）自动生成和聚合CTMC的手段。时态逻辑模型检查提供了以下内容：（id）以清晰，紧凑和灵活的方式指定复杂的感兴趣的度量；（ⅱ）通过CTMC量化这些度量的自动化方法；以及（ⅲ）度量驱动的自动聚合（集总）。将过程代数与模型检查相结合，构成了基于CTMC的绩效评估的连贯框架。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号