华东师范大学软件学院上海市高可信计算重点实验室

作品数：92被引量：987H指数：13
导出分析报告
发文作者：刘静陈胜利关冬亮吴敏何向南更多>>
发文领域：自动化与计算机技术理学文化科学医药卫生更多>>
发文主题：形式化验证推荐系统隐私保护社交网络混成系统更多>>
发文期刊：《计算机应用》《系统科学与数学》《哈尔滨理工大学学报》《亚太传统医药》更多>>
所获基金：国家自然科学基金国家重点基础研究发展计划上海市教育委员会重点学科基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一机构
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
星载嵌入式软件全数字仿真开发验证平台被引量：1
《计算机测量与控制》2024年第5期302-311,共10页王赛亚 吴小明 邓玉欣 
为了应对当前航天器软件功能日趋复杂与软件研制周期短、对软件可靠性和安全性要求高的矛盾,同时为了满足国产化自主可控的需求,在国产Linux操作系统下,以QEMU的SPARC V8指令集模拟器为基础,解决了SOC2012片内外设与A6017仿真等关键问题...
关键词：LINUX QEMU SPARC V8 SOC2012 嵌入式软件 全数字仿真 
片段级别的双编码器方面情感三元组抽取模型
《计算机科学与探索》2023年第12期3010-3019,共10页张韵琪 李松达 兰于权 李东旭 赵慧 
国家重点研发计划(2019YFB2102600)。
方面情感三元组抽取(ASTE)是方面级情感分析的子任务之一,旨在识别出句子中所有的方面词及其对应的观点词和情感极性。目前,ASTE任务通过流水线模型或端到端模型完成,前者无法解决三元组方面词重叠问题,且忽视了观点词和情感极性之间的...
关键词：情感分析 方面情感三元组抽取(ASTE) 流水线模型 片段 独立编码器 
阿育吠陀医学与藏医学、蒙医学的渊源关系被引量：1
《亚太传统医药》2023年第7期7-13,共7页平措绕吉 王证德 陈飞腾 蔡景伟 吴敏 海梅荣 
古印度作为世界四大文明古国之一,拥有独特的医学体系,其中阿育吠陀医学作为印度传统医学的主体,是历史最为悠久、具有代表性的医学体系。阿育吠陀医学、藏医学和蒙医学三者同为世界上较为古老的医学体系之一,相互之间存在着一定关联。...
关键词：藏医学 蒙医学 阿育吠陀 渊源关系 
PROPER:一个概率程序终止性与正确性分析工具
《软件学报》2022年第12期4464-4475,共12页赵旭慧 邓玉欣 符鸿飞 
国家自然科学基金(62072176,61832015,61802254)。
概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程...
关键词：概率编程 终止性 断言分析 程序验证 
一种SCADE同步语言程序安全属性自动验证工具被引量：3
《小型微型计算机系统》2022年第4期858-864,共7页孙毅 陈哲 冉丹 杨志斌 
国家自然基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助;南京大学计算机软件新技术国家重点实验室开放课题项目(KFKT2020B10)资助。
安全关键领域的反应系统大都采用同步语言开发,然而,学术界尚不存在SCADE同步语言程序的形式化验证工具,为此,本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模,可...
关键词：反应系统 SCADE同步语言 形式化验证 一阶逻辑 可满足性模理论 
基于程序转化的SCADE模型检测被引量：3
《计算机科学》2021年第12期125-130,共6页冉丹 陈哲 孙毅 杨志斌 
国家自然基金委员会-中国民航局民航联合研究基金(U1533130);中央高校基本科研业务费人工智能+专项(NZ2020019);上海市高可信计算重点实验室开放课题;南京大学计算机软件新技术国家重点实验室开放课(KFKT2020B10)。
SCADE同步语言是一种常用的嵌入式系统程序设计语言。在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统。SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语...
关键词：模型检测 安全有限状态机 词法分析 语法分析 抽象语法树 JKind 
颜色密度直方图检索方法被引量：2
《小型微型计算机系统》2021年第10期2085-2088,共4页王小玲 毛宏燕 
国家自然科学基金项目(19JZD023)资助。
颜色是基于内容的图像检索的重要特征.传统颜色直方图由于只考虑色彩总量而无法区别色彩空间分布差异.本文提出了一种新的颜色密度直方图(Color Density Histogram CDH).通过计算主要颜色的密度,反映颜色的空间分布离散程度.密度大,颜...
关键词：基于内容的图像检索 颜色直方图 空间分布 基于颜色的图像检索 
轨道交通控制软件中基于场景的需求分析方法被引量：1
《计算机工程》2021年第8期284-293,300,共11页闫倩倩 缪炜恺 
国家自然科学基金面上项目“数据驱动的机器学习软件系统的形式化需求建模工程方法”(61872144);国家自然科学基金青年基金“嵌入式控制软件的形式化规格说明构建的工程方法”(61402178)。
针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供...
关键词：形式化方法 需求规约 需求确认和验证 场景优化 轨道交通控制软件 
基于双通道R-FCN的图像篡改检测模型被引量：12
《计算机学报》2021年第2期370-383,共14页田秀霞 李华强 张琴 周傲英 
国家自然科学基金(面上项目,重点项目)(61772327,61532021);国网甘肃省电力公司电力科学研究院横向项目(H2019-275)资助.
随着大数据时代的到来和图像编辑软件的发展,恶意篡改图片的数量出现井喷式增长,为了确保图像的真实性,众多学者基于深度学习和图像处理技术提出了多种图像篡改检测算法.然而,当前提出的绝大多数方法在面对大量图片的情况下,篡改检测速...
关键词：图像篡改检测 深度学习 双通道网络 基于区域的全卷积网络 双线性插值 
点集拓扑学之杨忠道定理的一个机械化证明被引量：1
《中国科学：数学》2021年第1期257-288,共32页曾振柄 王建林 杨争峰 小林英恒 
国家自然科学基金(批准号:11471209和61772203)资助项目。
本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
关键词：拓扑空间 开集 闭集 导集 杨忠道定理 机器证明 
全选清除导出
共10页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部