Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method
Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method
复制标题
DOI：
10.1007/s10009-009-0130-5
复制
发表时间：
2007-12
影响因子：
1.5
通讯作者：
Joris Rehm
中科院分区：
文献类型：
--
作者：
Joris Rehm
我们提出了一个IEEE 1394根竞争协议的模型，并证明了它的安全性。该模型具有实时特性，用Event-B方法的语言表示：一阶经典逻辑和集合论。通过使用Event-B方法及其证明器进行验证，我们还提供了一种对模型进行模型检验的方法。精化被用来在不同的抽象层次上描述所研究的系统：首先没有时间抽象地固定事件的调度，然后有越来越多的时间约束。
We present a model of the IEEE 1394 Root Contention Protocol with a proof of Safety. This model has real-time properties which are expressed in the language of the event-B method: first-order classical logic and set theory. Verification is done by proof using the event-B method and its prover, we also have a way to model-check models. Refinement is used to describe the studied system at different levels of abstraction: first without time to fix the scheduling of events abstractly, and then with more and more time constraints.