摘要:为了更精确地认识与改造世界，新一代的嵌入式系统必须将计算世界与物理世界作为紧密交互的整体进行认知，实现集计算、通信与控制于一体的深度融合的理论体系与技术框架，即信息物理系统（cyber-physical systems，简称CPS）.与传统嵌入式系统不同，CPS充分考虑了计算部件与物理环境的深度融合，通过将设备智能化连接，实现物理环境系统与计算系统之间精确感知与高效协同.基于CPS理念设计出来的计算设备可以根据具体任务需求自适应地调整与配置计算逻辑，精确智能地获取外部物理环境信息并做出针对性的实时反应，完成安全可靠的控制服务，从而实现物理世界与信息世界的有机统一.
随着人们对信息技术质量要求的不断提高，CPS迅速在众多安全攸关领域得以部署承担关键任务.从远程精准医疗到智能轨道交通，从无人驾驶到航空航天，从智慧城市到智能制造，无处不见CPS的身影.虽然CPS在众多领域获得成功，然而由于其涉及多维时空约束、异构物理/计算进程交互、运行环境不确定等因素，CPS设计复杂度极高.在缺乏设计自动化方法与技术的情况下，CPS开发周期长且质量难于保证.日益复杂的CPS设计与实现在给产业界与学术界带来巨大挑战的同时，也创造了大量新的机遇，CPS设计自动化目前已成为国际相关研究领域的关注与研究热点.
本专题采取自由投稿的方式，共收到14篇投稿.特约编辑邀请了30余位领域专家参与审稿，每篇稿件至少邀请3位专家进行评审，每篇录用稿件都经过至少3轮审稿.14篇稿件中共计10篇稿件通过第1轮评审，8篇稿件通过第2轮评审，并在CCF软件工程专业委员会、系统软件专业委员会年会全国软件与应用学术会议NASAC2019会议上进行了报告.经过第3轮终审及少数稿件的第4轮复审后，最终有6篇论文入选本专题.
《基于SHML的CPS行为建模及仿真》提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.
《垂悬指针检测与防御方法》针对复杂系统软件中广泛出现的悬垂指针问题进行研究，提出了一种名为DangDone的垂悬指针防御方法，通过在编译时的程序转换来定位潜在的垂悬指针并防御use-after-free或double-free漏洞.
《自主机器人多智能体软件架构及伴随行为机制》提出了基于多智能体的自主机器人控制软件软件架构，以及基于相应架构的伴随行为机制.该工作基于分步规划和动态决策的思想设计并实现了相应自主决策算法DAAB，并在相应仿真环境和实际机器人环境上进行了案例分析.
《轨道交通联锁领域特定语言的形式化》基于轨道交通联锁系统中故障的随机性和行为实时性的特点，提出了基于建立随机混成系统模型来仿真、预测轨道交通连锁系统的方法.该方法在实际联锁系统进行实例研究，并在UPPAAL-SMC平台上进行了事故模型的预测分析.
《基于AADL的失效概率分配及安全性评估方法》综合考虑AADL架构的层次化设计、模型复杂度和构件失效造成影响的严重程度，针对安全关键系统提出基于AADL的失效概率分配方法，以应对安全性评估过程中如何分配失效概率的问题.相关技术在飞控CPS系统上进行了实例研究.
《马尔可夫信息物理系统拒绝服务攻击安全控制》研究了马尔可夫跳变信息物理系统在模态依赖拒绝服务（DoS）攻击下的安全控制问题.提出了一种新颖的模态依赖事件触发策略来减少网络资源消耗.
本专题面向信息物理系统的研究人员和工程人员，内容涵盖系统建模、系统架构、可信保障等领域，反映了我国学者在相关领域的高水平研究成果.感谢《软件学报》编委会、CCF软件工程专委会、系统软件专委会对专题工作的指导和帮助，感谢专题全体评审专家及时、耐心、细致的评审工作，感谢踊跃投稿的所有作者.希望本专题能够对形式化方法的科研工作有所促进.
专刊特约编辑、北航计算机学院刘超教授在专刊的筹划阶段分享了大量宝贵的经验，并在征稿、审稿等环节做了大量的工作，使得专刊实施过程得以顺利开展.然而，在本专刊即将完成之际，刘超老师却因病永远离开了我们.刘老师睿智、谦逊、渊博、平和，为推动我国软件工程事业发展做出了重要贡献，我们借此表达深深的怀念和敬意.

