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

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

面向新兴系统的形式化建模与验证方法专题前言

<正>形式化方法是计算机科学的重要理论基础.它以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法.近年来,随着相关技术的发展,形式化方法已经在越来越多的新兴系统中得到应用并取得显著效果.为了记录中国学者在新兴系统的形式化建模与验证理论、方法、工具和应用等方面的最新研究成果,特设立此专题.本专题采取自由投稿的方式,共收到17篇投稿,其中16篇通过了形式审查.特邀编辑邀请17位领域专家参     

软件形式化方法与应用专题前言

形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专刊收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.     

智能数据管理与分析技术专刊前言

数据管理与智能计算的深度融合已经成为大数据时代顺利前行的迫切需求.智能数据管理旨在“为数据增添智能”,是数据科学与技术的重要基石,更是大数据产业蓬勃发展的关键支撑.一方面,将新一代人工智能方法应用于先进数据管理技术,尝试探索和突破智能数据管理与分析的理论体系、技术方法及系统平台,已经成为数据管理领域的新兴研究方向;另一方面,研发面向人工智能的数据库基础软件,为新一代人工智能技术的研发和广泛应用提供海量数据的有效存储、查询、分析和挖掘等的系统支持,亦是国家科技创新的决定性因素.智能数据管理与分析领域日益得到学术界和工业界的普遍关注,其理论、技术和方法亟待深入地探索与思考.目前,针对智能数据管理与分析的研究仍然处于起步阶段,有很多需要研究的问题. 本专刊公开征文,共收到投稿38篇(包括第35届中国数据库学术会议(NDBC 2018)推荐的12篇高质量论文).其中,37篇论文通过了形式审查,内容涉及智能数据管理与分析技术和应用.特约编辑先后邀请了 70多位专家参与审稿工作,每篇投稿至少邀请2位专家进行评审.稿件经初审、复审、NDBC 2018会议宣读和终审4个阶段,历时5个月,最终有20篇论文入选本专刊.根据主题,这些论文可以分为4组.     

形式化方法概貌

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明：其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.     

云计算安全研究专刊前言

随着信息技术的发展快速步入大数据时代,云计算作为推动信息技术实现按需供给、促进信息技术和数据资源充分利用的全新业态,已成为信息化发展过程中的重大变革和信息技术发展的必然趋势.然而,正是由于云计算模式所具有的一些特性,如云计算平台的服务外包和基础设施公有化特征、超大规模多租户资源共享特征、云计算环境的动态复杂性、云平台资源的高度集中性、云平台的开放性等,使得人们在享受云计算所提供的应用便利和成本低廉的同时,也逐渐意识到了其在诸多安全方面的全新挑战.新的计算模式需要新的安全保障技术、理论和方法来应对安全挑战,如在外包环境下如何实现用户数据安全防护、如何实现虚拟化技术的安全性、如何设计适合云计算环境的安全协议、如何构建一个安全可靠的云计算平台以及如何测试和评价云计算平台的安全性等.本专刊选题为“云计算安全研究”,力图反映我国学者在云计算安全领域的近期研究成果. 专刊公开征文仅限一轮,共征得投稿37篇.稿件几乎全部来自国家211大学或者中科院相关研究单位,质量相对较高.稿件内容涉及云计算安全理论、算法以及应用等诸多方面的研究内容.对于云计算环境,云数据以及云计算应用等方面的安全问题进行了深入的探讨,反映了我国学者近期对于云计算安全关注的主要方向.特约编辑先后邀请了40余位云计算安全及相关领域的专家参与审稿工作,每篇投稿邀请2位专家进行评审.稿件评审时间历经3个月,经初审、复审、云计算安全专题研讨会宣读和终审各个阶段,最终由软件学报编委会批准,决定19篇论文入选本专刊.纵观所收录的文章,它们的研究范围和内容可分为三个部分.     

可信系统性质的分类和形式化研究综述

计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统.     

几何代数的高阶逻辑形式化

几何代数是一种用于描述和计算几何问题的代数语言.由于它统一的表达分析和不依赖于坐标的几何计算等优点现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具, 然而利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.本文在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型,主要包括片积、多重矢量、外积、内积、几何积、几何逆、对偶、基矢量运算和变换算子等的形式化定义和相关性质定理的证明.最后为了说明几何代数形式化的有效性和实用性,本文在共形几何代数空间中对刚体运动问题提供了一种新的简单有效的形式化建模与验证方法.     

