重访时序规范理论 II：可实现性

在本文中，我们提出了一种假设 - 保证规范理论（即来自 [14] 的接口理论），用于具有关键时序约束的实时系统的模块化综合与验证。这是我们早期工作 [10] 的进一步进展，该工作为具备冻结时间能力的实时系统建立了一套优雅的代数规范理论。在本文中，我们放弃了这种（不可实现的）能力，转而针对不具备停止时间能力的更现实系统。我们的理论结合了进程代数与反应式综合风格，提供了用于系统集成的并行组合操作、用于观点融合与独立开发的逻辑合取/析取操作，以及用于增量综合的商操作。我们表明，一种替代性细化预序（它是 [10] 中预同余的粗化）构成了保持无不相容错误自由性的最弱预同余。这种粗化要求将我们理论的重点转向更具博弈论色彩的处理方式，其中该粗化构成了一种名为规范化的反应式综合博弈，并可通过一种新颖的局部自底向上传播算法高效实现。此前，时序并发博弈已在 [1,14,13] 中得到研究，其核心关注点之一是通过应用责任分配 [13] 来消除阻塞时间的策略。我们的时序博弈也存在可能通过规范组合而产生的阻塞时间策略问题。然而，由于我们对时序博弈采用了截然不同的表述形式，我们发现了一种无需责任分配的优雅解决方案。我们的解决方案利用了另一种称为实现化的反应式综合博弈，它与规范化对偶，并可通过对偶的局部自顶向下传播算法实现。