摘要:

摘要:针对嵌入式系统的特点,提出一种策略驱动的可靠嵌入式系统建模与分析方法.基于Petri 网建立嵌入式系统的形式化描述语言,并对设备、计算与物理交互、组件及通信过程等要素进行建模.分析嵌入式系统的主要故障类型和特征,探索嵌入式系统的可靠性保障策略.采用面向方面思想提取可靠性保障策略相关关注点.通过构造关注点模型,并利用编织机制,将关注点模型动态地集成为一个完整的嵌入式系统可靠模型.利用Petri 网相关理论分析嵌入式系统可靠性保障策略的有效性.具体实例表明,该方法能够简化嵌入式系统的设计与分析过程,有效地提高嵌入式系统的设计质量.

摘要:指针指向分析的主要目的是静态地获取程序在运行时刻的指针指向信息.基于Andersen 算法,设计了一种有效的、上下文敏感的指针指向分析算法,支持继承、字段对象等语言特性.不同对象的字段在算法中被分别处理,同时,算法对复合类型的对象实现了基于字段的处理.为了提高算法的效率和可扩展性,引入了两种优化方式:一种是结点间的拓扑排序以降低分析过程中的迭代次数;另一种是在线的环路侦测与消除,它与拓扑排序过程同步实现,有效地提高了处理效率.实验数据表明,该算法可以用来为较大规模的Java 代码生成精确的指向关系集合.

摘要:对Object-Z 形式规格说明构造测试用例的研究,目前主要集中在理论研究阶段,测试用例的自动生成几乎没有相应的工具支持.Object-Z 是基于数学和逻辑的语言,并大量使用了模式复合和简写形式,这给计算机提取完整语义用以自动产生测试用例造成了困难.通过展开Object-Z 规格说明中的模式定义,改进Object-Z 的文法结构,给出了提取Object-Z 规格说明语义的方法,研究了从Object-Z 规格说明产生测试用例的自动化过程.这一过程主要包含3 个阶段:Object-Z 语言的自动解析、语义自动抽取和测试用例自动产生.通过介绍的工具原型,可以很容易得到规格说明中的各种语义;基于某些测试准则,能够方便自动产生可视化的抽象测试用例.

摘要:为了将对称化简扩展到更多的非对称系统上,扩展了传统的基于自同构的对称性,提出了一种称为循环对称的新的对称性.证明了采用循环对称置换群或者由一组循环对称置换所生成的置换群仍可得到与原模型互模拟的对称商结构,从而达到化简系统规模的目的.进一步地,研究如何将对称化简应用于多值模型.多值模型可以有效地表示系统中的不确定信息,正越来越多地用于软件系统的建模与分析中.针对一种具体的多值模型——三值模型,定义传统的对称化简和循环对称化简在其上面的扩展.最后,分析三值模型的商结构与由约简得到的二值模型商结构之间的关系,证明了两种途径的等价性.

摘要:提出了一个场景驱动的服务行为调控途径.首先,用UML 顺序图模型作为场景规约以描述用户对服务行为的需求,并且基于目标服务的BPEL 行为规约,构造表示服务行为的BPEL-Petri 网模型(简称BPN 模型);其次,基于并发变迁分析BPN 模型上表示服务行为的路径,并通过遍历BPN 模型获取包含UML 顺序图描绘场景的服务行为集合;最后,根据行为分析的结果构建了调控服务,通过在运行时监听、检查并过滤用户与目标服务的消息交互,从目标服务中抽取或过滤顺序图描绘的场景.在此基础上,开发了原型工具BASIS,以支撑场景驱动的服务行为调控途径,并通过实例研究展示了该方法的可行性.

摘要:提出了时间Petri 网的混合语义模型,通过在变迁及其非冲突变迁集的最小上界处设置强制实施点,排除冲突变迁对变迁可实施性的影响,达到既能扩大模型调度范围又可保证任务调度时限性的目的,以解决现有语义模型在调度分析上的缺陷.进一步证明了混合语义模型的图灵等价性及标识可达性问题的不可判定性,然后界定了3 种语义模型的时间语言接受能力.最后提出了状态类分析方法,用于模型的可调度性分析和时间计算,并以一个柔性制造系统为例,比较和验证了3 种语义模型的调度分析能力.

摘要:针对目前.软件体系结构动态演化描述方法的不足,提出用约束超图表示软件体系结构,用左右应用条件刻画软件体系结构动态演化的前断言和后断言,用条件超图文法建模软件体系结构动态演化过程.通过案例分析,讨论了如何构建条件超图文法并应用于软件体系结构动态演化.在此基础上,建立软件体系结构动态演化的一致性条件定义,给出动态演化的一致性判定方法.最后,设计实验进行分析,验证了方法的有效性.