摘要:信息物理融合系统（cyber-physical systems，简称CPS）是深度融合了计算进程和物理进程的统一体，是集计算、通信与控制于一体的下一代智能系统，具有广阔的应用前景.CPS的行为具有混成性、随机性等特征，建模及仿真CPS的动态行为对于开发高质量的CPS系统至关重要.但是目前缺乏面向CPS的领域建模方法及建模CPS的领域建模语言，也迫切需要支持仿真CPS领域模型的仿真工具.针对以上问题，提出一种面向CPS领域的随机混成建模语言（stochastic hybrid modeling language，简称SHML）以支持建模CPS系统的行为.首先，根据CPS的领域特征定义了SHML的元模型作为其抽象语法，并定义了SHML的具体语法和操作语义；其次，基于GEMOC框架实现了SHML的可视化建模工具.此外，集成GEMOC的序列化执行引擎和Scilab的连续行为仿真引擎，实现仿真CPS的混成行为.提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.

摘要:随着技术的发展，信息物理融合系统（cyber-physical system，简称CPS）在生活中扮演着越来越重要的角色，例如电力系统、铁路系统.如果CPS遭到攻击，将对现实世界的正常运转造成巨大影响，甚至威胁生命安全.垂悬指针是指向的区域被释放后未被置为空的指针，它是一种会导致攻击的软件缺陷.由垂悬指针导致的use-after-free和double-free漏洞能够执行任意恶意代码.迄今为止，只有少量工作针对垂悬指针进行检测、防御.其中多数都会导致过高的额外运行时开销.提出DangDone用于检测和防御垂悬指针.首先，通过静态分析检测潜在垂悬指针；然后，基于检测到的垂悬指针信息和一系列预定义的指针变换规则，依据指针传播信息变换指针，使得指针及其别名都指向同一个新引入的指针.基于该方法，实现了DangDone的原型工具.基于11个开源项目和SPEC CPU benchmark的实验结果表明：DangDone的静态分析部分只有33%的误报率，指针变换部分只引入了1%左右的额外开销.同时，DangDone成功防护了11个开源项目中的use-after-free和double-free漏洞.实验结果体现了DangDone的高效率及有效性.

摘要:自主机器人是一类由计算机软件控制的信息物理系统，如何支持该类机器人在开放环境下的有效和协调运行，是自主机器人控制软件（control software of autonomous robot，简称CSAR）研究与实践面临的一项重要挑战.基于组织理论的思想，采用Structure-in-5的组织架构模式，提出了基于多智能体的CSAR的软件架构MaRSA（multi-agent robotic software architecture），通过独立抽象CSAR的行为规划、分发、执行等软构件，并显式加强这些构件间的交互，从而为自主机器人行为的有效规划和协调实施奠定架构基础；提出了基于MaRSA架构的伴随行为机制，从因果性、时序性和按需性等3个方面建立了机器人观察行为和任务行为间的伴随关系，并基于分步规划和动态决策的思想，设计并实现了伴随行为的自主决策算法DAAB（decision algorithm of accompanying behaviors）.分别在仿真环境和实际机器人环境下设计了对比性实验，结果表明：与主流的反应式行为决策算法和BDI式概率决策算法相比较，基于MaRSA和伴随行为机制的DAAB算法所生成的伴随行为规划在开放环境下具有可行性和更高效的执行效率.

摘要:作为轨道交通系统的核心子系统之一，对联锁系统进行形式化建模与分析，是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合，由于形式化知识难以掌握，领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题，针对联锁系统的故障随机性、行为实时性、构件可重用的特点，提出设计联锁领域特定语言IS-DSL描述具体的联锁系统的参数，并基于随机混成自动机模板自动生成联锁系统的形式化模型，以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析，根据不同案例设计其领域特定语言；其次，确定联锁系统的系统模型模板，包括环境构件模板和控制器模板，并举例抽取其随机混成自动机模板；在模板基础上定义系统模型生成过程，让领域专家可以通过领域特定语言，输入参数自动生成具体的随机混成自动机系统模型；最后以某站联锁系统为例，展示了基于模板的具体系统模型的生成过程，并通过基于系统模型的事故预测分析，证明了该方法的可行性与有效性.

摘要:当代航空系统是复杂的安全关键信息物理融合系统（cyber-physical system，简称CPS）.失效概率分配是民用航空系统及设备初步系统安全性评估过程的重要工作，AADL（architecture analysis and design language）适用于航电系统的设计开发，对AADL模型实施失效概率分配和安全性评估是不可或缺的.提出了基于AADL的失效概率分配方法，可将系统失效概率分配给子构件，作为其安全性需求.该方法综合考虑系统架构设计、模型复杂度和严酷度（severity）等级.通过结合失效概率分配方法和确定性随机Petri网（deterministic stochastic Petri-net，简称DSPN），进一步提出了基于AADL的安全性评估方法，将系统的AADL模型转换为DSPN模型，以计算子构件的失效概率，并评估子构件是否满足安全性需求，直到设计出满足安全性目标的架构模型.最后给出了失效概率分配方法与安全性评估方法的实现算法和工具结构，并通过将所提出的方法应用到飞行控制系统，表明所提方法能够有效地完成失效概率分配和安全性评估.

