多媒体的随机模型检查

现代分布式系统包含一类应用程序，其中非功能性要求至关重要。特别是，这些应用程序包括多媒体设施，其中实时约束对于其正确功能至关重要。为了指定此类系统，有必要描述事件以概率分布给定的时间发生，随机自动机已成为一种指定和验证此类系统的有用技术。然而，随机描述非常通用，特别是它们允许使用一般概率分布函数，因此其验证可能比较复杂。过去几年，模型检查已成为大型系统的有用验证工具。本文我们描述两种用于随机自动机的模型检查算法。这些算法考虑如何检查以简单概率实时逻辑编写的属性。