Distributed Systems Testing

提出的研究重点是一个基于模型的测试框架，称为“假设-保证-推断”。与通常的基于模型的测试一样，在框架中，起点是被测系统(SUT)的预期行为的模型。然而，与现有的大多数方法不同的是，本研究的目标是考虑不一定完整和精确的模型。模型的不完备性隐含在关于被测系统的预期行为的知识的偏好性；而不精确性可能来自可选行为或对实际行为的过度抽象，这包括不可行的执行，并且通常是不确定的。然后，测试人员对手头的SUT中的实现错误的假设以某种故障模型的形式进行形式化。如果检测到故障，则测试执行结果可能导致测试者修改初始SUT模型或SUT本身。一旦纠正后的SUT通过了所有已执行的测试，后者可以帮助改进SUT的模型，即推断出更完整和更精确的模型。需要一个改进的模型，以便更好地记录被测试的系统，并在需要时生成额外的测试，以提高对系统质量的信心水平。这一步完成了假定-保证-推断测试框架。 拟议研究的意义在于，在假设-保证-推断测试框架的基础上，测试活动的自动化程度可以提高，并且正式的测试方法得到更广泛的接受，因为它们应用中的主要障碍是，允许不完整和不精确的模型可以显著降低完整和精确的SUT模型的可用性。

The proposed research focuses on a model-based testing framework, called "Assume-Guarantee-Infer". As usual for model-based testing, in the framework, the starting point is a model of the expected behaviour of a system under test (SUT). However, differently from the most of the existing approaches, the goal of this research is to consider models which are not necessarily complete and precise. Incompleteness of a model is implied by partiality of knowledge about the expected behaviour of a system under test; while impreciseness may come from optional behaviours or over-abstraction of the actual behaviour which includes infeasible executions and is usually nondeterministic. The tester assumptions about implementation faults in an SUT at hand are then formalized in the form of some fault model. Test execution results may lead the tester to modify either the initial SUT model or the SUT itself if faults are detected. Once the rectified SUT passes all the executed tests the latter can help refine the model of the SUT, i.e., infer a more complete and precise model. A refined model is needed to better document the tested system and to generate if required additional tests increasing the level of the confidence in the quality of the system. This step completes the Assume-Guarantee-Infer testing framework. The significance of the proposed research lies in an increased level of automation of testing activities which can be achieved based on the Assume-Guarantee-Infer testing framework and in a wider acceptance of formal approaches to testing, since the main hurdle in their application, the availability of a complete and precise SUT model can significantly be reduced by allowing incomplete and imprecise models.