摘要:研究了马尔可夫跳变信息物理系统（CPS）在模态依赖拒绝服务（DoS）攻击下的安全控制问题.提出了一种模态依赖事件触发策略来减少网络资源消耗.特别地，DoS攻击被设置为依赖系统模态，从而更贴近实际的应用.基于Lyapunov Krasovskii泛函方法建立了闭环系统在DoS攻击下渐近一致有界的充分性条件.更进一步，根据矩阵技术设计了所需的安全控制器.最后，通过一个实例说明了该方法的有效性.

摘要:软件不变量是软件的重要属性，在软件验证、软件调试和软件测试等领域有重要作用.自20世纪末以来，基于动态分析的不变量综合技术成为相关领域的一个研究热点，并且取得了一定的进展.收集了90篇相关论文对该领域进行系统总结.基于动态分析的不变量综合技术是该领域的核心问题，提出了“学习者-预言”框架统一描述相关方法，并且在此框架内根据学习者的归纳方法将综合技术大致分为4类，分别是基于模板穷举的方法、基于数值计算的方法、基于统计学习的方法以及基于符号执行的方法.其次，讨论了基于动态分析综合的不变量在软件验证和软件工程等领域的重要应用.随后，总结不变量生成技术中常用的实验对象程序和开源的不变量综合工具.最后，总结该领域并展望未来的研究方向.

摘要:设计模式检测是理解和维护软件系统的一项重要工作.以高效识别设计模式变体和提高设计模式识别准确率为目的，将面向对象度量与模式微结构相结合，提出一种基于堆叠泛化的设计模式检测方法.该方法应用典型的机器学习算法，分别训练度量分类器和微结构分类器，并基于两者的预测值和相关对象模型特征进一步训练，从而形成堆叠分类器.为了评估该方法，基于该方法开发了一个原型工具OOSdpd.该工具从Java字节码级别的系统实现中抽取设计模式实例，并在JUnit等几个经典的开源项目上进行实验.通过与现有的两种工具进行对比分析，实验验证了该方法在提高设计模式识别准确率及召回率方面的有效性.

摘要:作为社会媒体文本情感分析的重要研究课题之一，跨领域文本情感分类旨在利用源领域资源或模型迁移地服务于目标领域的文本情感分类任务，其可以有效缓解目标领域中带标签数据不足问题.从3个角度对跨领域文本情感分类方法行了归纳总结：（1）按照目标领域中是否有带标签数据，可分为直推式和归纳式情感迁移方法；（2）按照不同情感适应性策略，可分为实例迁移方法、特征迁移方法、模型迁移方法、基于词典的方法、联合情感主题方法以及图模型方法等；（3）按照可用源领域个数，可分为单源和多源跨领域文本情感分类方法.此外，还介绍了深度迁移学习方法及其在跨领域文本情感分类的最新应用成果.最后，围绕跨领域文本情感分类面临的关键技术问题，对可能的突破方向进行了展望.

摘要:近年来，随着深度学习的广泛应用，唇语识别技术也取得了快速的发展.与传统的方法不同，在基于深度学习的唇语识别模型中，通常包含使用神经网络对图像进行特征提取和特征理解两个部分.根据中文唇语识别的特点，将识别过程划分为两个阶段——图片到拼音（P2P）以及拼音到汉字（P2CC）的识别.分别设计两个不同子网络针对不同的识别过程，当两个子网络训练好后，再把它们放在一起进行端到端的整体架构优化.由于目前没有可用的中文唇语数据集，因此采用半自动化的方法从CCTV官网上收集了6个月20.95GB的中文唇语数据集CCTVDS，共包含14 975个样本.此外，额外采集了269 558条拼音汉字样本数据对拼音到汉字识别模块进行预训练.在CCTVDS数据集上的实验结果表明，所提出的ChLipNet可分别达到45.7%的句子识别准确率和58.5%的拼音序列识别准确率.此外，ChLipNet不仅可以加速训练、减少过拟合，并且能够克服汉语识别中的歧义模糊性.