用Pi演算为业务过程建模的生命周期

随着企业竞争日趋激烈,业务过程建模技术变得越来越重要.由于形式化方法降低了二义性并为模型的分析和验证提供了可行性,因此形式化的业务过程建模技术在学术界引起了很多人的关注,但到目前为止仍缺乏一套既能方便地进行过程建模,又具有对模型进行形式化分析与验证的整套理论体系.从生命周期的角度入手,探讨如何把形式化方法更有效地应用于商业过程建模.主要工作在于提出了基于Pi演算的生命周期,探讨了生命周期各个阶段使用的技术和工具.     

基于Web的形式化方法工具RRTChecker的研究与设计

形式化方法工具通常是在UNIX/Linux系统下设计开发的,难于使用阻碍了形式化方法的进一步推广.本文针对形式化方法RAISE,提出了一种研究和开发基于Web的工具的方法.该方法以原有的RAISE工具为基础,通过Shell管道拦截技术、ASP技术、ActiveX DLL技术及路径重写技术,将工具的所有功能集成整合到统一的、用户友好的Web界面上,用户可通过鼠标在浏览器中进行不同的操作.原有的RAISE工具的所有功能,在基于浏览器的集成化工具中得到全面支持.该方法也为开发其它形式化方法基于Web的工具提供了新思路.     

前言

<正>滑模控制因其对系统不确定性、参数摄动和外部扰动的强鲁棒性和易于工程实现等优点,已经成为非线性控制领域的一个重要分支.一方面,在处理非线性系统镇定、干扰抑制、参数不确定、输入/输出约束等非线性控制理论问题时,滑模控制理论得到了极大的发展,一系列滑摸控制相关设计工具和理论分析方法被提出,并得到逐步完善.另一方面,滑模控制理论也被尝试应用于多种实际工业系统,如机器人系统、电机系统、电动汽车、飞行器等.尽管滑模控制理论的发展已有几十年,但随着近年来智能系统的快速发展,滑摸控制理论还面临着一系列的挑战,如处理混杂系统、网络化系统、高阶非线性系统、抖振抑制等问题.此外,随着数字控制器性能的急速提升,滑模控制技术在工业控制系统中的实际应用也备受关注.基于上述考虑,本专刊聚焦滑模控制的最新理论、研究方法及其应用成果,共录用20篇研究论文,其中滑模控制基础理论与算法相关论文4篇,滑模控制理论在智能制造、电机控制、电气系统、无人机、自动驾驶、航空航天等领域的相关应用论文16篇.在滑模控制理论与算法方面,王永骥等研究了具有约束的二阶系统的固定时间跟踪控制问题,提出了具     

“工程博弈论”专刊前言

正现代工程系统中决策主体繁多,决策环境复杂,竞争与合作并存,博弈论的工程应用也日益广泛.受《工程控制论》启发,将工程设计与试验中应用博弈论的基本概念、建模与求解方法以及考虑工程实际的技术性条件进行决策的理论称为"工程博弈论".本专刊关注博弈论在工程技术领域的理论研究进展与应用成果,共录用17篇论文,包括综述论文2篇,博弈基础理论与算法相关论文6篇,工程应用相关论文9篇,其中电力     

《软件学报》可信软件的构造与演化专刊征文通知

本专刊将收录国内外在可信软件构造和演化方面的具有创新性的研究成果,展示可信软件在理论、方法和技术方面的研究现状。本专刊将于2009年第12期出版,现特向国内外关注该主题的研究人员公开征集稿件。读者群体包括软件工程、可信计算和分布计算领域的研究者和工程实践人员等。     

《软件学报》可信软件的构造与演化专刊征文通知

本专刊将收录国内外在可信软件构造和演化方面的具有创新性的研究成果,展示可信软件在理论、方法和技术方面的研究现状。本专刊将于2009年第12期出版,现特向国内外关注该主题的研究人员公开征集稿件。读者群体包括软件工程、可信计算和分布计算领域的研究者和工程实践人员等。     

《软件学报》网格计算专刊征文通知

