摘要:为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.

摘要:针对柔性制造系统的设计问题,提出了用Petri网精细化操作解决问题的方案.给出了两种精细化操作.研究了Petri网精细化操作的动态性质保持问题,给出了精细化操作保持活性、有界性、可回复性的充分必要条件;对一个柔性制造系统进行了设计和验证.其结果可为Petri网系统静态和动态性质的考察提供有效途径,为Petri网复杂大系统的分析提供重要手段,并特别适合于柔性制造系统的设计,具有一定的实用价值.

摘要:分析了描述逻辑ALNUI与ER模型的关系,特别是如何将ER模型转化为ALNUI的知识库,从而利用ALNUI的推理机制对ER模型进行自动推理的有效性,在此基础上,进一步研究了基于描述逻辑的模糊ER模型.针对模糊ER模型的特点和需求,在描述逻辑ALNUI的基础上,对描述逻辑ALNUI进行了模糊化推广,提出了一种新的描述逻辑,即模糊描述逻辑FALNUI.研究了基于FALNUI的模糊ER模型,即研究了如何将模糊ER模型转化为FALNUI的知识库,并利用FALNUI的推理机制研究了模糊ER模型的可满足性、冗余性和包含关系等自动推理问题,证明了这些推理问题的正确性.

摘要:J2EE(Java 2 platform enterprise edition)是构建分布式企业应用的基础中间件平台,当前的J2EE事务对资源的访问调度仍然是简单的先来先服务策略,导致服务器负载很重时,次要任务和关键任务争夺有限的资源,降低了关键任务的性能与成功率.为此,有必要识别任务类型,在资源不足时优先保证关键任务事务的执行.但提交给J2EE的事务基于交互方式执行,且缺乏必要的调度信息,因而不能简单地沿用已有的优先级驱动调度算法.提出一种新的事务调度算法TMPBP(threaded multi-queue priority-based protocol),该算法能够安全、有效地提高系统重负载情况下关键事务的服务质量,防止饥饿和优先级倒置.TMPBP包含了一种新的启发式优先级分派算法HRS(heuristic resource statistics),可以在调度信息缺乏的J2EE环境下动态识别关键事务.结果表明,通过合理地选择参数,TMPBP算法能够显著地提高关键事务的服务质量.

摘要:基于构件的软件复用是解决软件危机的重要手段,但目前还缺乏规范化的模式和方法以支持具有高复用性能的构件的识别与设计,借助特征空间作为工具以解决上述问题.首先介绍特征与特征空间的概念,从特征变化的相互依存关系入手,提出特征依赖的概念和4种具体的特征依赖.在此基础上,给出了基于特征空间的构件模型,使用特征的"型-值"机制与特征依赖表达构件的复用性.然后讨论了构件复用度的度量手段和规范化设计的目标,提出4种构件规范化模式(原子模式、基本模式、框架模式和内聚模式),研究了以特征空间分解为基础的规范化方法,并通过实例加以验证.该方法实现了多粒度、多模式构件的共存和构件间基于组合的松散耦合,从而提高了构件的复用效率并降低复用成本.结果在企业资源计划(enterprice resource planning,简称ERP)系统的构件化设计与开发中得到广泛应用,对指导构件设计具有较高的理论与实践价值.

摘要:在复杂的实时软件系统中使用构件式设计方法,已成为目前软件工程中的研究热点.如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一.通过在接口自动机模型中添加时间区间标记,来扩展其对实时系统接口行为的表达能力;使用实时接口自动机网络来描述实时软件系统的构件式设计模型;使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约,对系统设计阶段实时软件构件的动态行为进行形式化分析与检验.通过对实时接口自动机网络状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了验证算法,以检验构件式实时软件系统的设计与带时间约束的场景式规约之间的一致性.

摘要:为了提高企业过程结构优化的实用性、合理性以及计算机支持性,提出了基于有向超图和资源约束的优化方法.根据优化需求,通过对考虑了支持资源的过程进行不同的有向超图建模,利用有向超图的性质以及超图上所附加的过程语义,把过程结构优化转化为有向超图的切割和活动合并问题,并给出具体求解过程.求得的过程为一个结构和支持资源都优化的过程.最后,通过举例验证该方法可行、有效.

摘要:笔式用户界面软件以其自然、高效的交互方式,在很多领域中有着广泛的应用.笔式用户界面软件具有以交互为中心、用户个性化需求高的特点,由此也决定了用户在软件设计中的主导地位.以用户为中心的设计的关键问题在于,如何使用户的思想如实地反映到设计中.通过建立笔式用户界面软件特征模型PUIDM(thedomain model for pen-based user interface software),构造了一个连接用户与软件设计的平台.从上下文、软件实体、界面特征、体系结构等角度,对该模型的建立进行分析,并给出了相应的XML描述.在此基础上,描述了用户使用该模型进行软件设计的过程.实例表明,PUIDM能够正确引导用户进行设计,将用户意图充分地引入到软件设计和最终实现中,使软件满足可用性要求.

摘要:移动通信在人们的日常生活中发挥着越来越重要的作用,受到了越来越多的重视.人们希望能够在移动的时候获得与静态联网者相同的网络服务,这里最主要的就是要解决移动切换和无线网络带宽受限的问题.由于组播技术不仅能够提供很多新型的网络应用,而且能够高效地实现多点传送,并有效节省网络带宽,因此移动和组播的相互融合对两者的应用和发展都会带来较大的促进.提出了在移动环境中部署IP组播的框架体系,即基于快速组播切换的分层移动组播体系结构(fast multicast handoff based hierarchical mobile multicastarchitecture,简称FHMM).FHMM通过分层移动组播管理将节点在域内的移动对外屏蔽,提高了域间组播转发树主干的稳定性.FHMM还提出了快速组播切换机制,从而减少了切换延迟以及由此引发的分组丢失.另外,当节点移动到不支持组播的子网时,FHMM仍然可以为节点提供组播服务.模拟结果显示,FHMM具有分组丢失率低、组播分组传送效率高以及组播维护开销少等优点,是一种高效的移动组播解决方案.

