pyspect：基于可达性分析自动构建时序逻辑树的可扩展工具箱

本文介绍了 pyspect，一个简化时序逻辑问题中可达性分析使用的 Python 工具箱。目前，针对网络安全关键性系统满足复杂要求需要显著的手动工作量和专业知识才能开发底层可达性程序。这种高开发工作量限制了可达性分析在复杂验证问题中的广泛采用。为此，pyspect 提供了一种与方法无关的做法，通过时序逻辑树（TLTs）来验证时序逻辑规范。它允许使用独立于特定可达性技术或集合表示形式的高级逻辑公式来指定复杂的安全和活性要求。作为结果，pyspect 允许对同一时序逻辑规范比较不同的可达性实现，如 Hamilton-Jacobi 和基于混合zonotope的可达性分析。这种设计将实现开发者（开发可达性的数值程序）与最终用户（编写规范）的关注点分开。通过一个简单的车辆示例，我们演示了 pyspect 如何简化可达性程序的合成，促进规范的可重用性，并促进对复杂任务的可达性技术进行 side-by-side 比较。