基于SHML的CPS行为建模及仿真

信息物理融合系统（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的建模及仿真提供了一种有效的方法及工具支撑.     

基于AADL的CPS系统分析与设计

信息物理融合系统CPS(Cyber Physical System)的建模需要融合离散计算实体与连续物理实体,而传统的建模方法却是分别对两者进行建模,缺乏对两者相互融合的抽象。针对这种情况,利用结构分析与设计语言AADL(Architectural Analysis and Design Language)在基于模型开发上的优势,对AADL所不能支持的时空、行为、动态连续等方面进行扩展,通过比较现有元胞自动机、Modelica与AADL的区别与关联后,提出相应的变换公式将两者用AADL的形式表达。以车联网CPS系统为案例,详细描述系统的组成与建模过程,并对该模型在系统体系结构、端到端的流延迟等方面进行分析验证,证实该方案的可行性与正确性。     

面向领域的软件系统构造与质量保障专题前言

软件是推动新一代信息技术发展的驱动力.随着互联网、云计算、人工智能等技术的快速发展,软件与物联网、区块链、自动驾驶等众多领域的融合进一步加强,正引领并促进这些领域向数字化、智能化发展,为社会、经济的加速演进和创新发展带来了新的契机.因此,面向领域的软件技术不仅是软件领域,也是众多其他领域国内外学者的关注焦点和研究重点.与传统的软件系统相比,面向领域的软件系统(简称领域软件)带来了研究与应用上的新挑战.面对领域软件的特点和需求,如何有效地构造领域软件,实现领域应用的软件定义与智能化,如何通过验证、分析、测试等多种手段严格保障系统控制行为的正确性、实时性、协同性等重要质量特性,是一个重大挑战. 本专题采取自由投稿的方式,共收到37篇投稿,其中36篇通过了形式审查.特约编辑邀请了30位领域专家参与审稿,每篇稿件至少邀请2位专家进行评审,每篇稿件都经过两轮审稿.共计16篇稿件通过第1轮评审,并在CCF软件工程专业委员会、系统软件专业委员会、形式化方法专业委员会年会2020 CCF中国软件大会(Chinasoft)上进行了报告.经过第2轮终审,最终有10篇论文入选本专题.其中, 　　论文“基于反例确认的CPS不确定性模型校准”研究了CPS中不确定性模型的准确性问题,提出了一种基于反例确认的校准方法以提高不确定性模型的准确度并精化CPS系统模型的验证结果. 　　论文“安全关键异构软件混合建模及代码生成方法”提出了一种AADL和SDL的混合建模方法,支持以自底向上的方式对安全关键软件系统进行混合建模,并给出了面向多核处理器平台的代码自动生成方法. 　　论文“基于环境建模的物联网系统TAP规则生成方法”提出了一种基于环境建模的TAP规则生成方法,自动地基于环境模型从服务需求中推导系统行为,检测系统行为的完整性与一致性,并最后转换为TAP规则. 　　论文“区块链赋能的高效物联网数据激励共享方案”提出了一个高效的区块链物联网数据激励共享框架,利用分片技术构建能够并行处理数据共享交易的异步共识区,并在云/边缘服务器和分片异步共识区上部署高效的共识机制,从而提高数据共享交易的处理效率. 　　论文“时空轨迹数据驱动的自动驾驶场景元建模方法”提出一种面向自动驾驶领域的时空轨迹数据元建模方法以实现数据的统一、处理与重用,并基于自动驾驶安全场景建模语言ADSML讨论了如何使用ADSML实现场景实例化. 　　论文“基于深度学习的混合模糊测试方法”提出了一个基于深度学习将符号执行与模糊测试相结合的混合测试方法,并实现了相应的混合测试工具SmartFuSE. 　　论文“一种结构信息增强的代码修改自动转换方法”基于深度学习提出了一种结构信息增强的代码修改自动转换方法,增强了模型对代码的结构信息和依赖信息的捕获能力,从而提升了代码修改自动转换的准确性. 　　论文“融合代码与文档的软件功能特征挖掘方法”提出了一种融合代码与文档的软件功能特征挖掘方法.通过迭代挖掘软件源代码和以Stack Overflow讨论帖为代表的软件文档,自动提取开源软件的功能特征描述,并构造层次化的软件功能特征视图. 　　论文“基于偶然正确性概率的错误定位技术”通过对基于代码覆盖的错误定位技术中可疑度的计算方法进行修正,提出了一种错误定位技术,以消除偶然正确性现象对错误定位技术的影响. 　　论文“面向神经机器翻译系统的多粒度蜕变测试”提出了一种基于蜕变测试的多粒度测试框架,用于在没有参考译文的情况下评估神经机器翻译系统的翻译质量及其翻译鲁棒性. 　　本专题面向领域软件的研究人员和工程人员,内容涵盖领域软件的需求分析、设计与建模、开发与构造、测试与验证等领域,反映了我国学者在相关领域的高水平研究成果.感谢《软件学报》编委会、CCF软件工程专委会、系统软件专委会、形式化方法专委会对专题工作的指导和帮助,感谢专题全体评审专家及时、耐心、细致的评审工作,感谢踊跃投稿的所有作者.希望本专题能够对领域软件的科研工作有所促进.     