摘要:现有的形式化验证方法除了在模型层面对系统进行验证以外,越来越倾向于直接针对系统的实际代码和具体运行.运行时验证技术验证的对象是具体程序,它试图把形式化验证技术部署到程序的实际运行过程中.然而在把形式化技术部署到实际运行过程中会出现一系列在模型层面验证通常不会出现的问题,对这些问题中的冲突现象进行了研究,定义了运行时验证技术中存在的两种冲突,并给出了相应的检测算法.最后,对这些算法进行了实现和实例研究,结果表明了该方法的有用性.

摘要:分布式实时系统是广泛应用在众多关键领域的一类复杂实时系统.为保证其上运行任务的实时性,传统基于最坏响应时间的调度分析方法往往包含了实际系统运行过程中无法达到的最坏情况,因此在这些情况下的分析结果过于悲观.基于自动机理论的模型检测方法的好处在于能够穷尽地搜索整个系统状态空间,得到精确的分析结果.为了利用形式化方法的优势来精确分析分布式系统上任务的调度性,建立了分布式系统上的任务形式化模型,提出了行为自动机和环境自动机以分别描述任务的执行语义及其外部到达关系,把任务的调度性分析转换为对自动机网络位置的可达性进行分析,证明了在某些调度策略下的调度性的可判定性,并给出了满足调度可判定性调度策略的条件和范围.基于上述结论,实现了一个支持分布式系统任务实时调度分析工具SCT(schedulability checking tool),并与其他工具进行了分析精确度和性能的比较.比较结果显示,SCT 可以提供最为精确的分析结果,但同时也具有最长的分析时间.

摘要:主要针对AADL(architecture analysis and design language)嵌入式系统体系结构进行可靠性建模,实现AADL 可靠性模型到广义随机Petri 网(general stochastic Petri net,简称GSPN)可靠性计算模型的转换,并基于GSPN 可靠性计算模型对嵌入式系统进行可靠性评估.为了支持可靠性分析评估过程的自动化,根据模型转换的形式化方法,设计并实现了AADL 可靠性评估工具(AADL reliability assessment model tool,简称ARAM),该工具集成在AADL 体系结构设计工具OSATE(the open source AADL tool environment)中,并内置Petri 网计算工具PIPE2(platform independent Petri net editor 2),实现基于GSPN 模型的可靠性分析评估.同时,结合航空飞行控制系统的可靠性分析评估介绍了ARAM 工具的应用情况.

摘要:基于时间自动机理论,提出了时间窗、时间依赖服务代价以及时间依赖旅行时间这3 类时变网络中国邮路问题的统一建模的语义模型和求解方法.首先,将中国邮路问题可行解条件和时变参数与时间自动机联系起来,建立了3 类问题的统一时间自动机系统(timed automata system,简称TAS)模型;然后,将时变网络中国邮路问题归结为TAS 模型上的一系列可达性判定问题,并利用形式化验证算法给出了有效的求解方法.由于TAS 模型中存在O(|A|+|A_R|+1)个时间自动机,限制了问题求解规模.为此,通过扩展时间自动机语义,提出了TAS 模型中的时间自动机合并策略,进而将TAS 模型转换为一个广义时间自动机(GTA)模型.基于GTA 模型,利用UPPAAL 工具对9 组、共54 个随机算例进行实验.实验结果表明,该方法在求解精度上明显优于运筹学领域的方法.

摘要:P2P 流量的迅猛增长加剧了网络拥塞状况,P2P 流量识别为网络管理提供了基本的技术支持.首先介绍了P2P 流量的类别及流量识别面临的主要困难,然后综述了P2P 流量识别的主要技术及研究进展,最后给出下一步的主要研究方向.

摘要:由于属性基加密(attribute-based encryption,简称ABE)机制以属性为公钥,将密文和用户私钥与属性关联,能够灵活地表示访问控制策略,从而极大地降低了数据共享细粒度访问控制带来的网络带宽和发送结点的处理开销.因此,ABE 在细粒度访问控制领域具有广阔的应用前景.在对基本ABE 机制及其两种扩展:密钥-策略ABE(KP-ABE)和密文-策略ABE(CP-ABE)进行深入研究、分析后,针对ABE 中的CP-ABE 机制访问结构的设计、属性密钥撤销、ABE 的密钥滥用、多授权机构等难点问题进行了深入探讨和综合分析,对比了现有研究工作的功能及开销.最后讨论了ABE 未来需进一步研究的问题和主要研究方向.

摘要:无证书公钥密码体制(certificateless public key cryptography,简称CL-PKC)是在基于身份的公钥密码体制(identity-based public key cryptography,简称ID-PKC)的基础上提出来的一种新型公钥密码体制,没有密钥托管问题、不需要使用公钥证书,使得无证书公钥密码体制从其概念提出的初始就受到了学术界和工业界的极大关注.从2003 年至今,它一直是密码学和信息安全领域非常活跃的研究热点.其理论和技术在不断地丰富和发展.到目前为止,已经积累了大量的研究成果.将对这些成果进行较为系统的整理、分析、比较和简要的评述,并探讨该领域研究尚存在的不足及值得进一步研究的问题.

