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

软件学报 2011年第06期杂志 文档列表

软件学报杂志形式化方法与工具专刊

形式化方法与工具专刊前言1121-1122

摘要：形式化方法是指有严格数学基础的软件和系统开发方法，支持计算机系统及软件的规约、设计、验证与演化等活动．随着高可信软件的兴起，形式化方法作为重要的途径，关注度日益提高．其作用不仅深化了人们对计算系统规律的认识，而且支持了计算系统开发、运行和演化之工具、平台、环境的构建．本专刊收录的11篇论文反映了近年来我国学者在形式化方法与工具领域的部分研究成果.

2011年全国高性能计算学术年会征文通知1122-1122

摘要：由中国计算机学会主办、中国软件行业协会数学软件分会协办、中国计算机学会高性能专业委员会、山东省科学院、山东信息通信技术研究院、山东省计算中心承办的2011年全国高性能计算学术年会（HPC China 20111将于2011年10月26日-29日在山东济南召开。全国高性能计算学术年会是中国一年一度高性能计算领域的盛会，为相关领域的学者提供交流合作、最前沿科研成果的平台，推动中国高性能计算的发展。

策略驱动的可靠嵌入式系统建模及分析方法1123-1139

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

Object-Z规格说明测试用例的自动生成器1155-1168

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

循环对称化简及在三值模型上的扩展1169-1184

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

场景驱动的服务行为调控1185-1198

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

混合语义时间Petri网模型1199-1209

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

软件体系结构动态演化的条件超图文法及分析1210-1223

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

基于AOP的运行时验证中的冲突检测1224-1235

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

基于自动机理论的分布式实时调度分析工具1236-1251

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

AADL模型可靠性分析评估工具1252-1266

摘要：主要针对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 editor2）,实现基于GSPN模型的可靠性分析评估.同时,结合航空飞行控制系统的可靠性分析评估介绍了ARAM工具的应用情况.

时变网络中国邮路问题的时间自动机模型1267-1280

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

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

P2P流量识别1281-1298

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

属性基加密机制1299-1315

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

无证书公钥密码体制研究1316-1332

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

可量化的移动AdHoc网络时空动态特性评估方法1333-1349

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

高效安全的基于身份的签名方案1350-1360

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

WSANs中基于实时性约束的actor节点优化部署策略1361-1372

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