杂志简介：《软件学报》杂志经新闻出版总署批准，自1990年创刊，国内刊号为11-2560/TP，是一本综合性较强的计算机期刊。该刊是一份月刊，致力于发表计算机领域的高质量原创研究成果、综述及快报。主要栏目：理论计算机科学、系统软件与软件工程、模式识别与人工智能、数据库技术、计算机网络与信息安全、计算机体系结构
杂志简介：《软件学报》杂志经新闻出版总署批准，自1990年创刊，国内刊号为11-2560/TP，是一本综合性较强的计算机期刊。该刊是一份月刊，致力于发表计算机领域的高质量原创研究成果、综述及快报。主要栏目：理论计算机科学、系统软件与软件工程、模式识别与人工智能、数据库技术、计算机网络与信息安全、计算机体系结构
作者：詹乃军 王戟 李宣东 刊期：2016年第03期
形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专题收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.
作者：马莎 施智平 李黎明 关永 张杰 Xiaoyu SONG 刊期：2016年第03期
几何代数是一种用于描述和计算几何问题的代数语言,由于它统一表达分析和不依赖于坐标的几何计算等优点,现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具.然而,利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等,都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密...
作者：李轶 冯勇 刊期：2016年第03期
运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法.该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.
作者：孙景昊 关楠 邓庆绪 张鑫 杨丰源 刊期：2016年第03期
基于实时演算（real-time calculus,简称RTC）理论,为单/双行道两类城市交通网络的定时和自适应两类信号控制系统建立了统一的形式化模型.首先,将车流和交叉路口分别建模为RTC的到达曲线和资源曲线;然后,根据不同信号控制策略,将紧邻路口间的曲线进行综合计算,得到整个交通网络的RTC模型.应用最小加代数方法,RTC模型能够计算车辆在路口的最长等...
作者：陈睿 杨孟飞 郭向英 刊期：2016年第03期
在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程（任务）有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访...
作者：吕江花 高世伟 马世龙 孙波 李先军 刊期：2016年第03期
安全苛刻系统的可信性需求迫切,支持可信性评估的数据主要来自于测试.为了保证测试数据的可靠性和正确性,特别是对安全苛刻系统这类复杂系统,手工测试实际不可行.研发测试语言是实现自动化测试的有效途径,也是安全苛刻系统自动化测试发展的必然趋势.针对安全苛刻系统通用测试语言应独立于具体设备包括被测安全苛刻系统、测试设备的应用需求,对安...
作者：王婷 陈铁明 刘杨 刊期：2016年第03期
精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学...
作者：汤恩义 周岩 欧建生 陈鑫 刊期：2016年第03期
条件判定覆盖（condition/decision coverage,简称C/DC）准则是各种安全攸关软件测试中常用的测试覆盖准则,它要求软件测试覆盖程序中每个判定以及条件的真/假取值.现有的自动测试生成方法在针对该准则的测试用例生成过程中存在很多不足.例如：符号执行方法很难处理较为复杂的非线性条件约束,并在处理程序的规模上受到很大限制;希尔攀登法由于在...
作者：杨志斌 赵永望 黄志球 胡凯 马殿富 Jean-Paul BODEVEIX Mamoun FILALI 刊期：2016年第03期
能够提供更强计算能力的多核处理器将在安全关键系统中得到广泛应用,但是由于现代处理器所使用的流水线、乱序执行、动态分支预测、Cache等性能提高机制以及多核之间的资源共享,使得系统的最坏执行时间分析变得非常困难.为此,国际学术界提出时间可预测系统设计的思想,以降低系统的最坏执行时间分析难度.已有研究主要关注硬件层次及其编译方法的...
作者：陈鑫 黄超 张一帆 梅一鸣 刊期：2016年第03期
干涉问题是指基础程序和方面之间或者方面之间发生不需要的相互作用,导致最终程序中产生不想要的功能,危害程序的正确性.很难检测和修正在面向方面设计中存在的干涉,已经成为推广面向方面技术的阻碍.受到技术自身可扩展能力的局限,现有的基于模型验证技术的工作不能有效地处理功能干涉问题.设计开发了基于推理验证技术直接检查和去除面向方面设...
作者：甘庭 夏壁灿 刊期：2016年第03期
栅栏函数在连续系统验证方面有着广泛的应用,其主要想法在于：在可达集和非安全集之间寻找一个栅栏,从初始区域出发的路径不会越过这个栅栏,而非安全区域在栅栏的另外一端.这样,就可以通过寻找栅栏函数来验证一个系统的安全性.近年来,已有一些工作讨论连续系统在无界时间情况下的栅栏函数生成.但是对于有些系统,人们可能只关心其在有界时间内的...
作者：陈铭松 顾璠 徐思远 陈小红 刊期：2016年第03期
近年来,智能大厦的概念在国内外受到了高度的关注.相比于传统的建筑,智能大厦更加节能、舒适、易维护,已成为未来建筑的发展趋势.作为智能大厦空调通风系统的关键部分,空调系统及其调度策略决定了大厦整体的节能效果以及大厦中用户的舒适度.然而,由于智能大厦所处的环境具有许多不确定因素,极大地增加了空调系统调度策略设计与评估的复杂程度.因...
作者：陆旭 段振华 田聪 刊期：2016年第03期
由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTL^SL是一种二维（时间和空间）时序逻辑,它结合了分离逻辑（separation logic）与命题投影时序逻辑PPTL（propositional projection temporal logic）,能够描述和验证操作链表的指针程序的时序性质.简要回顾了PPTL^SL的相关理论,并详细介绍了工具S...
作者：宋富 吴志林 刊期：2016年第03期
无穷数据广泛存在于计算机程序和数据库系统中.受到形式验证与数据库两方面应用需求的推动,面向无穷数据的形式模型已经成为理论计算机科学的研究热点之一.对面向无穷数据的形式模型（逻辑与自动机）进行了相对全面而详细的总结.主要按照不同自动机模型对无穷数据的处理方式加以组织,并关注相关判定问题,即：自动机的非空性问题、语言包含问题以...
作者：黄震华 张佳雯 田春岐 孙圣力 向阳 刊期：2016年第03期
排序学习技术尝试用机器学习的方法解决排序问题,已被深入研究并广泛应用于不同的领域,如信息检索、文本挖掘、个性化推荐、生物医学等.将排序学习融入推荐算法中,研究如何整合大量用户和物品的特征,构建更加贴合用户偏好需求的用户模型,以提高推荐算法的性能和用户满意度,成为基于排序学习推荐算法的主要任务.对近些年基于排序学习的推荐算法研...
影响因子：0.16
期刊级别：省级期刊
发行周期：双月刊
影响因子：1.2
期刊级别：省级期刊
发行周期：半月刊
影响因子：1.75
期刊级别：北大期刊
发行周期：月刊
影响因子：1.26
期刊级别：部级期刊
发行周期：月刊
影响因子：0.37
期刊级别：省级期刊
发行周期：月刊
影响因子：1.71
期刊级别：统计源期刊
发行周期：半月刊
影响因子：--
期刊级别：部级期刊
发行周期：月刊
影响因子：0.62
期刊级别：北大期刊
发行周期：双月刊
影响因子：0.95
期刊级别：北大期刊
发行周期：月刊
影响因子：0.3
期刊级别：省级期刊
发行周期：月刊
影响因子：0.68
期刊级别：省级期刊
发行周期：月刊
影响因子：2.24
期刊级别：北大期刊
发行周期：月刊