关于并发反应系统的依赖-保证推理：PiCore 框架、语言集成与应用

依赖-保证（rely-guarantee）方法是并发反应系统（CRSs，如并发操作系统、中断驱动控制系统与业务流程系统）组合验证的一种有前景的途径。然而，使用异构反应模式、不同抽象层次的规约，以及真实世界 CRSs 的复杂性，仍在挑战依赖-保证方法。本文提出 PiCore，一个用于 CRSs 形式化规约与验证的依赖-保证推理框架。我们设计了一种支持复杂反应结构的事件规约语言及其依赖-保证证明系统，以将 CRSs 反应方面的规约与逻辑从事件行为中分离。PiCore 通过依赖-保证接口对事件行为的语言及其依赖-保证系统进行参数化，并允许通过依赖-保证适配器轻松集成第三方语言。借助该设计，我们成功集成了两种现有语言及其依赖-保证证明系统，而无需对其规约与证明作任何改动。PiCore 已应用于两个真实案例研究，即 Zephyr RTOS 中并发内存管理的形式化验证，以及一种标准化业务流程执行语言（BPEL）到 PiCore 的已验证翻译。