摘要:近年来，随着信息技术的发展及物联网技术的兴起，出现了越来越多的持续监控应用场景，如智能交通实时监控、疾病实时监控、智能基础设施应用等.在这些场景中，如何对参与者持续分享的数据进行隐私保护面临重大挑战.差分隐私是一种严格和可证明的隐私定义，早期差分隐私研究大都基于一个大规模、静态的数据集做一次性的计算和发布.而持续监控下差分隐私保护需对动态数据做持续计算和发布.目前，持续监控下差分隐私保护是差分隐私领域新的研究热点之一.对持续监控下差分隐私保护的已有研究成果进行总结.首先，对该场景下差分隐私保护模型进行阐述；然后，重点介绍了持续监控下满足event级、user级和w-event级隐私保护的实现方案.在对已有研究成果深入对比分析的基础上，指出了持续监控下差分隐私保护的未来研究方向.

摘要:移动社交网络（mobile social network，简称MSN）利用移动用户之间的社交关系，通过节点间的协作式转发实现消息交付.然而，随着大数据时代的到来，MSN需要满足移动用户日益增长的对内容（如视频）的需求.由于信息中心网络（information-centric networking，简称ICN）对移动性的支持，基于ICN架构，提出了一种MSN中基于社区划分的路由机制.在兴趣决策中，利用节点请求中的内容名字获取用户的兴趣偏好，进而计算用户间的兴趣差异度量；根据兴趣差异将节点划分为兴趣社区，依据这些兴趣社区进行兴趣包路由.在数据决策中，根据节点历史相遇信息计算用户间的相遇规律度量，根据相遇规律将节点划分为社交社区，依据这些社交社区进行数据包路由.同时，根据兴趣社区和社交社区信息优化节点的内容缓存，以快速满足未来的内容请求.进行了仿真实验，通过与现有机制在包交付率、平均延迟、平均跳数和网络开销方面的性能对比，表明所提出的机制是可行且有效的.

摘要:针对Ad Hoc网络路由发现过程中广播路由请求分组导致的广播风暴问题，提出了一种基于节点度估计和静态博弈转发策略的Ad Hoc网络路由协议NGRP.NGRP考虑边界影响，采用分段函数的思想将网络场景分为中心、边和角区域，分别估算网络中节点在不同区域的节点度，避免了周期性广播Hello消息获取节点度导致的开销；NGRP路由请求分组的转发采用静态博弈转发策略，利用节点度估算参与转发路由请求分组的节点数量，将转发和不转发作为策略集合，设计效益函数，通过纳什均衡获得节点转发路由请求分组的转发概率，从而减少了路由请求分组广播过程中产生的大量的冗余、竞争和冲突，提高了路由发现过程中路由请求分组的广播效率.运用NS-2对协议的性能进行大量的仿真，结果表明：NGRP的分组投递率、路由开销、MAC层路由开销和吞吐率这4项指标明显优于AODV+FDG，AODV with Hello和AODV without Hello协议.

摘要:现有的密文策略基于属性加密CP-ABE（ciphertext-policy attribute-based encryption）算法普遍在解密时存在计算量过大、计算时间过长的问题，该问题造成CP-ABE难以应用和实施.针对该问题，将计算外包引入到方案的设计之中，提出一种面向公有云的基于Spark大数据平台的CP-ABE快速解密方案.在该方案中，专门根据CP-ABE的解密特点设计了解密并行化算法；利用并行化算法，将计算量较大的叶子节点解密和根节点解密并行化；之后，将并行化任务交给Spark集群进行处理.计算外包使得绝大多数解密工作由云服务器完成，用户客户端只需进行一次指数运算；而并行化处理则提高了解密速度.安全性分析表明，所提出的方案在一般群模型和随机预言模型下能对抗选择明文攻击.

摘要:MORUS算法是Wu等人设计的认证加密算法，现已进入CAESAR竞赛的第三轮.动态立方攻击是Dinur等人2011年提出的针对迭代型序列密码的分析方法.提出了一种改进的动态立方攻击方法，优化了动态立方攻击的立方集合的选取规则，提出了优先猜测关键值并恢复相应的关键秘密信息的方法，据此给出了成功率更高的秘密信息恢复方法.利用该方法分析了初始化5步的简化版MORUS算法，最终以O（2^95.05）的复杂度恢复所有128比特密钥，攻击的成功率大于92%.

