检索结果-内蒙古大学图书馆

计算机工程 2021年第8期47卷 284-293,300页

作者：闫倩倩缪炜恺华东师范大学上海市高可信计算重点实验室上海200062

针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供... 详细信息

针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供模板。在对需求的确认和验证中,根据形式化规范建立需求模型,导出相关图表,基于此检查领域专家关注的场景。同时制定场景描述规则,使场景可以在需求模型中正确执行。在此基础上,从特殊变量、效率、场景质量三方面对场景进行优化,更充分地验证需求的正确性。实验结果表明,对于典型车载控制软件,该方法较传统分析方法可多探测到10%的潜在缺陷,效率提升80%以上。

关键词：形式化方法需求规约需求确认和验证场景优化轨道交通控制软件

来源：评论

学校读者我要写书评

暂无评论

时空轨迹数据驱动的自动驾驶场景元建模方法

引用

软件学报 2021年第4期32卷 973-987页

作者：张梦寒杜德慧张铭茁张雷王耀周文韬华东师范大学软件工程学院上海200062 上海市高可信重点实验室(华东师范大学) 上海200062 教育部可信软件国际合作联合实验室(华东师范大学) 上海200062 同济大学上海自主智能无人系统科学中心上海201210

时空轨迹数据驱动的汽车自动驾驶场景建模,是当前汽车自动驾驶领域中驾驶场景建模、仿真所面临的关键问题,对于提高系统的安全性具有重要的研究意义.近年来,随着时空轨迹数据建模及应用研究的快速发展,时空轨迹数据应用于特定领域建模... 详细信息

时空轨迹数据驱动的汽车自动驾驶场景建模,是当前汽车自动驾驶领域中驾驶场景建模、仿真所面临的关键问题,对于提高系统的安全性具有重要的研究意义.近年来,随着时空轨迹数据建模及应用研究的快速发展,时空轨迹数据应用于特定领域建模的研究引起人们的广泛关注.但是,由于时空轨迹数据所反映的现实世界的多元性和复杂性以及时空轨迹数据的海量、异构、动态等特点,基于时空轨迹数据驱动的安全攸关场景建模的研究仍面临着挑战,包括:统一的时空轨迹数据元模型、基于时空轨迹数据的元建模方法、基于数据分析技术的时空轨迹数据处理、数据质量评价等.针对汽车自动驾驶领域的场景建模需求,提出一种基于MOF元建模体系构建时空轨迹数据的元建模方法,根据时空轨迹数据的特征及自动驾驶的领域知识,构建了面向汽车自动驾驶的时空轨迹数据元模型;基于此,提出基于时空轨迹数据元建模技术体系的自动驾驶安全场景建模方法,并使用场景建模语言ADSML实例化安全场景,构建安全场景库,旨在为此类系统的安全关键场景建模提供一种可行的方案.结合变道超车场景的案例,展示了时空轨迹数据驱动的自动驾驶安全场景元建模方法的可用性,为场景模型的构建、仿真、分析奠定了基础.

关键词：时空轨迹数据时空轨迹数据元模型领域建模 MOF元建模汽车自动驾驶的场景建模

来源：评论

学校读者我要写书评

暂无评论

基于环境建模的物联网系统TAP规则生成方法

引用

软件学报 2021年第4期32卷 934-952页

作者：边寒陈小红金芝张民上海市高可信计算重点实验室(华东师范大学) 上海200062 北京大学信息科学技术学院计算机科学与技术系北京100871 高可信软件技术教育部重点实验室(北京大学) 北京100871

用户需求是物联网智能服务的根本驱动力,如IFTTT等很多物联网框架允许用户使用简单的触发-命令编程(TAP)规则进行编程,但它们描述的是设备调度程序,并不是用户服务需求.一些物联网系统提出采用面向目标的需求方法,支持服务目标的分解,... 详细信息

