谢健

作品数：15被引量：57H指数：4
导出分析报告
供职机构：南京航空航天大学更多>>
发文主题：AADL规约自动转换自动生成方法层次化更多>>
发文领域：自动化与计算机技术文化科学更多>>
发文期刊：《科教导刊》《计算机科学与探索》《计算技术与自动化》《文教资料》更多>>
所获基金：中央高校基本科研业务费专项资金国家自然科学基金中国航空科学基金江苏省自然科学基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
随机混成系统稀有属性的统计模型检测方法
《软件学报》2022年第10期3717-3731,共15页房丙午 黄志球 谢健 
国家重点研发计划(2016YFB1000802,2018YFB1003902);高安全系统软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学)研究项目(NJ2019006)。
统计模型检测,已成为随机混成系统安全性验证的重要方法.但对安全性要求较高的系统,其不安全事件和系统失效都是稀有事件.在这种情况下,统计模型检测很难采样到满足稀有属性的样本而变得不可行.针对该问题,提出了交叉熵迭代学习的统计...
关键词：随机混成系统 安全性 稀有属性 交叉熵迭代学习 统计模型检测 
安全关键系统多范式建模及安全性分析方法
《小型微型计算机系统》2022年第9期2005-2016,共12页李书铭 杨志斌 谢健 周勇 陈静 
国家自然科学基金项目(62072233)资助;航空科学基金项目(201919052002)资助;中央高校基本科研业务费专项资金项目(NP2017205)资助.
随着安全关键系统的规模和复杂性不断增长,单一建模语言无法完全覆盖该类异构系统的建模要求.近年来,多范式建模方法逐渐成为表达复杂异构系统的有力手段,而安全性分析则是保证安全关键系统质量的重要步骤.本文提出一种面向安全关键系...
关键词：安全关键系统 多范式建模 安全性分析 SYSML AADL ARP4761 
安全关键软件的AADL模型自动逆向构造方法被引量：2
《小型微型计算机系统》2022年第7期1553-1561,共9页邱志凯 杨志斌 谢健 周勇 程高辉 陈俊文 
国家自然科学基金项目(62072233)资助;航空科学基金项目(201919052002)资助;中央高校基本科研业务费专项资金项目(NP2017205)资助.
近年来,采用模型驱动(Model-Driven)尤其是形式化模型驱动的安全关键软件设计与开发方法逐渐受到重视,并被工业界认为是切实可行的重要手段.AADL(Architecture Analysis and Design Language)是一种广泛应用于安全关键领域的形式化建模...
关键词：安全关键软件 模型驱动工程 模型驱动逆向工程 AADL 
面向IMA的AADL多范式建模及代码自动生成方法被引量：10
《小型微型计算机系统》2021年第10期2223-2233,共11页邱宝 杨志斌 周勇 谢健 王铁鑫 郭鹏 
航空科学基金项目(201919052002)资助;中央高校基本科研业务费专项(NP2017205)资助。
综合模块化航空电子系统(Integrated Modular Avionics,IMA)是安全关键领域中一类重要的复杂嵌入式系统,具有分布式、异构、计算资源和物理资源强耦合等特征,单一建模语言无法完全覆盖该类系统的建模要求.近年来,多范式建模方法(Multi-P...
关键词：IMA 多范式建模 AADL 同步语言 SDL 代码生成 
基于限定中文自然语言需求的SysML模型自动生成方法被引量：3
《计算机研究与发展》2021年第4期706-730,共25页鲍阳 杨志斌 杨永强 谢健 周勇 岳涛 黄志球 郭鹏 
国家自然科学基金项目(62072233);航空科学基金项目(201919052002);中央高校基本科研业务费专项资金项目(NP2017205)。
模型驱动开发方法逐渐成为安全关键信息物理融合系统(safety-critical cyber-physical system,SC-CPS)设计与开发的重要手段.然而,安全关键信息物理融合系统需求往往是通过自然语言描述的,如何自动化或半自动化链接自然语言需求和基于...
关键词：安全关键信息物理融合系统 模型驱动开发方法 系统建模语言 术语推荐 限定自然语言需求 模型转换 
嵌入偏序约简的状态事件线性时序逻辑验证被引量：6
《计算机学报》2019年第10期2145-2159,共15页谢健 阚双龙 黄志球 王飞 杨志斌 李伟湋 
国家高技术研究发展计划项目（2015AA105303）;国家重点研发计划项目(2016YFB1000802）;江苏省自然科学基金青年基金（BK20170809）;中国博士后基金面上基金（2018M632304）资助
模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状...
关键词：偏序约简 状态事件线性时序逻辑 模型检验 同步乘 标签Kripke结构 
系统架构描述语言AADL的功能行为建模扩展被引量：2
《计算机科学与探索》2019年第10期1638-1653,共16页许金淼 杨志斌 黄志球 谢健 周勇 
国家自然科学基金;国家重点研发计划;GF基础科研重点项目;江苏省自然科学基金;中央高校基本科研业务费专项资金~~
架构分析与设计语言(AADL)是一种用于描述复杂嵌入式系统体系架构的建模语言,被广泛用于安全关键系统建模与验证。AADL通过行为附件以状态机的形式对组件的内部行为建模。工业界中的复杂系统常使用层次自动机描述组件的功能行为,而行为...
关键词：安全关键系统 架构分析与设计语言(AADL) 层次行为附件(HBA) 功能规约 
一种同步语言多线程代码自动生成工具被引量：13
《软件学报》2019年第7期1980-2002,共23页杨志斌 袁胜浩 谢健 周勇 陈哲 薛垒 Jean-Paul BODEVEIX Mamoun FILALI 
国家自然科学基金(61502231);国家重点研发计划(2016YFB1000802);GF基础科研重点项目(JCKY2016203B011);江苏省自然科学基金(BK20150753);中央高校基本科研业务费专项资金(NP2017205);国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130);南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20181603)~~
随着安全关键系统对计算性能要求的日趋提高,能够提供更强计算能力而又减少电子设备的体积、重量和功耗的多核处理器将在安全关键领域得到广泛应用。同步语言能够表达确定性并发行为且具有精确时间语义等特性,适用于安全关键软件的建模...
关键词：同步语言 同步多时钟卫式动作 多线程代码生成 
基于动态故障树的航空发动机可靠性分析方法研究被引量：12
《计算技术与自动化》2019年第2期1-7,共7页宛伟健 谢健 葛晓瑜 
国家自然科学基金资助项目(61772270);国家重点研发计划资助项目(2016YFB1000802)
随着航空发动机技术的不断发展,对其性能要求不断提高,使得航空发动机的安全性和可靠性变得愈发重要。然而,当前针对航空发动机的可靠性分析方法较少考虑系统失效时的动态特性,面向《航空发动机适航规定》(CCAR33-R2),考虑航空发动机危...
关键词：CCAR33-R2.75 动态故障树 离散时间马尔科夫链 概率模型检测 PRISM 
一种形式化建模中活性属性转化方法研究
《计算技术与自动化》2018年第3期161-164,共4页张棋 谢健 尹小花 
国家自然科学基金资助项目(61772270);国家重点研发计划(2016YFB1000802)
现有的安全关键系统开发的方法一般是在系统开发后期使用测试的方法对系统需求进行验证,这种方法一方面需要耗费大量时间与人力,另一方面测试并不能保证系统中不存在错误。使用形式化的开发方法可以将软件需求添加到模型中,使用数学证...
关键词：安全关键系统 KAOS EVENT-B 活性 模型检测 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部