摘要:诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量.相应的算法已经实现并用实例作了分析测试.实验结果表明该方法是有效的.

摘要:澄清了各类量子自动机之间的相互关系,并给出了量子自动机的各种等价刻画定理.引入G-量子自动机、g-量子自动机、(广义)量子自动机及G-量子文法和g-量子文法,并阐明了它们与其他量子自动机之间的等价关系.在一定条件下讨论了G(g)-量子自动机与G(g)-量子文法的等价性,从而解决了关于量子文法产生量子正规语言的问题.讨论了量子语言与正规语言的关系,特别是回答了Gudder提出的两个公开问题.最后,给出了一种减少状态空间维数的方法.

摘要:Action演算簇(action calculi)作为描述不同并发交互行为的数学框架,可以表示一大类具有某些相同特性的并发形式化模型.试图把(演算(一种基于约束的高阶并发计算模)也包含在action演算簇的框架下.首先定义了一个具体的action演算AC(K_γ),然后给出了从(演算到AC(K_γ)转换的形式描述,最后在定义AC(K_γ)的可观察性、弱互模拟关系和弱等价关系的基础上,以(演算为中间表示,证明了这种转换保持了(演算的弱行为等价性.研究表明,action演算簇可以表示基于约束的并发模型,从而充分说明了action演算簇的描述能力,并且为在action演算簇框架下把(演算与其他并发模型结合并进行比较提供了前提.

摘要:初步建立了基于量子逻辑的自动机和文法理论的基本框架.引入了量子文法(称为l值文法),特别是证明了任意l值正规文法生成的语言(称为量子语言)等价于某种基于量子逻辑且含动作(的自动机(称为l值自动机)识别的语言,反之,任意l值自动机识别的语言等价于某l值正规文法生成的语言.建立了l值泵引理,并得到量子语言的判定性刻画.最后简要讨论了正规文法与量子文法(即l值正规文法)的关系.因此,为进一步研究更复杂的量子自动机(如量子下推自动机和Turing机)和量子文法(如量子上下文无关文法和上下文有关文法)奠定了基础.

摘要:在数字图书馆和数据仓库中,需要解决海量数据的排序问题.利用蛇型磁带自身的物理特点,实现了一种高效的磁带排序算法STESort(serpentine tape external sort).与传统的2路归并磁带排序算法相比,STESort算法减少了磁带总定位时间.STESort算法具有更优的效率.STESort算法在提高排序效率的同时,通过减少磁头在磁带表面的移动次数延长了磁带的使用寿命.理论分析和实验结果表明,STESort算法优于传统的磁带排序算法,适合于海量数据排序.

摘要:TSP(traveling salesman problem)问题是最经典的NP-hard组合优化问题之一.长期以来,人们一直在寻求快速、高效的近似算法,以便在合理的计算时间内解决大规模问题.由于对较大规模的问题,目前的近似算法尚不能在较短的时间内给出高质量的解,因此提出了多重归约算法.该算法的基本原理是通过对TSP问题的局部最优解与全局最优解之间关系的分析,发现对局部最优解的简单的相交操作能以很高的概率得到全局最优解的部分解.利用这些部分解可以大大缩小原问题的搜索空间,同时也不会降低搜索的性能.这就是所谓的归约原理.再通过多次归约使问题的规模降到足够小,然后对这个较小规模的实例直接用已有的算法求解,最后通过相反的次序拼接部分解,最终得到一个合法的解.在TSPLIB(traveling salesman problem library)中,典型实例上的实验结果表明,此算法在求解质量和求解速度上与目前已知的算法相比有较大的改进.

摘要:协调检查点设置及回卷恢复技术作为一种有效的容错手段,已广泛地运用在集群等并行/分布计算机系统中.为了进一步降低协调检查点设置的时间和空间开销,提出了一种基于消息计数的协调检查点设置算法.该算法无须对底层消息通道的FIFO特性进行假设,并使同步阶段引入的控制消息复杂度由通常的O(n²)降低到O(n),有效地提高了系统的效率和扩展性.

摘要:DTD(distributed termination detection)是分布式算法研究中的一个重要问题.如果不能探测计算的终止,算法就失去了其现实意义.Mattern提出的credit-recovery算法实现了消息最优,但只局限于在集中式计算中应用.对其进行了改进,使其能够应用在非集中式计算中,以更适合分布式环境.

摘要:使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessor_P刻画程序P在单机上运行,用时序逻辑式Spec_P刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessors_P即使在出现硬件错误的情况下运行,也能满足性质Spec_P.

摘要:支持动态可变并具备灵活性是人们在实际应用中对工作流管理系统提出的新要求,已有的相关研究工作都集中在对工作流中发生变化的某个具体问题上.提出了支持动态特性的工作流过程元模型,可以为动态过程模型的设计提供指导.从时间和工作流组成的过程级别两个角度分析了其动态特性的表现,扩展了工作流管理联盟的工作流元模型.扩展后的过程元模型在工作流的建立阶段力求将动态特性进行描述和定义,在工作流执行阶段可以根据已定义的动态属性,处理过程的变化情况.基于该元模型,工作流管理系统既具有灵活性,又有利于变化控制操作.

摘要:软件时间性能分析与评估技术是实时软件开发中的一个重要课题.提出了一种基于控制流程图的程序执行时间的可视化分析框架,研究了中间代码段与源程序中语句的对应关系的自动分析、源程序语句行的CPU周期数的提取和计算方法、基于控制流程图的点到点最大时间分析算法和CPU周期的绝对时间估计方法.设计并实现了一个实用的基于控制流程图的程序执行时间静态分析与评估工具.最后,对研究工作进行了相关比较和总结.

摘要:目前的访问控制模型都是从系统的角度出发去保护资源,在进行权限的控制时没有考虑执行的上下文环境.然而,随着数据库、网络和分布式计算的发展,组织任务进一步自动化,与服务相关的信息进一步计算机化,这促使人们将安全问题方面的注意力从独立的计算机系统中静态的主体和客体保护,转移到随着任务的执行而进行动态授权的保护上.介绍了一种称为基于任务的访问控制TBAC(task-based access control)的访问控制机制.它从工作流中的任务角度建模,可以依据任务和任务状态的不同,对权限进行动态管理.TBAC非常适合分布式计算和多点访问控制的信息处理控制以及在工作流、分布式处理和事务管理系统中的决策制定.介绍了TBAC的基本概念,对其模型进行了形式化描述和分析.可以预见,TBAC将在办公及商业等多种领域中得到广泛的应用.

摘要:随着实时系统应用的日益广泛,多类型实时和非实时任务并存的情况给系统调度机制带来了新的需求和挑战.开放式实时系统的相关研究因为解决这一问题而受到关注,也为调度理论与方法带来了新的思路.在阐述了开放式实时系统的基本概念和理论的基础上,提出了一种调度对象的层次性模型,适用于开放式实时调度环境.对几种有代表性的相关方法进行了详细的比较研究,指出它们各自的功能特征和适用范围及其共同特征.把不同方法进行有机集成是可行的,也是一个发展方向,可以使各方法在集成的调度机制内各施所长,更适合于开放式实时系统的应用环境.

摘要:对安全政策灵活性的支持是现代安全操作系统追求的目标之一,DTOS(distributed trusted operating system)项目提出了安全政策格的思想,为安全政策灵活性的研究提供了一种很好的手段.然而,DTOS项目给出的安全政策的格描述把多级安全性(multi-level security,简称MLS)政策认定为静态安全政策.首先,从理论上构造MLS政策的一个实施策略,说明MLS政策具有历史敏感性,从而具有动态特征,不能简单地作为静态安全政策对待.同时,给出所构造的实施策略的实现算法,说明该实施策略与常规实施策略具有相同的复杂度,是一个实用的实施策略.由此证明,可以找到合理、灵活、实用的实施策略,使MLS政策具有历史敏感性,从而证明把MLS政策认定为静态安全政策的不合理性.

摘要:讨论了青鸟面向对象软件建模工具JBOO(Jade Bird object-oriented)的设计和实现方法.对JBOO所支持的青鸟面向对象规范作了简介,对JBOO的系统结构和功能进行了详细地描述,并提出了一种面向对象的软件建模工具的实现方法.最后,将JBOO与典型的同类工具作了比较.

摘要:详细分析了Chonlameth Arpnikanondt提出的基于UML约束的嵌入式系统的软、硬件协同设计方法(CBC/UML),并指出了它运用于复杂的嵌入式系统设计时的不足.针对这些不足,扩展了约束的概念,提出了一套相应的改善方法.并利用中国科学院软件研究所研制智能电话机的例子具体阐述了该解决方法.

摘要:Internet的测量与分析为加强网络管理、提高网络利用率、防范大规模网络攻击提供了技术平台,已成为学术界、企业界和国家政府部门所普遍关心的重要问题之一.介绍了网络测量与分析的主要研究内容,以及国内外相关领域的研究现状,并对该领域的关键技术和难点问题进行了分析,同时给出了网络测量与分析的3个典型应用案例.

摘要:介绍了提高Web服务器性能的前沿技术--分布式Web服务器系统,讨论了现有各种方案的优缺点,在此基础上提出一种新的分布式Web服务器系统.该系统使用基于标记的缓存协作用户请求分发方法(tag based cache cooperative Web requests distribution,简称TB-CCRD),通过前端机把系统中各个Web服务器的缓存组织成一个大的虚拟缓存系统,提高系统的整体缓存命中率,缩短了请求的响应时间;通过分布式处理TCP连接转交来消除前端机的性能瓶颈;利用标记通告URL在缓存中的位置,避免了额外的系统内部通信.从而得到了一个可扩展的高性能分布式Web服务器系统.

摘要:研究了通用多速率组播加权公平速率分配问题.首先,给出了一个形式化的多速率组播网络模型,在该模型中考虑了接收者的异构性.在此基础上,定义了通用多速率组播加权Max-Min公平概念,建立了通用多速率组播加权Max-Min公平速率分配基本理论.最后给出了一个解决通用多速率组播加权Max-Min公平速率分配问题的集中式算法,并证明了该算法的正确性.

摘要:移动Ad hoc网络(mobile Ad hoc network,简称MANET)作为一种新型移动无线通信网,与其他通信网络相比独有的特性增加了网络管理的难度.目前对MANET网络管理的研究处于起步阶段,一些标准尚未制定,而且像存在单向链路和节点的相对移动性这类问题也在研究中被忽视.为此,提出了一个利用令牌机制与最小节点标识相结合,适用于层次性管理结构的基于图的MANET簇生成算法,以及对MIB(management information base)的建议性改进.算法充分考虑了网络存在的单向链路和节点的相对移动性,提高了网络管理的灵活性和可扩展性,为MANET的网络管理提出了一种新方法.

摘要:在移动分布式计算环境中,事务移动性和无线网络固有的缺陷使得传统的分布式实时事务管理机制不足以支持移动分布式实时事务的执行,故有必要为移动实时事务研究新的事务处理机制,以提高其成功率.着重研究移动实时事务的提交机制.首先,通过分析移动分布环境中实时事务的特点给出了一个基于功能替代的移动实时嵌套事务模型.然后,提出了一个基于此模型的三层提交结构以及能够保证移动实时事务原子性和结构正确性的三阶段实时提交协议3PRTC(three-phase real-time commit).性能测试表明,所提出的事务模型及其提交机制能够提高实时事务的成功率.

摘要:对门限秘密共享体制中的防欺诈措施进行了研究,将门限秘密共享体制与RSA与单向函数相结合,充分利用RSA和单向函数进行数据合法性的验证.提出了基于RSA防欺诈的门限秘密共享体制,对该体制的欺诈等价于攻击RSA体制;又提出了基于RSA和单向函数防欺诈的门限秘密共享体制,对该体制的欺诈等价于攻击RSA体制或单向函数.这两个体制具有很强的防止欺诈能力,使欺诈成功的概率限定于一个很小的值,而不论欺诈者具有多么高的技术,因而是无条件安全的.另外,所提出的防欺诈的门限秘密共享体制具有很高的信息率.

摘要:密钥管理系统是安全组播的重要组成部分,而用户密钥存储量和密钥更新代价又是衡量密钥管理系统性能的关键因素.一个高性能的密钥管理系统应具有较小的用户密钥存储量和密钥更新代价.利用信源编码理论深入研究了基于用户概率模型的密钥管理问题,证明了采用密钥Huffman层次结构的密钥管理系统的平均密钥更新代价和用户密钥存储量最小,同时还推导得出了密钥层次结构的理论平均密钥更新代价和用户密钥存储量的下限.