面向CPS时空性质验证的混成AADL建模与模型转换方法

随着信息物理融合系统CPS(cyber physical system)研究的深入,CPS的安全性问题越来越受到人们的广泛关注,如何验证CPS时空不一致的安全性问题已经成为研究热点.针对该问题,提出了面向CPS时空性质验证的混成AADL(architecture analysis&design language)建模与...     

面向CPS系统仿真的建模方法研究与设计

CPS仿真建模在构建CPS系统时具有重要意义,不仅能够在系统开发过程中对系统进行验证和测试,而且是模型驱动开发中的重要环节。CPS系统通过精化和提炼可分为物理实体和计算实体,采用具有动态连续性、基于时间的运动状态行为模型构建物理实体;计算实体模型则采用基于有限状态机的离散系统行为模型进行构建。通过面向时间的状态精化对两种行为模型进行扩展,将两种扩展模型进行融合,完成CPS系统的建模仿真。分析了构建计算实体模型的统一建模语言(UML)以及构建物理实体模型的simulink/RTW建模工具的可行性,提出了基于UML框架的两种异质模型融合方法。     

信息-物理融合系统动态行为模型构建方法

信息-物理融合系统(Cyber-Physical System,CPS)特有的计算、通信、控制的联合动态性,计算与物理的多尺度融合性,系统环境及状态的时空交互性以及系统动态行为的非确定性,不但使面向CPS的模型驱动设计与验证方法在CPS系统设计中更为重要,而且也向其提出了新的技术挑战.论文在结合典型实例分析CPS系统特征及其模型构建具体挑战的基础上,研究并总结了CPS动态行为建模的主要方法:一体化建模方法从CPS系统层面描述计算过程与物理过程的交互与融合;时空交互建模方法关注CPS系统行为与时间及空间关系的语义表示;功能和实现兼容建模方法侧重刻画CPS系统的逻辑设计和物理实现的映射与支撑;而集成建模方法则重点解决多异构模型的交互方式与语义的一致表达.论文基于多异构实体的CPS系统建模框架,提出了一种CPS系统结构与动态行为的协同建模方法,并用CPS-ADL对其进行了实现和验证.     

泛在嵌入式智能系统专题前言

目前,世界范围的科技革命和产业变革正在孕育兴起,一些重要科学问题和关键核心技术正在呈现革命性的突破先兆.同时,“万物智联”时代正在加速到来,IOT/CPS、AIOT 等蓬勃发展,以泛在感知、泛在互联、泛在智能为特征的各类智慧系统,以嵌入式系统为基础,与大数据、区块链、云计算呈现融合发展趋势.随着人工智能技术和嵌入式AI 芯片技术的发展,人工智能已经开始逐步向嵌入式系统迁移,尤其是伴随着机器人、无人机、无人车等智能设备的技术成熟,越来越多的应用系统需要在以边缘计算为主的嵌入式系统上实现.目前,嵌入式系统应用前景愈发广阔,如5G 通信、智能制造、智能电网、智能交通、国防军事、航空航天、智能网联汽车、数字医疗设备、机器人、智慧家庭、智能建筑等产业的创新发展都与嵌入式系统的技术发展息息相关. 本专题采取定向邀请和自由投稿相结合的方式,共收到 9 篇投稿,其中 8 篇通过了形式审查.特约编辑邀请了13 位领域专家参与审稿,每篇稿件至少邀请2 位专家进行评审,每篇稿件都经过2 轮审稿.共计6 篇稿件通过第1 轮评审,并在CCF 形式化方法专委会年度会议上进行了报告.经过第2 轮终审,最终有6 篇论文入选本专题.     

