GATeL1扩展：面向状态机规范的测试生成与时钟约束设计

GATeL1是一种针对Lustre/Scade程序的强大测试环境，这些程序广泛应用于反应式系统和工业控制系统中，如DO-178B和IEC-61508标准所规定的认证过程。GATeL的核心功能是基于Constraint Logic Programming (CLP)的测试序列生成，能够自动创建复杂的测试用例，以验证程序的行为。 然而，原始的GATeL版本对于处理Scade中广泛应用的状态机描述存在局限性。Scade程序的特点是分解为多个模式，每个模式通过状态机来表示其高层逻辑。这些状态机之间的转换关系通常由特定的时钟驱动，形成一个多时钟层次结构。当前的GATeL版本仅能通过系统布尔编码来处理这种复杂性，但这种方法隐藏了时钟和状态转换的真实关系，导致效率低下。 为了克服这一挑战，本文提出了对GATeL进行两层扩展的方法。首先，作者定义了一套显式的时钟类型层次结构约束，允许GATeL更好地理解和管理不同时钟之间的关系，使得测试生成更加精确。这涉及到了多时钟表达式的编译，将状态机描述与GATeL的输入语言无缝对接。 其次，文章引入了状态机属性约束，这些约束是根据Scade编译过程中的模式构建模式来设计的。这有助于捕捉状态机的动态行为，包括状态的迁移条件、事件触发等，从而生成更符合实际运行环境的测试用例。 整个扩展工作是在ANR-07-TANG-019项目和IRSN核安全局的支持下完成的，它不仅提升了GATeL在复杂系统测试中的适用性，还展示了如何将工业级编程实践与理论上的CLP测试工具相结合，以提高测试覆盖率和有效性。 总结来说，这项研究扩展了GATeL的能力，使之能够更有效地处理状态机规范，从而在实际应用中发挥更大的作用，尤其是在那些需要精细时序控制和高级抽象的反应式系统领域。这不仅增强了GATeL作为测试生成工具的实用价值，也为其他类似工具的发展提供了新的思路和方法。