摘要:云渲染技术已被广泛应用于影视和动漫等行业.与传统的渲染农场和租赁市场模式不同，云渲染系统依托云计算基础设施提供多种软件服务进行渲染作业的方式，正逐渐成为新兴的计算模式.由于任务执行和资源操作等作业调度对于用户而言是透明的，这要求云渲染系统应具备智能化以实现计算资源优化调度和多端任务管理，并对系统可靠性提出了更高要求.针对这一问题，提出了采用概率模型检验对云渲染系统任务调度进行定量评估.首先，考虑渲染服务失效等因素引发的随机系统异常和指令错误，如文件损坏和渲染任务超时等，提出了基于离散马尔可夫链（DTMC）的概率模型对云渲染系统的文件准备模块、资源请求模块、渲染任务执行模块进行形式化建模；其次，从服务质量属性角度提出了9类验证性质用于定义云渲染系统的可靠性，采用概率计算树逻辑（PCTL）描述检验性质公式并执行工具PRISM计算和验证渲染系统可靠性；最后，结合案例和实验证明了该方法的可行性和有效性，尤其是对改进前后云渲染系统进行定量检验，可用于指导如何进行失效恢复和任务切换.因此，该方法在一定程度上可提高云渲染系统的可靠性.

摘要:云计算已成为大数据分析作业的主流运行支撑环境，选择合适的云资源优化其性能面临巨大挑战.当前研究主要考虑大数据分析框架（如Hadoop，Spark等）的多样性，采用机器学习方法进行资源供给，但样本少容易陷入局部最优解.提出了大数据环境下基于负载分类的启发式云资源供给方法RP-CH，基于云资源共享特点，获取其他大数据分析作业的运行时监测和云资源配置信息，建立负载分类与优化云资源配置的启发式规则，并将该规则作用到贝叶斯优化算法的收益函数.基于HiBench，SparkBench测试基准的结果显示：RP-CH相对于已有方法CherryPick、大数据分析作业的性能平均提升了58%，成本平均减少了44%.

摘要:容器将应用和支持软件、库文件等封装为镜像，通过发布新版本镜像实现应用升级，导致不同版本之间存在大量相同数据.镜像加载消耗大量时间，使容器启动时间从毫秒级延迟为秒级甚至是分钟级.复用不同版本之间的相同数据，有利于减少容器加载时间.当前，容器镜像采用继承和分层加载机制，有效实现了支持软件、库文件等数据的复用，但对于应用内部数据还没有一种可靠的复用机制.提出一种基于分片复用的多版本容器镜像加载方法，通过复用不同版本镜像之间的相同数据，提升镜像加载效率.方法的核心思想是：利用边界匹配数据块切分方法将容器镜像切分为细粒度数据块，将数据块哈希值作为唯一标识指纹，借助B-树搜索重复指纹判断重复数据块，减少数据传输.实验结果表明，该方法可以提高5.8X以上容器镜像加载速度.

摘要:云计算和移动互联网的不断融合，促进了移动云计算的产生和发展，但是其难以满足终端应用对带宽和延迟的需求.移动边缘计算在靠近用户的网络边缘提供计算和存储能力，通过计算卸载，将终端任务迁移至边缘服务器上面执行，能够有效降低应用延迟和节约终端能耗.然而，目前针对移动边缘环境任务卸载的主要工作大多考虑单个移动终端和边缘服务器资源无限的场景，这在实际应用中存在一定的局限性.因此，针对边缘服务器资源受限下的任务卸载问题，提出了一种面向多用户的串行任务动态卸载策略（multi-user serial task dynamic offloading strategy，简称MSTDOS）.该策略以应用的完成时间和移动终端的能量消耗作为评价指标，遵循先来先服务的原则，采用化学反应优化算法求解，充分考虑多用户请求对服务器资源的竞争关系，动态调整选择策略，为应用做出近似最优的卸载决策.仿真结果表明，MSTDOS策略比已有算法能够取得更好的应用性能.

摘要:近来出现诸多以非易失性存储器（non-volatile memory，简称NVM）作为存储设备的新型持久化内存文件系统，充分发掘NVM的低延迟和可按字节寻址等优点，优化文件访问的I/O栈和一致性机制，极大提升文件系统的性能.然而，现有持久化内存文件系统都没有考虑NVM写耐受度低的缺陷，极易导致NVM被磨损穿（wear out）.针对NVM写耐受度低的缺点，探索多种利用基本文件操作对NVM造成磨损攻击的方式，并在真实持久化内存文件系统PMFS中以实验证明磨损攻击的严重性.为有效防御针对NVM的磨损攻击，提出了持久化内存文件系统磨损防御机制（persistent in-memory file system wear defense technique，简称PFWD），包括索引节点元数据虚拟化技术、超级块迁移技术、文件数据页磨损均衡技术和文件索引结构迁移技术，保护文件系统中所有可能被磨损攻击利用的数据结构.实验结果证明所提出的PFWD技术能有效地防御病毒发动对NVM的磨损攻击，提高了存储系统的稳定性.