摘要:信任是多方面的,在不同的应用场景中,同一节点在不同领域具有不同的可信度.现有信任模型粒度过于粗糙,不能很好地解决同一Peer节点在不同领域、不同方面的可信度计算问题.据此,提出一种新的Peer-to-Peef环境下的多粒度信任模型,并给出该模型的数值分析和分布式实现方法.分析及仿真结果表明,该模型与已有模型相比,在可信度计算的粒度、模型的安全性等方面有较大的提高.

摘要:目前绝大多数带宽测量方法都是基于网络瓶颈分隔原理的,在此基础上形成了基于包对/包队列的各种容量/可用带宽探测方法.但是,这类方法的测量结果不能超过源节点的最大发送速率,因此无法在高带宽环境中使用.另外,目前的可用带宽测量理论均没有考虑背景流的不同路由对测量方法所产生的影响.全面分析了背景流的路由对可用带宽测量的影响.在此基础上,基于蒙特卡洛(Monte Carlo)随机抽样的思想,提出了一种与现有测量方法截然不同的探测理论.该方法用随机发送单个小探测报文取代了目前的探测理论所依赖的包对/包队列,其测量范围不受源节点最大发送速率的限制.分析及实验表明,该方法不仅可以计算整条路径的可用带宽,也可以计算各段链路的容量和空闲率,进而分析得到各路由节点上的流量变化,以及各链路上对应的不同类型的背景流的分布.

摘要:在扩展网络或网络拓扑发生变化时,需要用最小的代价重新布置网络监测体系,以保证能收集到所有必需的网络信息.更新网络监测体系包括新增和重新配置收集节点两方面的代价,求解总代价最小的更新方案的问题是NP难的.提出了一种基于贪婪策略的近似算法,并分析了算法的时间复杂性和近似比.

摘要:在Internet日益孕育新技术和新应用的同时,交互主体间的生疏性以及共享资源的敏感性成为跨安全域信任建立的屏障.自动信任协商是通过协作主体间信任证、访问控制策略的交互披露,逐渐为各方建立信任关系的过程.系统介绍了这一崭新研究领域的理论研究和应用进展情况,并对信任协商中的协商模型、协商体系结构、访问控制策略规范、信任证描述及发现收集、协商策略及协商协议等多项关键技术的研究现状进行分析和点评,最后针对目前研究工作中存在的一些问题,对未来的研究方向及工作进行展望.通过对自动信任协商的研究及其进展的介绍,希望有助于在维护开放网络中主体自治性和隐私性的同时,研究更高效、实用的信任自动建立技术.

摘要:发布/订阅系统技术具有异步、松散耦合和多对多通信的特点,适应了目前动态多变的大规模分布式计算环境的需求,有着广阔的应用前景.分析了国内外发布/订阅系统的研究现状,并从拓扑结构、事件模型和订阅模型等不同角度进行了系统的分类,然后分别就其关键问题从匹配算法、基于内容的路由算法、形式化建模和服务质量等方面进行了阐述,并对已有的典型系统进行了分析比较,指出了当前该领域研究存在的问题和不足.同时,分析了在支持语义和近似匹配来增强系统智能性所面临的挑战,展望了发布/订阅系统在支持移动计算、P2P等新型计算环境下的研究趋势.

摘要:认证测试是一种新型的在Strand空间模型基础上发展而来的安全协议分析与辅助设计技术,可用于大部分协议的关联属性的分析;但是与Strand空间模型一样,它主要用于协议正确性证明,在协议为何不正确以及如何进行改进这个问题上处理分析能力较弱.在认证测试概念的基础上,结合逻辑分析的优点,提出了增强型认证测试EAT(enhanced authentication test)和Correspondence函数等概念来对安全协议进行关联属性的分析,很好地解决了这一问题与原有技术相比,该方法更为形式化,协议分析人员可以很方便地进行手动分析,并且更有利于协议分析自动化工具的实现.

摘要:数字作品的所有权证明允许在不泄漏任何秘密信息和防止所有者欺骗的前提下,对版权声明进行验证.提出一种基于Proactive可验证秘密共享和安全多方计算的数字作品所有权证明方案.在该方案中,可验证秘密共享,保证了所有权秘密的正确性,并防止对协议参与者的欺骗.通过Proactive安全提供自动恢复功能来保证协议生存周期内秘密的完整性和安全性.使用安全多方计算和同态承诺的零知识证明,实现了所有权验证.在不假设可信方存在的前提下,所提出方案能够在没有太多成员合谋的情况下,完成有效计算并发现不忠实成员.

摘要:GMPLS(generalized multiprotocol label SWitching)网络中的多约束QoS路由问题是要在诸如带宽、代价和延迟的约束条件下找到一条优化的路径.这个问题通常被认为是一个NP-完全问题.在研究共享风险链路组具有的启发信息的基础上,提出了一种具有共享风险链路启发信息的多约束预计算算法.该算法包含预计算和搜索两个部分.预计算主要是能创建和更新每个节点上的路由表.而后,搜索部分则可以在层次化的结构中选择满足约束条件的优化的路径.大量仿真数据表明,相应的方法能够取得满意的结果,可以有效地解决GMPLS网络中多约束的QoS路由问题.