XML Schema特征提取算法

Twig模式最小化作为XML查询优化的一个重要方面,由于在进行最小化的过程中通常要利用XML Schema中的约束信息,因此被称为Schema特征。为了简化运用传统方法提取Schema特征的过程,以及确保提取过程的正确性,提出了一种自动提取Schema特征的模型检查算法。在Schema的形式模型的基础上,利用扩展的CTL公式表示Schema特征,提出算法以检查Schema模型是否满足要求的特征。由于扩展了CTL公式,所提算法不但可以检查孩子、子孙等前向的Schema特征,而且可以检查双亲、祖先等后向特征。最后,实现了支持该算法的模型检查器。

姿态估计算法在古建筑室内环境中的应用研究

摄像机姿态估计是影响三维注册成功与否的关键技术,目前在基于基本矩阵的估计中最流行的是八点算法,但八点算法针对平面场景出现明显的退化,因此在针对古建筑室内环境的注册应用中,为了扩大场景的适用范围,利用计算机视觉技术,对基于五点算法和八点算法的两种算法进行研究。以盒子结构为古建筑的室内环境结构进行模拟,结果表明,五点算法较八点算法恢复的三维模型有更高的精确性。

增强现实交互技术在历史博物馆中的应用

针对文物展示形式枯燥单一以及使用的标志物被遮挡部分信息时虚拟物体将消失的问题,以西安历史博物馆中秦兵马俑为例,利用增强现实(Augmented Reality,AR)交互技术中.Vuforia特征点检测匹配方法实现秦兵马俑交互系统的显示.分析标志物的选取原则,虚拟按键的设置、计算,利用相似比算法将虚拟按键由二维坐标转化为三维坐标,根据真实秦兵马俑坐标信息制作的幻影模型导入计算机,通过参观者的手指控制标志物上已设置好的虚拟按键,实现人与秦兵马俑幻影模型之间交互显示的效果.AR变互技术的应用不仅可以展示数字化的历史文物,而且使人机交互成为可能.

基于UPPAAL的WSNs数据收集协议的建模与分析

无线传感器网络(Wireless Sensor Networks,WSNs)广泛应用于各类数据收集系统,如居民区无线抄表(包括水表、电表和燃气表)系统。数据收集协议设计的正确性与合理性是影响网络正常运作的关键因素。针对数据收集协议的实时性需求,提出了基于UPPAAL实时模型检查器的WSNs数据收集协议的建模与分析方法。由于UPPAAL的输入模型相对于一般时间自动机模型而言较为复杂,因此首先对所选数据收集协议的通信行为建立一般时间自动机模型,之后再将其进一步转换为UPPAAL的输入模型。为了阐明该方法的有效性,选择了一个实际的无线抄表数据收集协议WM2RP作为例子进行建模,并利用UPPAAL分析其性质。分析结果显示,该协议能够满足一些与安全性及可靠性相关的性质。为了从多角度对协议进行分析,进一步建立了WM2RP协议的异常模型和能耗模型。

基于时间自动机模型的无线传感器网络数据收集协议测试用例生成

从协议测试的角度出发研究了基于时间自动机模型的无线传感器网络数据收集协议测试用例生成方法,提出利用UPPAAL工具对数据收集协议建立时间自动机模型,进而利用UPPAAL Co Ver工具生成满足特定覆盖标准的测试路径集合的方法。为了便于生成实际测试用例,开发了辅助自动测试用例生成工具ATCGT。通过一个工业界的无线抄表数据收集协议的建模与测试用例生成实例,阐明了该方法的有效性。

基于CBMC有界模型检测的无线抄表路由协议验证

针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法。WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证十分适用。CBMC能够直接对C/C++源码进行验证,这样不仅省去了传统模型检测技术需要对代码抽象建模的工作,而且不用担心模型和代码之间可能存在的不一致性问题。首先利用CBMC系统自生成断言验证技术,找到WM2RP协议实现中可能存在的漏洞,并对实现协议的公司给予反馈。然后进一步借助CBMC提供的用户自定义断言技术,通过自定义断言的插入以及对实现代码的适当处理,验证了WM2RP协议的网络层接收函数实现与协议规范的相符性。