摘要:移动模型是Ad Hoc 网络区别于其他形式网络的重要标志,对其产生的动态网络特性(简称动态特性)进行评估,是研究Ad Hoc 网络的协议仿真和网络相关技术(如拓扑控制和网络性能测量等)的基础性问题.在已有研究的基础上,改进了网络的模型化描述,克服了以往模型无法很好地描述相关联的时空动态特性的缺陷,并在此基础上,提出了移动模型通用的可量化时空动态特性评估方法.通过构建节点空间位置分布,建立网络拓扑时空动态特性的分析模型,深入研究了几种移动模型的动态性.提出一种圆周曲线移动模型,弥补了以往移动模型难以描述现实的曲线移动场景.仿真实验结果表明,该方法能够有效地对现有移动模型的动态性进行评估.实验结果表明,圆周曲线移动模型与以往移动模型相比,具有良好的时空动态特性.

摘要:Paterson 等人在Waters 签名方案的基础上提出的基于身份的签名方案,虽然在标准模型下被证明能够归约于CDH 问题假定,但方案的计算效率不高.此后,李-姜等人对Paterson 方案虽然进行了改进,但方案的在线计算效率不高.在Paterson 方案的基础上,提出了一种在标准模型下更高效的基于身份的签名方案.该方案采用转变原方案中的群元素乘法运算为整数加法运算的方法来提高计算效率,而且利用预先计算双线性对的方法来改进方案的在线计算性能.与Paterson 方案相比，消除了多次乘法运算,减少了验证方的双线性对计算次数;与李-姜方案相比,减少了签名方和验证方的在线运算量以及系统输出参数;同时,该方案在标准模型下被证明具有在自适应选择消息攻击下存在不可伪造性,其安全性能够归约于CDH 问题假定.与现有的标准模型下基于身份的签名方案相比,该方案的计算效率更高.

摘要:旨在研究基于实时性约束的actor 节点优化部署策略.由于WSANs通常是随机播撒的,导致基于实时性约束的actor 节点优化部署问题是NP 难问题.因此,提出了基于Voronoi 图的最大实时覆盖部署策略,并通过实验,与现有针对区域覆盖的部署策略进行对比.该部署策略可以使WSANs 获得更好的实时性,且在收敛速度、能量消耗方面具有较好的性能.

摘要:为了解大规模P2P IPTV 系统中的用户行为特征和拓扑结构特征等内在信息,开发和部署了一个多协议P2P IPTV 爬行器TVCrawler,对3 个主流的P2P IPTV 系统——PPLive,PPStream 和UUSee 进行了大量的主动测量,并对P2P IPTV 系统中的用户行为和网络拓扑特征进行了分析和比较.主要发现包括:1) P2P IPTV 系统的频道在线人数中,有一半以上位于不可达的NAT 或者防火墙后面;2) 节点动态性的波动范围随频道人数的增加而增加,但是其取值范围具有幂律上限;3) 节点会话长度符合广延指数分布;4) PPLive 的入度分布属于具有指数截断的幂次分布,PPStream 的入度表现为某种分段幂律函数,UUSee 的入度接近威布尔分布;5) P2P IPTV 系统都是异配网络;6) P2P IPTV 系统都表现为小世界网络;7) PPLive 网络具有聚类特征,而PPStream 和UUSee 则不存在明显聚类特征;8) 3 个系统都表现出类似于无标度网络的鲁棒性特征,而与其他两个系统比较时,PPLive 具有更高的故障容错性和更明显的攻击脆弱性.这些测量研究和发现不仅有助于设计出更符合真实网络应用环境的系统或协议,也是实现对P2P IPTV 进行监测、引导、控制等方面的重要依据和基础.

摘要:研究异构传感环境下移动对象的反监控问题,提出一种暴露模型,该模型可用于近似估算移动对象穿越各向异性传感器网络时的风险.并在此基础上,结合各向异性Voronoi 图提出了一种路径判定算法,该算法能够保障移动对象选择一条具有近似最小风险的路径穿越各向异性传感器网络区域.理论分析和实验结果表明,算法具有良好的反监控性能.另外,算法只需知道移动对象侦测半径之内的局部信息,因此也具有分布式和实用性等良好特性.

摘要:网络漏洞分析是提高网络安全性的重要基础之一.以主机为中心的漏洞分析方法可在多项式时间内生成攻击图,但是没有考虑网络链路本身存在的不确定性.提出了一种基于不确定图的网络漏洞分析方法,采用链路不确定度以准确地描述网络链路状态,使得求解最佳利用链成为可能.在此基础上,提出了一种时间复杂度为O(n⁴)的不确定攻击图生成算法;基于不确定攻击图提出了一种时间复杂度为O(n³)的最佳利用链生成启发式算法.实验结果表明,该方法能在可接受的时间内生成不确定攻击图,找到一条攻击效益最佳的漏洞利用链.