面向机器人与自治系统的合成安全监督器的完整测试

已验证控制器合成使用包含人类、机器人、其他设备以及待合成控制器的所有潜在行为的世界模型。世界模型支持定量风险评估,例如通过随机模型检查。此类模型描述了一系列控制器行为,其中某些行为——若被正确实现——可保证实际世界中的整体风险是可接受的,前提是随机假设已偏向安全侧。合成随后选择一个可接受风险的控制器行为。然而,由于跨越抽象、形式化方法与工具边界,机器人与自治系统的已验证合成必须伴随严格的测试。一般而言,安全关键系统的标准与法规要求在投入使用前将测试作为获得认证信用的关键要素。这篇进展中论文提出了一种对合成监督控制器的完整测试方法,这些控制器在人机协作与自动驾驶等领域强制实施安全性质。控制器代码由所选控制器行为生成。然而,代码生成器难以(若非不可行)以形式化且全面的方式验证。作为替代,利用测试生成一个抽象测试基准,即一个比代码语义更简单的符号有限状态机。从该基准导出完整测试套件,并应用于证明合成抽象测试基准与运行于控制系统平台上的生成具体控制器代码之间的观测等价性。