Modeling and Verifying Concurrent Reactive Systems Using Separation Logic

Sun, Huan

doi:10.1007/978-981-95-4213-0_14

2026-01-01

PRE

DOI：10.1007/978-981-95-4213-0_14

原文链接

原文求助

摘要

En 中文

反应式系统依赖于一组定义明确的处理程序来持续响应环境刺激。在并发环境中，这些处理程序之间的交互引入了额外的复杂性，例如抢占式系统中的硬件中断和多核架构中的处理程序间通信。现有面向命令式语言的并发技术常在建模处理程序调用的潜在无界序列和精确捕获事件上下文方面面临挑战，而这两者对于有效推理并发反应式系统至关重要。本文提出ReCore，一个用于建模和验证并发反应式系统中共享资源的完全形式化框架。基于PiCore（一种能自然表示无界处理程序调用序列并精确跟踪事件上下文的基于事件的编程语言），我们开发了一种基于分离逻辑的推理框架，专门用于并发反应式系统的正确性验证。我们的ReCore框架使用Isabelle/HOL实现，并通过一个涉及Zephyr操作系统IPC模块中并发栈机制的非平凡案例研究进行验证，展示了其实用有效性。

Keyword:

EVENT

RELY/GUARANTEE

SPECIFICATIONS