基于模AC的异步通信对象测试与验证方法探讨

本文主要探讨了基于模AC的异步通信对象模型测试与验证方法的研究，特别是在挪威奥斯陆大学计算机科学系进行的相关工作。作者Olaf Owe、Martin Steesen和Arild B. Thoresen针对异步环境中的软件可靠性问题，提出了一个黑盒测试的接口规范语言。这种语言以约束-承诺的风格描述对象的行为，特别适用于高级的克理奥尔（Creol）对象模型，这是一种面向对象建模的工具。 在传统的系统测试中，确保软件质量和可靠性至关重要。随着形式化方法和程序语言理论的应用，测试过程变得更严谨和系统化。近期，基于模型的测试策略逐渐受到重视，如在之前的论文中，研究人员提出了一种针对异步通信组件的规范测试方法，这种方法适用于开放环境下的非确定性交互。 本文的工作受到了欧盟项目Credo（分布式服务进化结构）和HATS（使用形式化方法的高度适应性和可信赖的软件）的资助，以及德国-挪威DAAD-NWO交换项目的Avabi（异步活动对象行为接口的自动验证）的支持。在这个背景下，作者利用Creol语言进行模型测试，通过同步执行规范与受测组件，实现观察等效性的测试目标。然而，由于异步通信的特性，测试案例可能导致状态空间显著增长，这增加了测试的复杂性。 为了解决这个问题，作者们利用了模AC（结合性和交换性）的概念，将其融入到重写逻辑系统Maude中，通过优化状态空间的处理。他们采用了广度优先搜索策略，有效地减少了状态空间的探索，从而提高了测试效率和实用性。当前的实验结果显示，这种方法在实际应用中展现出了良好的效果。 总结来说，本文的核心贡献是提供了一种有效的方法来处理异步通信对象模型的测试和验证，利用形式化手段，尤其是通过 Creol 和 Maude 的结合，简化了复杂性，提高了测试的准确性和效率。这对于保证软件在异步环境中的可靠性和质量具有重要的意义。