Testing Probabilistic and Stochastic Systems (ProbTest)

传统上，正式指定或建模系统的方法集中在系统功能行为的表示上。这样的模型可以用作测试被测系统（SUT）具有所需的行为集的基础：它的功能行为是正确的。它们是表示被测系统所需功能属性的有效方法，但不允许我们表示所需的非功能属性，如时间、概率或资源。为了处理这类性质，我们扩展了几种形式。新语言允许显式表示执行特定任务的概率，例如，如果使用系统的一个功能，它应该至少在99.9%的时间内提供预期的功能。它们还允许我们表达系统在执行任务时应该消耗的时间，要么是固定的时间，要么是用概率/随机术语定义的时间。例如，我们可能要求平均在1秒内产生一个结果。ProbTest将考虑包含概率和随机时间的模型。许多系统都有实时限制，因此包含时间是很重要的。在资源共享的情况下，概率是高度相关的，因此服务质量需求可能是概率性的。此外，由于在（可能不可靠的）介质上使用子系统通信，或者通过由多个线程或并行组件组成的系统进行通信，并且存在不同的可能同步序列，因此许多系统本质上是概率性的。还有许多通信协议（如蓝牙和以太网）具有概率要求，为了对基于状态的嵌入式系统进行推理，通常有必要使用概率。因此，存在具有概率和/或随机要求的系统，重要的是要有有效的、系统的方法来测试它们是否实际上满足这些要求。ProbTest是一个为期四年的项目，将支持布鲁内尔大学的Hierons和马德里康普顿斯大学的Nunez在这一领域的合作。

Traditionally, methods for formally specifying or modelling systems have concentrated on the representation of the functional behaviour of the systems. Such models can be used as the basis of testing that the system under test (SUT) has the required set of behaviours: its functional behaviour is correct. They are an effective way of representing the required functional properties of the system under test but do not allow us to express desired non-functional properties such as time, probabilities or resources. Several formalisms were extended in order to deal with these kind of properties. The new languages allow the explicit representation of the probability of performing a certain task, for example that if a function of the system is used it should provide the expected functionality at least 99.9% of the time. They also allow us to express the time that should be consumed by the system while performing tasks, either given by fixed amounts of time or defined in probabilistic/stochastic terms. For example, we may require that on average a result is produced within 1 second.ProbTest will consider models that include probabilities and stochastic time. Many systems have real-time constraints and thus the inclusion of time is important. Probabilities are highly relevant where resources are shared and so Quality of Service requirements can be probabilistic. In addition, many systems are probabilistic in nature due to either the use of subsystems communications over a (possibly unreliable) medium or through the system consisting of several threads or parallel components and there being different possible synchronization sequences. There are also a number of communications protocols, such as Bluetooth and Ethernet, that have probabilistic requirements and in order to reason about embedded systems, which are state-based, it is often necessary to use probabilities. Thus, there are systems with probabilistic and/or stochastic requirements and it is important to have efficient, systematic methods for testing whether they actually satisfy these requirements. ProbTest is a four year project that will support collaboration in this area between Hierons, of Brunel University, and Nunez, of Universidad Complutense de Madrid.