论文部分内容阅读
模型检测由于其自动化程度高，是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器，首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理，并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型，并对实验结果进行分析。
基于SPIN的系统建模研究
【摘 要】
：
模型检测由于其自动化程度高，是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器，首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理，并采用SPIN模型检测
【机 构】
：
北京航空航天大学计算机学院
【出 处】
：
计算机与现代化
【发表日期】
：
2012年9期
其他文献
在对激光的能量分布分析前需要提取光斑的有效区域。激光远距离传输后,在大气作用下,光斑会发生变形和弥散现象,造成光斑的质心和几何中心不重合。利用Cany边缘检测技术,先确定光斑的边界,再通过Hough变换算法进行圆检测,可以提取出近场完整光斑和远场弥散光斑的有效区域。对实际光斑的定位计算验证检测技术的有效性。
利用全相位方向滤波器组良好的多方向性和平移不变性的特征,提出一种基于小波-全相位方向滤波器组变换的多聚焦图像融合方法。对不同聚焦图像进行小波-全相位方向滤波器组变换,采用加权平均算子对低频系数进行融合,采用局部方差准则对各个方向上的高频系数进行融合,对融合后的系数进行重构,得到高低频比例升高的融合图像。实验结果表明,与其它多聚焦图像融合算法相比,该方法显著减少均方根误差的值,提高峰值信噪比的值,使
提出一种改进的适用于机房教学的屏幕共享方案。该方案采用C/S模式。服务器端定时抓取屏幕图像和鼠标图标,形成位图数据流,利用GDI+压缩为JPEG文件,然后采用套接字广播图像数据。客户端接收图像数据后在本机显示,从而实现了屏幕共享。实验结果表明,在客户端重现的服务器屏幕画面,清晰流畅,能与服务器保持实时同步,满足了局域网环境下多媒体教学的实际需要。
RSS订阅服务让浏览者不用再花费大量的时间去浏览互联网上的海量信息,RSS订阅的提供者会收集和组织浏览者所定制的新闻,按照希望的格式直接传送到浏览者的计算机。本文分析RS
针对在传输语音秘密信息过程中存在破坏或窃取的问题,提出一种鲁棒性较强的信息隐藏方法。把一段语言作为秘密信息隐藏到宿主音频中,在公共信道中传递秘密信息。该算法是根据
利用Word、Excel和PowerPoint对象模型,结合数据库理论,研究和提出Office办公软件改卷的技术方案,包括出题系统数据库的设计、Office组件的对象和属性、改卷系统实现的方法。
在介绍SR23温控仪的通信协议的基础上,详细叙述在C#.NET环境下利用SerialPort类实现SR23温控仪与PC机间的数据通信的原理与方法。通过串口通讯实现多点温度的远程监控与记录,
提出基于短时能量和过零率的简化语音信号双门限端点检测算法，搭建Matlab的算法仿真平台，实验结果表明，基于短时能量和过零率的双门限端点检测算法在保证检测率的前提下，运算复杂
大豆国家新标准(GB 1352-2009)于2009年9月1日起正式实施,新标准首次增加对热损伤粒的要求。基于此,本文在分析大豆表面颜色特征的基础上,提出利用神经网络和大豆表面颜色特征对大豆进行标准粒和热损伤粒分类的方法。文中选取大豆图像的6种颜色特征值作为神经网络的训练样本,并尝试利用粒子群优化算法与BP(Back Propagation)结合算法训练网络。仿真结果表明,本文提出的方法取得一定的
根据医院实际情况，设计一种基于智能一卡通的医院内部管理系统，将门禁系统、餐饮消费系统和图书管理系统整合，有效地提高医院的管理效率和管理水平。