基于AADL的失效概率分配及安全性评估方法

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

智慧物理系统及其建模与仿真框架

智慧物理系统(cPs)是一个综合计算、通讯和控制的多维复杂系统.首先分析了智慧物理系统的特点以及对现有分布式建模与仿真技术的挑战,进而提出了一种扩展的HLA建模与仿真框架.讨论了四方面新技术,即基于MDA的建模技术,基于协同本体的知识融合技术,资源管理联邦技术,以及互配RTI技术.该框架将目前的HLA的单层结构扩展为双层结构,即资源联邦层与应用联邦层.它实现了基于MDA实现CPS的语义建模,支持多联邦的协同并发运行,以松耦合集成的方式实现大规模、异构CPS的建模与仿真.     

基于AADL的电网信息物理系统分层建模

信息物理融合系统（cyber-physical system, CPS）旨在通过物理与信息系统的深度融合,从而提升系统的性能与运行效率。随着信息通信技术广泛应用于电力网,大量的传感设备配置与电网一次设备上,电网系统的信息与物理的耦合关系越为明显,由此电网信息物理融合系统（grid cyber-physical system, GCPS）便出现了;本文首先介绍电网信息融合系统的概念;基于GCPS的特性提出三层模型,使用体系结构分析和设计语言（architecture analysis and design language, AADL）对GCPS进行分析与建模,并对该模型的决策控制子进程构件进行端对端流延迟分析,证实该方案的可行性与正确性。     

AADL模型的形式化研究

在嵌入式系统建模领域,AADL以其软硬件协同建模的特点已经逐渐成为业界的标准。围绕AADL的形式化特点,国内外众多学者展开了热烈的讨论。为了帮助系统开发人员深入了解AADL,指导软件开发进程,提高基于AADL模型的软件开发效率,分别从AADL模型可靠性分析、可调度性分析以及AADL模型测试这三个不同角度综述了已经出现的各种AADL形式化验证理论,对比分析了它们的优点和不足。简要介绍有关AADL验证工具,研究基于AADL模型的嵌入式开发平台的构建。     

ARINC653航空电子系统AADL建模技术研究

随着ARINC653系统在我国航空领域的广泛应用,研究ARINC653系统建模方法将为进一步研究基于模型的ARINC653系统可靠性、可调度性分析奠定基础.详细研究了ARINC653系统AADL建模的方法,具体描述了ARINC653系统、分区、进程、进程通信和健康监控等核心元素的AADL建模映射机制,并进行实例说明.     

基于多模态进化Rao-Blackwellized 粒子滤波器的 移动机器人航迹推算系统的故障诊断

针对一类移动机器人航迹推算系统的故障诊断问题, 提出一种多模态进化Rao-Blackwellized 粒子滤波
器(MERBPF) 算法. 为解决由粒子贫乏引起的不一致性问题, 采用交叉与变异种群策略优化, 根据粒子多样性加入扰
动因子. 利用专家规则判定机器人运动状态所对应的MERBPF, 构造复杂逻辑表述方法. 仿真实验结果表明: 在强过
程噪声下, MERBPF 仍具有较高的鲁棒性, 提高了诊断机器人航迹推算系统的准确率.

     

AADL模型的形式化研究

在嵌入式系统建模领域,AADL以其软硬件协同建模的特点已经逐渐成为业界的标准。围绕AADL的形式化特点,国内外众多学者展开了热烈的讨论。为了帮助系统开发人员深入了解AADL,指导软件开发进程,提高基于AADL模型的软件开发效率,分别从AADL模型可靠性分析、可调度性分析以及AADL模型测试这三个不同角度综述了已经出现的各种AADL形式化验证理论,对比分析了它们的优点和不足。简要介绍有关AADL验证工具,研究基于AADL模型的嵌入式开发平台的构建。     

面向服务的信息物理融合系统建模与验证