用户需求是物联网智能服务的根本驱动力,如IFTTT等很多物联网框架允许用户使用简单的触发-命令编程(TAP)规则进行编程,但它们描述的是设备调度程序,并不是用户服务需求.一些物联网系统提出采用面向目标的需求方法,支持服务目标的分解,但很难保证物联网不同服务间的一致性和服务部署的完整性.为了支持正确的"用户编程"并保证用户服务需求的一致性与完整性,提出了基于环境建模的TAP规则自动生成方法,在用户提供的服务需求的基础上,根据环境模型自动推导出所需的系统行为,以检测系统行为的一致性和完整性,并最终自动生成TAP规则,实现从用户服务需求到物联网设备调度的自动生成.构建了物联网应用场景的环境本体以建模环境,并定义了基于环境本体的服务需求的描述方法.另外,针对方法的准确性、效率、性能以及构建环境本体的时间开销,在智能家居场景上进行了评估.结果表明,所提方法的准确性、效率和性能均超过可用阈值,且在需求达到一定数量后,构建环境本体花费的时间可忽略不计.

关键词：物联网系统用户服务需求需求一致性需求完整性环境建模

来源：评论

学校读者我要写书评

暂无评论

基于Coq的Paxos形式化建模与验证

引用

软件学报 2020年第8期31卷 2362-2374页

作者：李亚男邓玉欣刘静上海市高可信计算重点实验室(华东师范大学) 上海200062

Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在... 详细信息

Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在定理证明工具Coq中,形式化描述和定义了Lamport的Basic Paxos算法,并且证明了其满足共识性.

关键词：分布式系统 Basic Paxos 定理证明工具 Coq 验证

来源：评论

学校读者我要写书评

暂无评论

星载嵌入式软件全数字仿真开发验证平台

引用

计算机测量与控制 2024年第5期32卷 302-311页

作者：王赛亚吴小明邓玉欣华东师范大学上海市高可信计算重点实验室上海200062 北京控制工程研究所北京100190

为了应对当前航天器软件功能日趋复杂与软件研制周期短、对软件可靠性和安全性要求高的矛盾,同时为了满足国产化自主可控的需求,在国产Linux操作系统下,以QEMU的SPARC V8指令集模拟器为基础,解决了SOC2012片内外设与A6017仿真等关键问题... 详细信息

为了应对当前航天器软件功能日趋复杂与软件研制周期短、对软件可靠性和安全性要求高的矛盾,同时为了满足国产化自主可控的需求,在国产Linux操作系统下,以QEMU的SPARC V8指令集模拟器为基础,解决了SOC2012片内外设与A6017仿真等关键问题,搭建了一种星载嵌入式软件全数字仿真开发验证平台;提出了通过共享内存解决方案,提高QEMU指令集仿真内核对外围IO空间读写仿真效率;该平台已经用于某卫星型号控制分系统软件和星务软件测试,相较于基于硬件的测试平台,该平台具有更好的可重用性和快速搭建性,能够大大降低硬件测试的风险和成本,同时具备更强的可控性以及更丰富的调试和测试手段。

关键词： Linux QEMU SPARC V8 SOC2012 嵌入式软件全数字仿真

来源：评论

学校读者我要写书评

暂无评论

利用特征融合和整体多样性提升单模型鲁棒性

引用

软件学报 2020年第9期31卷 2756-2769页

作者：韦璠宋云飞邵明莉刘天陈小红王祥丰陈铭松上海市高可信计算重点实验室(华东师范大学) 上海200062

使用深度神经网络处理物联网设备的急剧增加产生的海量图像数据是大势所趋,但由于深度神经网络对于对抗样本的脆弱性,它容易受到攻击而危及物联网的安全.所以,如何提高模型的鲁棒性,就成了一个非常重要的课题.通常情况下,组合模型的防... 详细信息