本专刊瞄准与网格技术及其应用相关的基础性、前瞻性、战略性的重大理论和关键技术问题,以及网格技术与其他学科领域的交叉性,同时为了加强网格界和各应用领域专家之间的合作与交流,共同促进技术进步,推动网格技术在国民经济重大领域的应用普及,提高该领域信息化程度。本专刊面向全国征集论文,欢迎广大学者、专家、工程技术人员积极投稿,现将专刊论文征集的有关事项通知如下:专刊题目:网格计算特约编辑:金海(华中科技大学)、郑纬民(清华大学)一、征文范围1.网格基础理论研究主要包括网格核心协议和核心服务的研究,如服务管理、网格执行管理…     

面向智能制造的业务过程管理与服务技术专题前言

业务过程管理(business process management,简称BPM)致力创新企业业务过程管理、分析、控制与改进的系统化与结构化方法,其目标在于改进产品质量、提升服务水平,是现代信息系统的共性基础技术.当今全球产业结构正呈现由“工业型经济”向“服务型经济”加速转型.智能制造是实施《中国制造2025》的主攻方向之一,是落实工业化和信息化深度融合、打造制造强国的战略举措,更是我国制造业紧跟世界发展趋势、实现转型升级的关键所在.如何针对智能制造的发展需求,研究更高效、柔性、智能的业务过程管理与服务技术面临巨大的机遇与挑战. 专题公开征文,共征得投稿31篇.这31篇论文通过特约编辑形式审查,有29篇论文进入到评审阶段.特约编辑先后邀请了30余位业务过程管理、服务计算、软件工程、智能制造等相关领域的专家参与审稿工作,每篇投稿邀请2位专家进行评审.稿件评审历经5个月,经初审、复审、第7届中国业务过程管理大会(CBPM 2017)会议宣读和终审4个阶段,最终有10篇论文入选本专题.这10篇论文主要涉及模型管理、过程挖掘、调度方法、服务技术等研究方向,其中模型管理2篇、过程挖掘2篇、调度方法3篇、服务技术3篇.     

基于Petri网的面向方面用况建模研究

将现有的在面向对象领域中的一些比较成熟的技术使用到面向方面领域是一个重要的研究方向.提出在需求分析时通过UML的扩展机制来进行面向方面的用况建模方法,阐述如何应用Petri网来对面向方面用况模型进行形式化,以增加用况模型的语义约束.通过一个在线外汇交易平台系统的建模实例,详细说明基于Petri网的面向方面用况建模方法,最后应用这种方法在需求分析阶段方便、有效地产生测试用例.实践证明,基于Petri网的面向方面用况建模方法取得了良好的效果.     

2016年绿色计算专题前言

计算系统的能耗问题是影响计算系统本身发展、使用以及人类生存环境的重大问题,受到学术界、工业界等各方面的高度关注。本刊定于今年出版“绿色计算”专辑,为计算机系统的研究、开发、使用和管理等工作者提供一个展示计算系统节能创新技术的平台。本专辑征文发出后,获得计算机领域专家学者的广泛支持,收到大量投稿;稿件经过数十位专家的评审,遴选出9篇论文刊登于本专辑。本专辑刊登的文章涵盖了面向高能效的体系结构设计、重要应用的高能效实现以及高能效的系统资源管理和调度等方面的内容。     

社会计算:理论与方法专刊前言

信息技术与互联网的深入发展与普及,对人们的社会交往模式产生了深远的影响,其发展也带来一场计算技术的变革.信息科学技术的研究从以往重视具体技术问题,发展到更高层次上利用计算手段模拟及解析社会理论和研究社会相关问题,进行计算科学与社会科学的交叉研究.近年来,社会计算迅速兴起和发展,并得到国内外计算机及相关交叉学科领域的高度重视.与此同时,为了有效应对复杂和动态变化的网络化社会带来的新型问题与挑战,亟需发展社会计算的基础理论、建模、分析与计算方法.本专刊收录的12篇论文反映了我国学者近期在社会     

CIM建模及模型形式化方法研究综述

以模型为驱动的开发方法是当前软件工程领域研究的热点,计算无关模型(computation independent model,CIM)在模型驱动架构中关注系统的需求和环境,其有效的建模方法和模型形式化是实现高层概念模型至代码自动转换的关键.首先介绍了现有CIM建模内容和方法;然后分析了现有CIM模型形式化方法现状与不足;最后探讨了针对不同应用系统可行的多视图多层次CIM建模方法及一致性问题研究,并提出CIM完全形式化方法研究的可行方案.