阚双龙

作品数：15被引量：110H指数：5
导出分析报告
供职机构：南京航空航天大学计算机科学与技术学院更多>>
发文主题：SPIN嵌入式机载软件适航认证嵌入式系统更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《计算机学报》《计算机工程与应用》《计算机科学与探索》《计算机应用研究》更多>>
所获基金：国家自然科学基金中央高校基本科研业务费专项资金中国博士后科学基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
嵌入偏序约简的状态事件线性时序逻辑验证被引量：6
《计算机学报》2019年第10期2145-2159,共15页谢健 阚双龙 黄志球 王飞 杨志斌 李伟湋 
国家高技术研究发展计划项目（2015AA105303）;国家重点研发计划项目(2016YFB1000802）;江苏省自然科学基金青年基金（BK20170809）;中国博士后基金面上基金（2018M632304）资助
模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状...
关键词：偏序约简 状态事件线性时序逻辑 模型检验 同步乘 标签Kripke结构 
位置约束的访问控制模型及验证方法被引量：5
《计算机研究与发展》2018年第8期1809-1825,共17页曹彦 黄志球 阚双龙 彭焕峰 柯昌博 
国家"八六三"高技术研究发展计划基金项目(2015AA015303);国家自然科学基金项目(61772270;61602262;61602237);江苏省自然科学基金青年项目(BK20150865;BK20170809)~~
随着物联网和信息物理融合系统等新一代信息技术的发展,位置约束的访问控制系统的安全性需求不仅体现在虚拟的信息空间,还体现在现实的物理空间.如何在这种新需求下制定位置约束的访问控制模型与验证方法成为保证访问控制系统安全的关...
关键词：位置约束访问控制系统 模型检测 偶图 反应规则 验证 
SIGNAL模型多线程代码生成研究被引量：1
《计算机科学与探索》2018年第4期536-549,共14页阚双龙 黄志球 杨志斌 
国家自然科学基金No.61502231;国家高技术研究发展计划(863计划)No.61502231;国家重点研发项目No.2016YFB1000800~~
反应式系统是指与环境不断发生交互的控制系统。这类系统通过接收外部环境输入,对输入进行计算,并将计算结果反馈到外部环境来控制系统的行为。同步语言是一种规约反应式系统的建模语言,同步语言的优势在于支持形式化验证和精确的代码...
关键词：反应式系统 同步语言 SIGNAL 代码生成 卫式操作 
一种安全攸关嵌入式系统需求追踪方法被引量：7
《计算机学报》2018年第3期652-669,共18页王飞 黄志球 杨志斌 阚双龙 沈国华 陈光颖 
国家"八六三"高技术研究发展计划项目基金(2015AA105303);GF基础科研重点项目(JCKY2016203B011);国家自然科学基金(61502231)资助
嵌入式系统在航空、航天、核能及交通等安全攸关领域中的广泛应用,使得保障其安全性至关重要.需求可追踪是安全攸关领域标准的基本要求,也是安全性分析与保障的重要前提.当前可追踪性的研究主要集中在需求与代码之间,缺乏需求与设计间...
关键词：嵌入式系统 系统需求 设计 可追踪性 谓词逻辑 语义模型 安全性分析 
一个基于两区间八边形约束的抽象域
《计算机工程与科学》2017年第4期740-747,共8页丁泽文 郭鸿昌 阚双龙 张弛 
国家863计划(2015AA015303);江苏省研究生培养创新工程(KYLX_0315);国家自然科学基金(61272038)
抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界。抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精...
关键词：抽象解释 八边形抽象域 两区间 迁移函数 
面向DO-333的襟缝翼控制单元安全性分析被引量：6
《计算机科学》2016年第5期150-156,161,共8页陈光颖 黄志球 陈哲 阚双龙 
国家自然科学基金(61100034;61170043);中国博士后科学基金(20110491411);江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助
DO-333是对机载软件安全性标准DO-178C关于形式化方法的补充,为机载软件开发过程中形式化方法的使用提供指导。模型检验作为一种形式化方法,可以应用于对软件需求和设计阶段制品的严格验证。基于DO-333,使用模型检验对飞控系统中襟缝翼...
关键词：适航认证 形式化方法 模型检验 机载软件 SPIN 
基于八边形抽象域的襟缝翼控制系统安全性分析被引量：2
《小型微型计算机系统》2016年第5期902-907,共6页陆陈 黄志球 阚双龙 曹德建 黄传林 
国家自然科学基金项目(61100034;61170043)资助;中国博士后科学基金项目(20110491411)资助;江苏省研究生培养创新工程项目(KYLX_0315)资助;江苏省普通高校研究生科研创新计划项目资助;中央高校基本科研业务费专项资金项目(CXZZ11_0218)资助
嵌入式软件在安全关键领域的广泛运用使得保障软件安全性成为工业界和学术界关注的重要课题.抽象解释作为一种形式化方法为程序变量的数值分析提供了一种通用框架,八边形抽象域是抽象解释的一种关系型数值抽象域,可以表示两个变量间的...
关键词：抽象解释 八边形抽象域 数值分析 航空控制软件 
云计算环境中支持语义的安全策略匹配研究被引量：2
《小型微型计算机系统》2015年第11期2451-2456,共6页朱羿全 沈国华 黄志球 康达周 阚双龙 
国家自然科学基金项目(61272083;61100034;61170043)资助;江苏省自然科学基金青年基金项目(BK20130812)资助;中央高校基本科研业务费专项资金项目(NS2014099)资助
云计算环境中,一致的安全策略是用户和服务能够成功交互的基础.如何有效地实现安全策略的匹配已经成为保证云计算环境安全的重要关注点之一.因此,提出一种云计算环境中支持语义的服务安全策略匹配方法,将策略匹配的问题转换成语义概念...
关键词：云计算 安全策略 语义匹配 云安全本体 描述逻辑 
基于故障扩展SysML活动图的软件安全性分析方法研究被引量：5
《小型微型计算机系统》2015年第9期2067-2074,共8页曹德建 黄志球 阚双龙 黄传林 
国家自然科学基金项目(61100034;61170043)资助;中国博士后科学基金项目(20110491411)资助;江苏省普通高校研究生科研创新计划项目;中央高校基本科研业务费专项项目(CXZZ11_0218)资助
随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对软件模型的安全性分析与验证方法一直是学术界和工业界的研究热点之一.功能模型和安全需求分析模型是分析嵌入式安全关键系统的两个重要方面,但两种模型一般都被分开使用.提出...
关键词：嵌入式系统 安全性分析 SysML活动图 故障树分析 故障扩展Sys ML活动图 
一种结合AADL和IMC的系统可靠性建模方法被引量：5
《计算机工程与科学》2015年第8期1517-1524,共8页程亦涵 黄志球 阚双龙 
随着嵌入式软件在安全关键领域广泛应用,系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显重要。结构分析设计语言AADL是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。由于AADL是一种半形式化模型,需要精确描述其语...
关键词：AADL 可靠性模型 IMC模型转换 形式化方法 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部