软件学报杂志 北大期刊 CSCD期刊 统计源期刊

软件学报 2005年第03期杂志 文档列表

软件学报杂志理论计算机科学

由一阶逻辑公式得到命题逻辑可满足性问题实例327-335

摘要：命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

不可满足公式的同态证明系统336-345

摘要：合取范式(CNF)公式H到F的同态(是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.

一种用于Java程序验证编译的标签类型346-354

摘要：在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继承接口的Java程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言能够有效地实现Java程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语言的Java字节码即时编译器中.

QRDChecker：一个QRDC模型检验工具355-364

摘要：反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.

软件学报杂志默认

第2届“游戏与虚拟现实在教育中的应用”国际研讨会会议通知335-335

“数字媒体处理及数字博物馆技术”高级研讨班会议通知335-335

第10次全国Petri网学术年会暨形式化方法学术讨论会征文通知399-399

2005年全国开放式分布与并行计算学术会议征文通知426-426

第1届中国分类技术及应用研讨会（CSCA2005）征文通知452-452

软件学报杂志算法设计与分析

均值漂移算法的收敛性365-374

摘要：均值漂移是一种有效的统计迭代算法,已广泛应用于聚类分析、跟踪、图像分割、图像平滑、滤波、图像边缘提取和信息融合等方面.但是,其收敛性仍没有得到严格的证明,而收敛性是任何迭代算法的必要前提.推广并严格证明了该算法的收敛性.首先将均值漂移算法做了以下推广:反映不同样本点处局部空间结构的差异及其各向异性.然后,在推广的条件下从数学上严格证明了均值漂移算法的收敛性.最后,探讨了均值漂移算法中参数的自适应选择方法.从而为该算法的应用奠定了理论基础.

时隙间迭代的输入队列交换机Round-Robin调度算法375-383

摘要：输入队列因具有良好的可扩展性而广泛应用于高速交换机和路由器中,但输入队列需要精心设计调度算法以获取较好的性能.Round-Robin算法因其简单性和并行性而得到广泛的研究,但现有的Round-Robin算法在突发流量和非均匀流量下的负荷-延迟性能较差.提出了调度决策在时隙间进行迭代的思想,并利用队列长度具有随机性的特点设计了能近似最大匹配的Round-Robin算法--iSLOT.仿真结果表明,iSLOT不仅在均匀流量下是稳定的,在非均匀流量和突发流量下的吞吐率及延迟性能均远好于现有的Round-Robin算法.

一种分布式吴方法计算模型384-391

摘要：吴方法是由我国科学家吴文俊院士开创的一个新兴研究领域.考虑到吴方法"分而治之"的思想非常适合分布式计算,将分布式计算技术引入到该方法的计算过程中,给出一种既可以在集群环境下,也可以在网格环境下实现的分布式吴方法计算框架.首先分析了吴方法分布式计算需求,并以特征列计算为例来说明吴方法分布式计算算法,然后讨论了符号计算基本数据类型:大整数和多项式的消息传递方法,最后简单给出了在网格环境下基于符号计算软件系统ELIMINO和网格中件间Globus Toolkits 3的分布式吴方法计算环境的设计、实现与实验结果.

κ-Median近似计算复杂度与局部搜索近似算法分析392-399

摘要：κ-Median问题的近似算法研究一直是计算机科学工作者关注的焦点，现有研究结果大多是关于欧式空间和Metric空间的，一般距离空间κ-Median的结果多年来一直未见．考虑一般距离空间κ-Median问题，设dmax／dmin表示k-Median实例中与客户点邻接的最长边长比最短边长的最大者，首先证明dmax/dmin≤ω+ε的κ-Median问题不存在近似度小于1+ω-1/e的多项式时间近似算法，除非NP包含于DTIME（n^O(log longn),由此推出Metric κ-Median问题不可近似到1+2/e,除非NP包含于DTIME（n^O(log logn)，然后给出κ-Median问题的一个局部搜索算法，分析表明，若有dmax/dmin≤ω,则算法的近似度为1+ω-1/2,该结果亦适用于Metric κ-Median．ω≤5时，局部搜索算法求解Metric κ-Median的近似度为3，好于现有结果3+2/p．通过计算机实验，进一步研究了κ-Median局部搜索求解算法的实际计算效果和该算法的改进方法。

软件学报杂志系统软件与软件工程

工作流活动多实例的调度控制400-406

摘要：支持多实例的工作流管理系统为工作流过程处理带来极大的灵活性,活动多实例要解决的主要问题之一是多实例的调度控制.在分析了多实例的分配和汇聚等问题之后,针对过程中活动间不同活动语义的上下文,对活动多实例的活动属性进行了统一的形式描述,提出了活动多实例控制体Shell,用于控制活动多实例的分配和提交.Shell可以根据不同的活动语义,处理多实例的同步并控制整个过程的运行.Shell的提出解决了工作流执行中一个活动多个执行实例的同步执行问题.

一种支持软件过程控制和改进的主动度量模型407-418

摘要：提出了一种支持软件过程控制与改进的主动度量模型AMM(active measurement model)和度量方法.模型形式化描述了软件过程的目标、特征和度量指标等关键元素以及相互间的关系,给出了确定软件过程度量的原则、方法和步骤.基于该度量模型,软件组织一方面可以依据确定的过程目标,主动导出合适的度量过程;另一方面还可以依据度量的结果,识别过程改进的机会,并主动导出过程改进的方向.为正确的决策和成功的结果提供有效的支持.

针对一般线性约束的Petri网控制器设计方法419-426

摘要：针对基于Petri网离散事件系统关于标识向量和Parikh向量的不等式约束反馈控制器设计问题,提出一种新的控制器设计方法.该方法首先利用Petri网的状态方程把关于标识向量和Parikh向量的不等式约束转变成关于Parikh向量的不等式约束,然后基于Petri网库所是关于Parikh向量的不等式约束的观点构造控制器.最后将该方法与Iordache和Moody提出的方法作比较,实验结果显示该方法更简单、有效.

软件需求定量分析及其映射的模糊层次分析法427-433

摘要：在用数量化理论3类(quantification theory of type 3,简称QT3)定量地分析软件需求的基础上,以质量功能展开(quality function deployment,简称QFD)中的质量屋(house of quality,简称HOQ)系列矩阵为纲领,基于由模糊技术改进后的模糊层次分析法(fuzzy analytic hierarchy process,简称FAHP),提出了一种软件需求定量分析及其向设计实现过程模糊映射的方法.将该方法具体应用于CD-R/RW光盘刻录机软件的开发过程,其有效性得到了验证.

软件学报杂志计算机网络与信息安全

MANET中TCP改进研究综述434-444

摘要：传统TCP(transmission control protocol)本是为有线网络设计,它假设包丢失全是由网络拥塞引起,这个假设不能适应于MANET (mobile ad hoc network),因为MANET中除了拥塞丢包以外,还存在由于较高比特误码率、路由故障等因素引起的丢包现象.当出现非拥塞因素丢包时,传统TCP将错误地触发拥塞控制,从而引起TCP性能低下.任何改进机制都可以分为发现问题和解决问题两个阶段.首先概括了MANET中影响TCP性能的若干问题;然后针对发现问题和解决问题两个阶段,详细地对每一阶段中存在的各种可行方法进行了分类、分析和比较;最后指出了MANET中TCP性能优化的研究方向.