A Design-for-Verification Framework for a Configurable Performance-Critical Communication Interface
A Design-for-Verification Framework for a Configurable Performance-Critical Communication Interface
复制标题
用于可配置性能关键通信接口的验证设计框架
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
D. May
中科院分区：
文献类型：
--
作者：
S. Kharmeh;K. Eder;D. May
在本文中，我们提出了一个可配置的性能关键通信接口的验证框架的设计。为了管理问题的固有复杂性，我们将接口分解为独立的可参数化通信块。然后使用Tock-CSP对接口的时序和功能规范进行建模。FDR模型检查器及其tau优先级模型用于证明已配置接口的属性在目标通信协议的属性范围内。
In this paper we present a Design-for-Verification framework for a Configurable Performance-Critical Communication Interface. To manage the inherent complexity of the problem we decomposed the interface into independent parametrisable communication blocks. Tock-CSP was then used to model the timing and functional specifications of our interface. The FDR model checker and its tau-priority model were used to prove that the properties of the configured interface are within the properties of targeted communication protocols.