一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

软件模型检测中的抽象模型研究综述

抽象是解决模型检测中状态爆炸问题的一个基本方法。对近年来软件模型检测研究中所提出的一系列抽象模型进行综述。首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分。然后根据模型的结构和功能特征,将抽象模型分为3类：1）传统的用于支持自上逼近或者自下逼近的布尔Kripke 结构;2）分别对应于3值和4值 Kripke 结构的 Kripke 模态迁移系统（Kripke modal transition systems ,KM TS）和混合迁移系统（mixed transition system ,MixTS）,可同时支持自上逼近和自下逼近的抽象;3）具有超迁移关系的广义 Kripke 模态迁移系统（generalized Kripke modal transition system ,GKM TS）和超迁移系统（hyper transition system ,HTS）,可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果。最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向。     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

基于MAS模型检测与抽象的Web服务验证

Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统( MAS)模型检测工具( MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。     

反例引导的模型检验工具的设计

针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.     

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题。针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法。根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型。利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例。实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题。     

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题.针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法.根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型.利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例.实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题.     

基于吴方法的符号模型检验

模型检验技术广泛应用于验证并发系统的性质。它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题。然而,随着系统规模的增大,BDD的大小仍呈指数增长。吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明。给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题。     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

一种针对CP-nets并发模型的验证方法

状态爆炸问题导致CP-nets并发模型的正确性验证工作十分困难。提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正。这在一定程度上避免了状态爆炸问题并实现了模型验证。通过将上述方法应用于HMIPv6协议模型,验证了其有效性。     

A minimum-energy path-preserving topology control algorithm for wireless sensor networks

The topology control strategies of wireless sensor networks are very important for reducing the energy consumption of sensor nodes and prolonging the life-span of networks. In this paper, we put forward a minimum-energy path-preserving topology control （MPTC） algorithm based on a concept of none k-redundant edges. MPTC not only resolves the problem of excessive energy consumption because of the unclosed region in small minimum-energy communication network （SMECN）, but also preserves at least one minimum-energy path between every pair of nodes in a wireless sensor network. We also propose an energy-efficient reconfiguration protocol that maintains the minimum-energy path property in the case where the network topology changes dynamically. Finally, we demonstrate the performance improvements of our algorithm through simulation.     

基于多传感器的室内三维定位算法研究

针对消防员在日常救援过程中难以准确获知自身位置坐标的问题,采用姿态传感器和气压计,提出一种室内三维定位算法(ITPA)。在ITPA算法中,根据加速度的幅值均方根、加速度的幅值方差和角速度的幅值均方根,实现过零监测,从而获知消防员的行走步数。根据气压计的数据,采用高度获取,卡尔曼滤波和异常数据处理等操作,获知消防员的高度,并判断其移动行为。通过二维移动距离计算和位置获取操作获知二维坐标。根据消防员的行为对其三维坐标观测值进行修正,并采用Kalman融合算法估计消防员的当前三维位置坐标。实验结果表明:在直行行走、楼梯行走和综合行走下,ITPA算法都能获得较接近真实路线的消防员室内三维位置,降低了算法的步数误差、距离误差和漂移误差,比FINS,IPNS和IPA3D算法更优。     

Efficient minimum spanning tree algorithms on the reconfigurable mesh

1 IntroductionLet G = (V, E) be a connected, undirected graph with a weight function W on the set Eof edges to the set of reals. A spanning tree is a subgraph T = (V, ET), ET G E, of C suchthat T is a tree. The weight W(T) of a spanning tree T is the sum of the weights of its edges.A spanning tree with the smallest possible'weight is called a minimum spanning tree (MST)of G. Computing an MST of a given weighted graph is an important problem that arisesin many applications. For this …     

基于频移干涉光纤腔衰荡技术的甲烷传感系统

煤矿事故严重威胁人们的生命和财产安全,瓦斯作为煤矿事故的罪魁祸首,其主要成分是甲烷。因此,选择一种性能优良并且能够实时探测甲烷浓度的气体传感器对安全生产和检测大气环境是十分有意义的。在众多气体传感器中,光纤气体传感器由于容量大、损耗小、体积小、抗腐蚀、抗干扰能力强等优势受到学者和仪器制造商的青睐。本文对比了几种光纤气体传感器,基于光谱吸收技术的光纤气体传感器体积小、成本低、功耗小,其使用最为广泛。在光谱吸收技术的基础上,发展了一种高灵敏度的探测技术,腔衰荡CRD(Cavity Ring-Down)技术。相比于普通的光谱吸收技术,其吸收光程长,灵敏度高出3个～4个数量级,并且对光源强度稳定性要求不高。但是,为了有效、实时地探测到衰荡信号,该技术对探测器的速度要求极高。本文研究的频移干涉腔衰荡FSI-CRD(Frequency-Shifted Interferometry Cavity Ring-Down)技术,通过将腔衰荡技术结合频移干涉技术,构建了频移干涉腔衰荡甲烷传感系统,实现了衰荡信号从时间域到频域的转换,降低了对探测设备的要求,并通过实验验证了该系统可以用于甲烷气体浓度的测量。     

Multiple-Morphs Adaptive Stream Architecture

In modern VLSI technology, hundreds of thousands of arithmetic units fit on a 1cm^2 chip. The challenge is supplying them with instructions and data. Stream architecture is able to solve the problem well. However, the applications suited for typical stream architecture are limited. This paper presents the definition of regular stream and irregular stream, and then describes MASA （Multiple-morphs Adaptive Stream Architecture） prototype system which supports different execution models according to applications＇ stream characteristics. This paper first discusses MASA architecture and stream model, and then explores the features and advantages of MASA through mapping stream applications to hardware. Finally MASA is evaluated by ten benchmarks. The result is encouraging.     

基于鸡群算法的无线传感器网络定位研究

针对无线传感器网络(WSN)节点定位精度不足的问题,提出一种改进鸡群算法与典型定位模型相结合的ICSO(Improve Chicken Swarm Optimization)算法。首先,提出基于pareto距离分级的分类算法,优化鸡群算法种群比例;然后,在母鸡位置公式中引入随机游走策略,增大搜索范围;最后,将净能量增益引入小鸡的位置公式,进一步提高定位精度。仿真结果表明,ICSO与改进后的粒子群算法(MPSO)和鸡群算法(BIDCSO)相比,在参考节点比例、节点密度、通信半径和定位区域面积等方面的平均定位精度分别提高了19.2%、22.1%、12.1%、8.5%和6%、10.5%、4.4%、4.7%。实验结果表明,ICSO算法能够有效提高定位精度。     

基于组合模型的时栅信号处理系统健康状况预测

为了保障时栅传感系统稳定性、提高测量精度,提出一种基于ELMAN神经网络和灰色模型组合预测的时栅信号处理系统健康状况预测方法。采用克朗巴哈系数法分析确定激励信号幅值、相位为预测参数。基于ELMAN神经网络及灰色模型,结合加权-比例-平均思想实现了组合模型建模。根据系统运行实际,以幅值和相位的相对误差为指标,制定健康诊断标准。实验结果表明,组合模型预测结果的相对误差、预测均方差和相对系数分别为0.101 6、0.011 9和0.988 5,预测误差小、相关性高。经健康诊断标准判定,健康状况预测结果与电路实际相符。该健康状况预测方法预测精度高,且明显高于单一模型,满足提前准确获悉电路系统健康状况的要求。     

水下CMUT动态性能仿真与测试的研究

目前CMUT以其频带宽、易集成阵列化、无需匹配层、灵敏度高等优点成为水下超声传感器在研究及应用推广方面的一个新热点。主要开展了对CMUT动态性能的仿真与测试。首先利用SIMULINK对CMUT发射和接收性能进行动态仿真分析,并建立实验平台,以仿真结果作为依据对CMUT动态性能进行了测试,同时实现了CMUT水下初步探测。本研究为CMUT的设计提供了有利的依据。     

基于节点速度和能量的MPR节点集选择

考虑到无人机群在协同完成任务时对时延的高要求,选用先验式路由协议OLSR(Optimized Link State Routing)协议。但无人机自组网中无人机节点高速移动和能量有限的特性,使得OLSR选举出来的MPR(Multi-Point Relay)节点可能会因此而丧失MPR资格,从而导致时延增加,网络开销增大。针对该问题,提出一种基于节点速度和能量的MPR集选择算法,运用HELLO分组在邻居探测的过程中感知节点能量和速度,之后在MPR选举前根据节点速度和能量对一跳邻居进行预处理,从而使速度快能量低的节点永不成为MPR节点。排除掉节点后,在节点意愿值相同的情况下再次对节点的速度和能量进行加权计算,选出最优MPR节点。仿真结果表明,基于节点速度和能量的MPR集选择算法在时延、吞吐量、节点能量消耗三个指标都具有良好的特性。