使用深度神经网络处理物联网设备的急剧增加产生的海量图像数据是大势所趋,但由于深度神经网络对于对抗样本的脆弱性,它容易受到攻击而危及物联网的安全.所以,如何提高模型的鲁棒性,就成了一个非常重要的课题.通常情况下,组合模型的防御表现要优于单模型防御方法,但物联网设备有限的计算能力使得组合模型难以应用.为此,提出一种在单模型上实现组合模型防御效果的模型改造及训练方法:在基础模型上添加额外的分支;使用特征金字塔对分支进行特征融合;引入整体多样性计算辅助训练.通过在MNIST和CIFAR-10这两个图像分类领域最常用的数据集上的实验表明,该方法能够显著提高模型的鲁棒性.在FGSM等4种基于梯度的攻击下的分类正确率有5倍以上的提高,在JSMA,C&W以及EAD攻击下的分类正确率可达到原模型的10倍.同时,不干扰模型对干净样本的分类精度,也可与对抗训练方法联合使用获得更好的防御效果.

关键词：物联网特征融合整体多样性模型防御鲁棒性对抗样本

来源：评论

学校读者我要写书评

暂无评论

基于双通道R-FCN的图像篡改检测模型

引用

计算机学报 2021年第2期44卷 370-383页

作者：田秀霞李华强张琴周傲英上海电力大学计算机科学与技术学院国网兰州供电公司互联网部信息通信安全实验室华东师范大学数据科学与工程研究院华东师范大学软件学院上海市高可信计算重点实验室

随着大数据时代的到来和图像编辑软件的发展,恶意篡改图片的数量出现井喷式增长,为了确保图像的真实性,众多学者基于深度学习和图像处理技术提出了多种图像篡改检测算法.然而,当前提出的绝大多数方法在面对大量图片的情况下,篡改检测速... 详细信息

随着大数据时代的到来和图像编辑软件的发展,恶意篡改图片的数量出现井喷式增长,为了确保图像的真实性,众多学者基于深度学习和图像处理技术提出了多种图像篡改检测算法.然而,当前提出的绝大多数方法在面对大量图片的情况下,篡改检测速率较低且小面积篡改区域检测效果较差.为了有效解决这些问题,本文首次将基于区域的全卷积网络(Region-based Fully Convolutional Networks,R-FCN)引入双通道篡改检测网络,通过彩色图像通道提取图像的表层特征,使用隐写分析通道挖掘图像内部的统计特征,并利用双线性池化层将两个通道的信息融合,构建了一种面向实际应用场景的图像篡改检测模型.其中,利用R-FCN中位置敏感得分图提高图像篡改检测效率,使用双线性插值算法提高小面积篡改区域的检测率.通过在国际主流的标准图像篡改数据集上进行实验,有效地验证了该模型的图像篡改检测速率相比当前最新模型提高2.25倍,检测精度提升1.13%到3.21%,本文提出的模型是一种更加高效而精准的图像篡改检测模型.

关键词：图像篡改检测深度学习双通道网络基于区域的全卷积网络双线性插值

来源：评论

学校读者我要写书评

暂无评论

一种面向ADS的模型驱动式逻辑场景建模及仿真方法

引用

中国汽车 2023年第8期 50-57页

作者：周文韬郑成行万宜萱杜德慧华东师范大学软件工程学院上海200062 上海市高可信重点实验室(华东师范大学) 上海200062 教育部可信软件国际合作联合实验室(华东师范大学) 上海200062

汽车自动驾驶的场景建模及仿真分析是确保自动驾驶系统安全性的关键,对于提高整个系统的安全性至关重要,已经引起工业界和学术界的广泛关注。场景建模是场景仿真、测试、验证分析的基础,能够有效帮助发现场景中存在的危险,是自动驾驶系... 详细信息

汽车自动驾驶的场景建模及仿真分析是确保自动驾驶系统安全性的关键,对于提高整个系统的安全性至关重要,已经引起工业界和学术界的广泛关注。场景建模是场景仿真、测试、验证分析的基础,能够有效帮助发现场景中存在的危险,是自动驾驶系统设计开发面临的挑战性问题之一。然而,现有的场景模型生成方法,主要采用数据驱动式,结合路采数据和数字孪生技术构建具体场景,无法有效应对ADS场景复杂、类型多样、测试效率不高的问题。同时,为了提高场景的覆盖率,迫切需要从逻辑场景的层次设计一种可视化的场景建模语言,可用于构建逻辑场景,并具有丰富的语义模型,能够支持逻辑场景的测试及验证分析。针对以上问题,我们提出一种模型驱动式场景建模方法用于构建逻辑场景模型,并结合ADS领域知识及ISO 26262功能安全标准,提出了一种逻辑场景建模语言SML4ADS,给出了其相应的语法及语义模型。此外,设计并实现了一种可扩展的、灵活的场景模型仿真方法,能够支持多种场景仿真工具。结合实际案例分析,展现了本文所提出的模型驱动式场景建模及仿真方法的有效性,为后续场景模型的测试、验证与分析奠定基础。

关键词：自动驾驶场景建模领域特定建模语言场景仿真

来源：评论

学校读者我要写书评

暂无评论

一种SCADE同步语言程序安全属性自动验证工具

引用

小型微型计算机系统 2022年第4期43卷 858-864页

作者：孙毅陈哲冉丹杨志斌南京航空航天大学计算机科学与技术学院南京211106 华东师范大学上海市高可信计算重点实验室上海200062 南京大学计算机软件新技术国家重点实验室南京210093

安全关键领域的反应系统大都采用同步语言开发,然而,学术界尚不存在SCADE同步语言程序的形式化验证工具,为此,本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模,可... 详细信息

安全关键领域的反应系统大都采用同步语言开发,然而,学术界尚不存在SCADE同步语言程序的形式化验证工具,为此,本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模,可将SCADE同步语言程序的安全属性的验证问题转化为无量词一阶逻辑公式的可满足性问题;然后采用先进的可满足性模理论求解器对其可满足性进行求解.本方法旨在实现对SCADE同步语言程序进行自动地、直接地验证,以填补SCADE同步语言程序验证领域的技术空白.此外,本文对所提方法进行了代码实现,并通过实验验证了所提方法的有效性.

关键词：反应系统 SCADE同步语言形式化验证一阶逻辑可满足性模理论

来源：评论

学校读者我要写书评

暂无评论

区域控制器的安全需求建模与自动验证

引用

软件学报 2020年第5期31卷 1374-1391页

作者：刘筱珊袁正恒陈小红陈铭松刘静周庭梁上海市高可信计算重点实验室(华东师范大学) 上海200062 卡斯柯信号有限公司上海200071

轨道交通区域控制器是我国轨道交通信号系统选型的主流制式--基于通信的列车控制系统的核心子系统,其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题.但是区域控制器自身的复杂性以及领域知识的繁杂难以掌握,使得形式化... 详细信息

轨道交通区域控制器是我国轨道交通信号系统选型的主流制式--基于通信的列车控制系统的核心子系统,其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题.但是区域控制器自身的复杂性以及领域知识的繁杂难以掌握,使得形式化方法很难应用到安全需求的验证中去.针对这些问题,提出一种安全需求的自动验证方法,使用半形式化的问题框架方法来建模和分解安全需求,根据需求模型自动生成安全需求的验证模型和验证性质,在此基础上自动生成验证模型的Scade语言实现,并通过DesignVerifier验证器对需求进行组合验证.最后,使用某个实际案例区域控制器的一个子问题CAL_EOA进行了研究,实验结果证明了该方法的可行性与有效性.它能够自动地将安全需求模型进行组合验证,改善了验证的效率.

关键词：区域控制器安全需求建模自动验证需求分解组合验证

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：