Software engineering requires rigorous testing to guarantee the product's quality. Semantic testing of functional correctness is challenged by nondeterminism in behavior, which makes testers difficult to write and reason about. This thesis presents a language-based technique for testing interactive systems. I propose a theory for specifying and validating nondeterministic behaviors, with guaranteed soundness and correctness. I then apply the theory to testing practices, and show how to derive specifications into interactive tester programs. I also introduce a language design for producing test inputs that can effectively detect and reproduce invalid behaviors. I evaluate the methodology by specifying and testing real-world systems such as web servers and file synchronizers, demonstrating the derived testers' ability to find disagreements between the specification and the implementation.
翻译:软件工程需要严格的测试来保证产品的质量。 功能正确性的语义测试受到行为不确定性的挑战, 这使得测试者难以写作和解释。 此论文为测试互动系统提供了一种基于语言的技术。 我提出了一个用于具体说明和验证非确定性行为的理论, 并有保证的正确性和正确性。 然后, 我将这一理论应用于测试实践, 并展示如何将规格引入互动测试程序。 我还引入了一种语言设计, 用于生成测试投入, 以有效检测和复制无效行为。 我通过指定和测试网络服务器和文件同步器等真实世界系统, 来评估方法, 演示导出测试者发现规格与执行之间存在的分歧的能力 。