期刊文献+
共找到4篇文章
< 1 >
每页显示 20 50 100
基于带参系统Murphi模型的SMV自动建模
1
作者 段凯强 李勇坚 《计算机系统应用》 2016年第11期178-182,共5页
提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建模比较容易,而且得到的模型代码量比较少,易于阅读、理解和修改;而SMV模型则能实现更丰富的控制,如进行快... 提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建模比较容易,而且得到的模型代码量比较少,易于阅读、理解和修改;而SMV模型则能实现更丰富的控制,如进行快速不变式检查和限界模型检测等,但是建模过程复杂,模型不易维护.我们通过对两者进行分析,首先提出了能够很好描述带参系统的一个语义模型,然后读入相应的Murphi模型并进行分析以获取其语义模型表示,最后再通过一系列的策略自动得到限定参数时的SMV模型,由此得到的模型能够满足实际科研工作的应用要求. 展开更多
关键词 带参系统 模型检测 自动建模 形式验证
下载PDF
基于不变量查找的German协议验证 被引量:2
2
作者 曹燊 李勇坚 《计算机系统应用》 2015年第11期173-178,共6页
提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存... 提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质. 展开更多
关键词 缓存一致性协议 带参系统 不变量查找 多核处理器
下载PDF
ON THE PERFORMANCE OF ANALOG MULTIUSER DETECTION IN ULTRA-WIDEBAND TRANSMITTED-REFERENCE SYSTEM
3
作者 Ge Wei Zheng Lin Qiu Hongbing 《Journal of Electronics(China)》 2009年第6期798-803,共6页
The detection performance is evaluated for our proposed analog multiuser receiver in Ultra-WideBand (UWB) transmitted-reference system. In the presence of dense multipath and multi-access signals,the performance analy... The detection performance is evaluated for our proposed analog multiuser receiver in Ultra-WideBand (UWB) transmitted-reference system. In the presence of dense multipath and multi-access signals,the performance analysis is difficult due to the complicated waveform of received impulse. We develop an approach to analyze the steady-state Signal-to-Interference-plus-Noise (SINR) of the detector output. The multipath-spread impulse is fitted to an exponentially decaying profile in the analysis. A closed-form expression of steady-state SINR is further deduced for the proposed Least Minimum Square (LMS) detector. The analysis is validated by simulations in Line-Of-Sight (LOS) and Non-Line-Of-Sight (NLOS) channel respectively. Based on the theoretical results,the multipath delay spread is employed to determine the optimal width of the integration window of the detector. 展开更多
关键词 Multiuser detection Minimum Mean Square Error (MMSE) Transmitted reference Ultra-WideBand (UWB)
下载PDF
Effects of transmitter-related parameter settings on ranging accuracy for IR-UWB systems
4
作者 吴绍华 张钦宇 张乃通 《Journal of Harbin Institute of Technology(New Series)》 EI CAS 2010年第1期51-57,共7页
For impulse radio ultra-wideband (IR-UWB) ranging systems,effects of the settings of transmitter-related parameters, which include the pulse shape, the bandwidth and the pulse repetition interval (PRI), on ranging acc... For impulse radio ultra-wideband (IR-UWB) ranging systems,effects of the settings of transmitter-related parameters, which include the pulse shape, the bandwidth and the pulse repetition interval (PRI), on ranging accuracy were studied through theoretical analysis and simulations. Both the match-filtering based coherent TOA estimation algorithm and the energy-detection based non-coherent algorithm were used during simulations. Results show that the pulse shape has the least effect on the ranging accuracy. Increasing the pulse bandwidth can improve the ranging performance, but the performance is hardly improved any more when the bandwidth is increased beyond a certain level. PRI should be set long enough to guarantee the accurate ranging, because when PRI is shorter than the maximum excess delay of the channel, the ranging accuracy will be deteriorated by inter-pulse interference. 展开更多
关键词 IR-UWB ranging TOA estimation algorithm parameter setting match-filtering energy-detection
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部