实时React系统中安全验证与合格测试的集成

在本文中，我们提出了一种可用于验证实时React系统中实现的方法。 与其他软件模型检查方法不同，我们的方法基于测试。 这种方法允许直接在真实代码上进行安全性验证，而不是从最终实现中提取模型。 验证这种模型是一项艰巨的工作，只能应用于实施的某些部分。 该方法是通过在实时系统中的安全验证和一致性测试之间建立连接来完成的。 我们首先证明一个定理，即在实时系统中，在启用输入的前提下，如果实现符合其规范并且该规范满足安全属性，则实现也满足该定理。 然后，基于前一个结论的对立性，我们提出了一个测试用例生成框架，该框架为生成可以用来检测实现中违反安全属性的测试用例奠定了基础。 此外，与其他实时测试生成方法相比，该测试生成框架还可以检测更多不合格缺陷。 该方法用火车门控制系统示出。