针对信息物理融合系统(CPS)中建模与验证面临的问题与挑战,基于服务组合的思想,提出一种CPS建模与验证方法。首先,综合分析已有研究成果,提出一种CPS的组成结构,包含物理世界、感知系统、信息处理系统、控制系统及时间约束。基于该结构提出CPS资源的服务分类及组成框架,并利用时间自动机理论,提出CPS物理环境建模方法、CPS原子服务建模方法及服务组合方法。最后,通过案例设计和模型检测工具Uppaal,分别对系统安全性、可达性、活性及时间约束四种类型的性质进行了相关验证。结果表明,系统通过了这些性质的验证,这也证明了面向服务的CPS建模方法的正确性。     

嵌入式软件系统体系结构可靠性分析方法

AADL是嵌入式领域对SA进行建模、评估的常用方法,但其属于一种半形式化开发语言,无法直接对SA的可靠性进行验证。为此,提出一种基于AADL的可靠性分析框架,对SA的可靠性进行形式化验证。首先通过分析系统体系结构的元素关系,建立AADL可靠性模型;然后设计转换模型及其规则,将AADL模型转换为连续时间马尔科夫链模型;最后采用概率模型检验工具对连续时间马尔科夫链模型进行可靠性定量分析。仿真结果表明,与现有可靠性分析方法相比,该方法在计算效率和转换效率上都有明显的提高。基于AADL的可靠性分析框架实现在软件系统开发早期对SA进行可靠性定量计算,为AADL在嵌入式软件系统可靠性定量分析方面提供了一种新的验证思路。     

基于体系结构模型的综合化航电分区可调度性验证

分区可调度性验证是影响综合模块化航电系统(IMA)可靠性与安全性的关键问题。为解决现有的模型驱动验证方法难以满足系统整体验证需求或需要繁琐的二次建模的问题,提出一种基于体系结构分析与设计语言(AADL)的IMA分区可调度性验证建模方法。在构建分区静态体系结构模型的基础上,通过AADL行为附件建模描述系统中任务的调度过程。再采用AADL Inspector工具对模型中的任务调度行为进行动态仿真,根据仿真结果即可对IMA分区可调度性进行评估。案例实验表明,该方法能够有效发现分区调度配置信息中的错误。此外,只需一次性建模即可直接完成可调度性验证。与现有方法相比,避免了对AADL模型进行繁琐的二次转化。     

基于异构模型融合的CPS系统仿真建模方法研究

单一的离散系统仿真或连续系统仿真已无法满足复杂的CPS系统仿真需求。结合CPS一体化模型的3类 实体,对计算实体构建基于事件驱动的离散事件仿真模型(UML模型),对物理实体构建基于动态连续时间坐标的连 续时间仿真模型(Simulink模型),并以刻画计算实体和物理实体的交互接口和行为特征为目的,进行协同仿真,构建 交互实体模型。给出并分析了UM工丫Simulink协同建模的优点,研究并分析了3种不同的模型融合方法,结合无人机 模型,从模型级对CPS一体化模型的融合进行了分析设计。     

信息物理融合系统网络安全综述

信息物理融合系统（cyber-physical systems， CPS）是集计算、通信和控制于一体的智能系统，实现网络和物理的深度协作和有机融合.目前CPS在关键的基础设施、政府机构等领域发挥着越来越重要的作用.由于物理限制，计算机和网络产生的安全漏洞会导致CPS遭受巨大的破坏，同时还会引起经济损失、社会动乱等连锁反应，所以研究CPS的安全问题对于确保系统安全运行具有重要意义.本文结合国内外的研究现状，概述了CPS安全控制和攻击检测的最新进展.首先本文总结了CPS典型的系统建模以满足对系统性能分析的需要.然后介绍了3种典型的网络攻击，即拒绝服务攻击、重放攻击和欺骗攻击.根据检测方法的类别，对CPS攻击检测的发展进行的概述.此外还讨论了系统的安全控制和状态估计.最后总结和展望了CPS网络安全面临的挑战和未来的研究方向.     

AADL建模工具的设计

设计一种架构分析与设计语言(AADL)建模工具,便于用户建立AADL模型.基于模型驱动体系结构思想,在Eclipse插件开发平台上开发可扩展的插件集合AADL模型设计工具.用户根据该工具建立的嵌入式系统AADL架构模型,通过XML文档保存,分析与验证工具以第三方插件的形式集成到该工具中,提取系统的AADL架构模型.通过应用实例验证了该工具的有效性.