并发反应式系统中基于事件的组合推理方法
An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems
摘要：
反应式系统由一组定义良好的输入事件组成，系统通过对每个事件执行关联的处理程序来对其进行反应。在并发环境中，事件处理程序可以与其他程序的执行交互，例如抢占式系统中的硬件中断，或多核架构中的反应式系统的其他实例。现有的基于可靠保证的验证框架只关注命令式程序，难以在可靠和保证关系中捕获与事件处理程序的可能无限序列的交互以及事件处理程序的输入参数。在本文中，我们提出了形式化的Isabelle/HOL的基于事件的可靠性保证方法的并发反应系统。我们开发了一个Pi-Core语言，它通过事件将并发命令和系统规约语言结合起来，我们为Pi-Core建立了一个可靠保证的证明系统，并证明了它的可靠性。我们的方法可以处理多核和可中断并发。我们使用两个案例研究来说明这一点：步进电机的可中断控制器和ARINC 653多核内核，并证明功能的正确性和Isabelle/HOL中的不变量的保存。
英文摘要：
Reactive systems are composed of a well defined set of input events that the system reacts with by executing an associated handler to each event. In concurrent environments, event handlers can interact with the execution of other programs such as hardware interruptions in preemptive systems, or other instances of the reactive system in multicore architectures. State of the art rely-guarantee based verification frameworks only focus on imperative programs, being difficult to capture in the rely and guarantee relations interactions with possible infinite sequences of event handlers, and the input arguments to event handlers. In this paper, we propose the formalisation in Isabelle/HOL of an event-based rely-guarantee approach for concurrent reactive systems. We develop a Pi-Core language which incorporates a concurrent imperative and system specification language by `events', and we build a rely-guarantee proof system for Pi-Core and prove its soundness. Our approach can deal with multicore and interruptible concurrency. We use two case studies to show this: an interruptible controller for stepper motors and an ARINC 653 multicore kernel, and prove the functional correctness and preservation of invariants of them in Isabelle/HOL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
