NUSMV

作品数：38被引量：77H指数：5
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：魏强胡军吴海桥刘超刘博更多>>
相关机构：南京航空航天大学北京交通大学陕西师范大学中山大学更多>>
相关期刊：《计算机技术与发展》《计算机与数字工程》《青岛大学学报（自然科学版）》《电子科技大学学报》更多>>
相关基金：国家自然科学基金中央高校基本科研业务费专项资金国家重点基础研究发展计划国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
RFID认证协议安全性模型检测验证方法被引量：1
《信息安全研究》2024年第11期1043-1048,共6页贾昊洲 徐鹏 王丹琛 徐扬 
中央高校基本科研业务费专项资金项目(2682021GF012)。
RFID技术作为物联网的核心技术,在各个领域中已被广泛应用.目前RFID系统频繁遭受安全威胁,主要原因在于RFID系统中的读取器和标签使用的是无线通信方式.RFID安全认证协议作为RFID系统通信安全保障的一种重要手段,其内在安全至关重要,同...
关键词：RFID 认证协议 模型检测 NUSMV 形式化验证 
基于UML-NuSMV的并发系统建模与验证
《华中科技大学学报（自然科学版）》2024年第2期90-95,共6页马占有 郭昊 李召恺 李健祥 
国家自然科学基金资助项目(61962001);宁夏自然科学基金资助项目(2021AAC03004).
为解决直接建立系统NuSMV(符号模型检测器)模型的困难,提出一种从UML(统一建模语言)模型转换到NuSMV模型的方法,实现了UML与NuSMV结合的形式化验证.首先,使用UML中的视图对系统进行描述,建立系统的UML模型;然后,设计转换规则并给出转换...
关键词：模型检测 统一建模语言 模型转换 并发系统 符号模型检测器 
基于NuSMV的LD和ST语言形式化验证研究与实现被引量：1
《电子技术应用》2022年第12期94-99,共6页郭肖旺 赵德政 
国防基础科研计划资助项目(JCKY2018211C001)。
依据工控系统的特点,在分析现有工控系统编程标准IEC61131-3规定的工业语言基础上,研究基于工业语言的形式化验证方法,通过对ST和LD语言进行分析得到有限状态机组态模型,实现对控制目标进行准确描述;通过NuSMV验证有限状态机模型,获得...
关键词：工控系统 编译 形式化验证 有限状态机 建模 
基于NuSMV的AADL模型形式化验证技术被引量：5
《航空学报》2022年第3期443-458,共16页刘畅 蒋永平 马春燕 张涛 
航空科学基金(20175553028,20185853038,201907053004)。
结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先,覆盖AADL模...
关键词：AADL模型 NUSMV 形式化验证 模型转换 飞行控制系统 
基于模型检查的民用飞机飞控系统安全性评估被引量：2
《民用飞机设计与研究》2021年第3期32-37,共6页范基坪 洪骥宇 
在以大型民机为代表的安全关键系统研制中,系统复杂度的提升极大地降低了依赖设计人员经验的传统安全性评估手段的效率与有效性,并带来了反复迭代困难等问题,基于模型的安全性评估方法(MBSA)能够显著降低研制过程的分析复杂度,提高安全...
关键词：基于模型的安全性评估 模型检查 SMV NUSMV 飞控系统 
基于符号模型检测的Web服务组合形式化验证被引量：1
《计算机与数字工程》2021年第3期496-501,520,共7页张世杰 徐鹏 刘沛瑶 
国家自然科学基金项目“基于矛盾体分离的动态自动演绎推理研究”(编号:61673320);四川省教育厅项目(编号:18ZB0589)资助。
随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求。Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题。针...
关键词：WEB服务组合 符号模型检测 有限状态自动机 形式化定义 NUSMV 
一种AltaRica3.0模型到NuSMV模型的转换方法被引量：1
《计算机科学》2020年第12期73-86,共14页陈朔 胡军 唐红英 石梦烨 
国家重点基础研究发展计划(973计划)(2014CB744904);南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20181607)。
AltaRica 3.0是一类面向复杂关键系统的安全性建模与分析语言,缺乏时态属性的模型检验技术,不支持穷尽式的空间检验,而NuSMV支持穷尽式的模型检验技术,因此对AltaRica 3.0模型进行扩展,提出了基于语言解析器生成器ANTLR(Another Tool fo...
关键词：ANTLR AltaRica 3.0 GTS AST NUSMV 模型转换 
基于NuSMV的SysML模型形式化验证被引量：4
《计算机技术与发展》2019年第10期153-156,共4页邓刘梦 葛晓瑜 宛伟健 
国家自然科学基金(617722770);南京航空航天大学开放基金(kfjj20171606)
航空航天道路交通等高安全领域的系统开发需要保证高安全、高可靠,对于该类系统的合理建模以及模型验证则尤为重要。当前模型驱动开发方法已经广泛应用于安全关键系统的开发过程中,它支持在早期就对系统进行安全分析和验证,有效地控制...
关键词：需求工程 模型转换 形式化验证 模型驱动开发 
安全关键系统需求形式化建模分析实例研究被引量：1
《计算机科学与探索》2019年第8期1295-1306,共12页张维珺 胡军 李宛倩 陈朔 石梦烨 唐红英 
国家重点基础研究发展计划(973计划)No.2014CB744903;南京航空航天大学研究生创新基地(实验室)开放基金No.kfjj20171611;中央高校基本科研业务费专项资金~~
近年来,基于模型的安全性分析技术(MBSA)在航空等领域有着广泛应用,因此对以xSAP安全分析平台为核心,基于MBSA的系统安全性评估方法进行了研究,并通过一个真实的综合航电系统GarminG1000的自动飞行控制系统(AFCS)GFC700为实例来详细介...
关键词：自动飞行控制系统(AFCS) 基于模型的安全性分析方法(MBSA) NUSMV xSAP 模型扩展 故障树 失效模式与影响分析(FMEA)表 
面向需求的安全关键系统形式化建模与验证方法研究被引量：3
《计算机工程与科学》2019年第8期1426-1433,共8页胡军 张维珺 李宛倩 
南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20171611)(中央高校基本科研业务费专项资金);国家重点基础研究发展计划-973计划(2014CB744903)
在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML-e语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML-e模型转化成NuSMV...
关键词：MBSE 自动飞行控制系统(AFCS) 形式化验证 RSML-e NUSMV 模型转换 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部