多媒体系统的随机模型检测
Stochastic Model Checking for Multimedia
摘要：
现代分布式系统包括一类非功能性需求很重要的应用程序。特别是，这些应用程序包括多媒体设施，实时约束是至关重要的，他们的正确运作。为了指定这样的系统，它是必要的，以描述事件发生的概率分布和随机自动机已成为一个有用的技术，通过它可以指定和验证这样的系统。然而，随机描述是非常一般的，特别是它们允许使用一般的概率分布函数，因此它们的验证可能是复杂的。在过去的几年里，模型检测已经成为一个有用的验证工具，大型系统。在本文中，我们描述了两个随机自动机的模型检测算法。这些算法考虑如何写在一个简单的概率实时逻辑的属性可以检查一个给定的随机自动机。
英文摘要：
Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions and stochastic automata have emerged as a useful technique by which such systems can be specified and verified. However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In the last few years, model checking has emerged as a useful verification tool for large systems. In this paper we describe two model checking algorithms for stochastic automata. These algorithms consider how properties written in a simple probabilistic real-time logic can be checked against a given stochastic automaton.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
