Distributed Systems Testing

提出的研究重点是基于模型的测试框架，称为“假设-保证-推断”。与通常基于模型的测试一样，在框架中，起点是被测系统（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.