Towards a test automation framework for alloy
Towards a test automation framework for alloy
复制标题
合金测试自动化框架
作者：
Allison Sullivan;Razieh Nokhbeh Zaeem;S. Khurshid;D. Marinov
编写软件设计的声明模型并分析它们以检测缺陷是开发更可靠的软件系统的有效方法。但是，正确编写这样的模型对于可能不精通宣言编程的从业者来说可能具有挑战性，他们的模型本身可能是越野车。我们介绍了一种新型的测试自动化框架AUNIT的基础，我们设想为使用合金编写的声明模型（一种由其SAT基于SAT的分析仪支持的一阶，关系语言）。我们从Xunit框架家族的成功中汲取灵感，这些框架在实践中被广泛用于测试自动化，尽管是针对或面向对象的程序。我们工作的主要新颖性是定义合金单元测试的基础，特别是定义测试案例和覆盖范围的概念，以及声明模型的覆盖标准。我们在不需要SAT解决方案的情况下将声明性测试执行和覆盖范围计算的问题减少到评估。我们的愿景是将开发人员与合金用户如何在合金中制定其模型，从而融合开发人员如何编写单元测试，从而促进新合金用户和专家的合金模型的开发和测试。我们使用一个小但复杂的合金模型来说明我们的想法。当我们专注于合金时，我们的思想将其推广到其他声明性语言（例如Z，B，ASM）。
Writing declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, AUnit, which we envision for testing declarative models written in Alloy -- a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of xUnit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and coverage, and coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM).