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

软件学报 2020年第9期31卷 2723-2740页

作者：许瑞谷守珍沙行勉诸葛晴凤石亮高思远华东师范大学计算机科学与技术学院上海200062 上海市高可信计算重点实验室(华东师范大学) 上海200062

当前,大数据及人工智能技术向嵌入式系统发展,对嵌入式系统的存储访问能力提出了更高的要求.磁畴壁存储器凭借其高读写速度、高密度以及低功耗等优点,可以用于嵌入式系统,以满足数据密集型应用对访问速度、容量及能耗的需求.但是磁畴壁... 详细信息

当前,大数据及人工智能技术向嵌入式系统发展,对嵌入式系统的存储访问能力提出了更高的要求.磁畴壁存储器凭借其高读写速度、高密度以及低功耗等优点,可以用于嵌入式系统,以满足数据密集型应用对访问速度、容量及能耗的需求.但是磁畴壁存储器在进行数据访问之前需要进行移动操作,这将极大影响其存储访问性能.而减少移动操作可以有效提升磁畴壁存储器的性能.面向运行数据密集型应用的多读/写头磁畴壁存储器系统,研究减少移动操作的最优指令调度与数据放置技术.首先提出了可获得最小移动次数的整数线性规划(integer linear programming,简称ILP)模型.由于ILP模型不能在多项式时间内求得最优解,所以提出了多项式时间的启发式算法——生成指令调度和数据放置(generation instruction scheduling and data placement,简称GISDP)算法.实验结果表明,ILP模型和GISDP算法可以有效减少移动操作的次数.在配备8个读/写头的磁畴壁存储器上,GISDP算法生成的指令调度与数据放置方案相较其他算法可以平均减少89.7%的移动操作,并且GISDP算法的结果接近ILP模型的最优解.

关键词：磁畴壁存储器数据密集型应用指令调度数据放置移动操作

来源：评论

学校读者我要写书评

暂无评论

轨道交通联锁领域特定语言的形式化

引用

软件学报 2020年第6期31卷 1638-1653页

作者：赵梦瑶陈小红孙海英刘静陈良育周庭梁上海市高可信计算重点实验室(华东师范大学) 上海200062 卡斯柯信号有限公司上海200071

作为轨道交通系统的核心子系统之一,对联锁系统进行形式化建模与分析,是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合,由于形式化知识难以掌握,领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题... 详细信息

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

关键词：联锁系统模板重用形式化建模随机混成自动机领域特定语言

来源：评论

学校读者我要写书评

暂无评论

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

引用

软件学报 2020年第6期31卷 1587-1599页

作者：杜德慧管春琳王耀郭童华东师范大学软件工程学院上海200062 上海市高可信重点实验室(华东师范大学) 上海200062 教育部可信软件国际合作联合实验室(华东师范大学) 上海200062

信息物理融合系统(cyber-physical systems,简称CPS)是深度融合了计算进程和物理进程的统一体,是集计算、通信与控制于一体的下一代智能系统,具有广阔的应用前景.CPS的行为具有混成性、随机性等特征,建模及仿真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的建模及仿真提供了一种有效的方法及工具支撑.

关键词：信息物理融合系统领域建模语言元建模仿真 GEMOC

来源：评论

学校读者我要写书评

暂无评论

多神经网络协作的军事领域命名实体识别

引用

清华大学学报（自然科学版） 2020年第8期60卷 648-655页

作者：尹学振赵慧赵俊保姚婉薇黄泽林华东师范大学软件工程学院上海200062 华东师范大学上海市高可信计算重点实验室上海200062 北京遥感信息研究所北京100085

互联网公开数据蕴含着大量高价值的军事情报,成为获取开源军事情报的重要数据源之一。军事领域命名实体识别是进行军事领域信息提取、问答系统、知识图谱等工作的基础性关键任务。相比较于其他领域的命名实体,军事领域命名实体边界模糊... 详细信息

互联网公开数据蕴含着大量高价值的军事情报,成为获取开源军事情报的重要数据源之一。军事领域命名实体识别是进行军事领域信息提取、问答系统、知识图谱等工作的基础性关键任务。相比较于其他领域的命名实体,军事领域命名实体边界模糊,界定困难;互联网媒体中军事术语表达不规范,随意性的简化表达现象较普遍;现阶段面向军事领域的公开语料鲜见。该文提出一种考虑实体模糊边界的标注策略,结合领域专家知识,构建了基于微博数据的军事语料集MilitaryCorpus;提出一种多神经网络协作的军事领域命名实体识别模型,该模型通过基于Transformer的双向编码器(bidirectional encoder representations from transformers, BERT)的字向量表达层获得字级别的特征,通过双向长短时记忆神经网络(bi-directional long short-term memory, BiLSTM)层抽取上下文特征形成特征矩阵,最后由条件随机场层(conditional random field, CRF)生成最优标签序列。实验结果表明:相较于基于CRF的实体识别模型,应用该文提出的BERT-BiLSTM-CRF模型召回率提高28.48%,F值提高18.65%;相较于基于BiLSTM-CRF的实体识别模型,该文模型召回率提高13.91%,F值提高8.69%;相较于基于CNN (convolutional neural networks)-BiLSTM-CRF的实体识别模型,该文模型召回率提高7.08%,F值提高5.15%。

关键词：军事命名实体识别双向偏码器(BERT) 模糊边界多神经网络

来源：评论

学校读者我要写书评

暂无评论

循环迭代程序的一种可信计算算法

引用

软件学报 2020年第12期31卷 3685-3699页

作者：赵世忠陈冬火刘静华东师范大学软件工程学院上海200062 上海市高可信计算重点实验室(华东师范大学) 上海200062 苏州大学计算机科学与技术学院江苏苏州215006

循环迭代程序作为软件的基本组成部分,其正确运行具有重要意义.然而,有时(比如其相关错数大于0时)计算时的舍入误差(或表示误差)会导致循环迭代的计算结果不稳定.基于“中间计算精度自动动态调整”的计算技术,给出了循环迭代程序的一种... 详细信息

循环迭代程序作为软件的基本组成部分,其正确运行具有重要意义.然而,有时(比如其相关错数大于0时)计算时的舍入误差(或表示误差)会导致循环迭代的计算结果不稳定.基于“中间计算精度自动动态调整”的计算技术,给出了循环迭代程序的一种可信计算算法.利用该算法,可获得循环迭代程序任意次迭代的任意位的正确有效数字.目前,通过C++语言该算法已被编程实现于ISReal中.

关键词：循环迭代误差可控计算可信计算可靠计算错数

来源：评论

学校读者我要写书评

暂无评论

嵌入式实时操作系统内核混合代码的自动化验证框架

引用

软件学报 2020年第5期31卷 1353-1373页

作者：郭建丁继政朱晓冉华东师范大学软件工程学院上海200062 上海市高可信计算重点实验室(华东师范大学) 上海200062 软硬件协同设计技术与应用教育部工程研究中心(华东师范大学) 上海200062

"如何构造高可信的软件系统"已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠,将形式化方法引入到操作系统内核验证中,提出... 详细信息

"如何构造高可信的软件系统"已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠,将形式化方法引入到操作系统内核验证中,提出了一个自动化验证操作系统内核的框架.该验证框架包括:(1)分别对C语言程序和混合语言程序(C语言和汇编语言)进行验证;(2)在混合语言程序验证中,为汇编程序建立抽象模型,并将C语言程序和抽象模型粘合形成基于C语言验证工具可接收的验证模型;(3)从规范中提取性质,基于该自动验证工具,对性质完成自动验证;(4)该框架不限于特定的硬件架构.成功地运用该验证框架对两种不同硬件平台的嵌入式实时操作系统内核μC/OS-Ⅱ进行了验证.结果显示,利用该框架在对两个不同的硬件平台上内核验证时,框架的可重复利用率很高,高达83.8%,虽然其抽象模型需要根据不同的硬件平台进行重构.在对基于这两种平台的操作系统内核验证中,分别发现了10处~12处缺陷.其中,在ARM平台上两处与硬件相关的问题被发现.实验结果表明,该方法对不同硬件平台的同一个操作系统分析验证具有一定的通用性.

关键词：实时操作系统 VCC 混合程序验证自动验证 Z3求解器

来源：评论

学校读者我要写书评

暂无评论

点集拓扑学之杨忠道定理的一个机械化证明

引用

中国科学：数学 2021年第1期51卷 257-288页

作者：曾振柄王建林杨争峰小林英恒上海大学数学系上海200444 河南大学计算机与信息工程学院开封475004 华东师范大学上海市高可信计算重点实验室上海200062 Department of Mathematics College of Science and TechnologyNihon UniversityTokyo 101-8308Japan

本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.

关键词：拓扑空间开集闭集导集杨忠道定理机器证明

来源：评论

学校读者我要写书评

暂无评论

藏药方解数字化研究初探

藏药方解数字化研究初探

引用

第二十届中国科学家论坛

作者：平措绕吉郭新辉海梅荣吴敏蔡景伟旦增益西云南农业大学华东师范大学上海市高可信计算重点实验室

目的:探讨藏药方解的数字化规律。藏药方解,即对藏药方剂配伍规律的解析,是藏医药的核心理论和临床实践的重要依据。方法:应用集合论、群论、矩阵代数等数学方法和Python可视化软件,对藏药方解理论中的五源体系、药物的味性效进行了建模... 详细信息

目的:探讨藏药方解的数字化规律。藏药方解,即对藏药方剂配伍规律的解析,是藏医药的核心理论和临床实践的重要依据。方法:应用集合论、群论、矩阵代数等数学方法和Python可视化软件,对藏药方解理论中的五源体系、药物的味性效进行了建模,并选取30多首25味以下的常用藏药方剂,计算和分析了方剂的六味、三化味、八性、十七效及作用于三因的比例。结果:模型的计算结果在方剂的实际功效与所对治的疾病三因比值上均高度吻合;运用Python可视化软件对方剂的六味、三化味、八性、十七效与对治疾病进行了可视化呈现。结论:针对25味以下的藏药方剂,本研究提出的线性模型简单、有效、准确度高。下一步的研究思路是,进一步细化六味以及其相互增强或抑制的关系,在味性效模型中增加量效关系的考虑,以提高模型的准确率,扩大适用范围。

关键词：藏药方解数字化五源六味十七效群论矩阵代数

来源：评论

学校读者我要写书评

暂无评论

颜色密度直方图检索方法

引用

小型微型计算机系统 2021年第10期42卷 2085-2088页

作者：王小玲毛宏燕上海立信会计金融学院信息管理学院上海201620 华东师范大学上海高可信计算重点实验室上海200062

颜色是基于内容的图像检索的重要特征.传统颜色直方图由于只考虑色彩总量而无法区别色彩空间分布差异.本文提出了一种新的颜色密度直方图(Color Density Histogram CDH).通过计算主要颜色的密度,反映颜色的空间分布离散程度.密度大,颜... 详细信息

颜色是基于内容的图像检索的重要特征.传统颜色直方图由于只考虑色彩总量而无法区别色彩空间分布差异.本文提出了一种新的颜色密度直方图(Color Density Histogram CDH).通过计算主要颜色的密度,反映颜色的空间分布离散程度.密度大,颜色分布较集中,密度小,则颜色分布较分散.在HSV颜色空间上,使用CAREL的1000图像做测试数据集,在平均查准率、查全率上都优于颜色直方图方法.结果表明,CDH能够结合颜色和空间特征,比传统的颜色直方图具有具有更好的检索效果.

关键词：基于内容的图像检索颜色直方图空间分布基于颜色的图像检索

来源：评论

学校读者我要写书评

暂无评论

基于程序转化的SCADE模型检测

引用

计算机科学 2021年第12期48卷 125-130页

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

SCADE同步语言是一种常用的嵌入式系统程序设计语言。在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统。SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语... 详细信息

SCADE同步语言是一种常用的嵌入式系统程序设计语言。在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统。SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码。目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后。为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测。此外,通过理论推导和大量实验证明了工具的模型检测的正确性。实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低。

关键词：模型检测安全有限状态机词法分析语法分析抽象语法树 JKind

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：