形式化

作品数：5172被引量：11555H指数：35
导出分析报告
相关领域：自动化与计算机技术文化科学更多>>
相关作者：关永施智平薛锦云张广泉段振华更多>>
相关机构：华东师范大学国防科学技术大学西安电子科技大学清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家社会科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=小型微型计算机系统x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
面向无线传感器网络的认证密钥协商机制
《小型微型计算机系统》2024年第5期1204-1208,共5页李贵勇 张航 韩才君 李欣超 
教育部-中国移动科研基金项目(MCM201805-2)资助。
无线传感器网络(Wireless Sensor Networks,WSN)是物联网的重要组成部分,因为WSN能通过因特网将采集到的数据发送到云服务器.认证和密钥协商机制是一个重要的密码学概念,可以确保数据传输的安全和完整性.传感器节点是资源受限的设备,因...
关键词：无线传感器网络 认证和密钥协商 eCK模型 CDH假设 形式化证明 
一种基于无锁队列的运行时多线程并行验证方法被引量：1
《小型微型计算机系统》2024年第5期1249-1256,共8页李佳洁 陈哲 陈龙腾 
国家自然科学基金项目(62172217)资助;国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助。
运行时验证是一种动态的软件验证技术,主要包括使用形式化规约描述待验证性质、自动生成对应监控器以及监控器的插桩.然而现有的面向C语言程序的运行时验证技术存在一些局限性,主要体现在多监控器的情况下,现有的运行时验证工具只能使...
关键词：运行时验证 形式化规约 多线程 无锁队列 C语言程序 
面向自然语言需求的验证性质生成方法
《小型微型计算机系统》2024年第1期84-92,共9页李晓劼 杨志斌 王翰丰 周勇 李维 
国家自然科学基金项目(62072233)资助;国防基础科研项目(JCKY2020205C006)资助;航空科学基金项目(201919052002)资助.
安全关键系统和软件的安全性、可靠性需要形式化验证来保障,使用形式化验证的前提是从自然语言需求文本中提取相关验证性质并将其转化为形式化规约,这已成为当前形式化验证领域研究的热点和难点.当前的形式化规约提取工作大多针对英文需...
关键词：形式化验证 模式定义语言 自然语言处理 规约生成 
TrustZone中断隔离机制的形式化验证被引量：1
《小型微型计算机系统》2023年第9期2105-2112,共8页付俊仪 张倩颖 王国辉 李希萌 施智平 关永 
国家自然科学基金项目(61802375,61602325,61876111,61877040)资助;北京市教委科技计划一般项目(KM201910028005)资助;中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题项目(CARCH201920)资助;国防科技创新特区项目(18-163-11-ZT-005-038-05)资助;中央支持地方建设-“双一流”建设项目(20531120005)资助.
TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断...
关键词：TRUSTZONE 可信执行环境 中断隔离 信息流安全 形式化验证 
一种支持三方认证的轻量级RFID双向认证协议被引量：1
《小型微型计算机系统》2022年第10期2205-2213,共9页吴恺凡 殷新春 
国家自然科学基金面上项目(61472343)资助.
针对RFID系统存在的无线信道通信安全以及隐私保护问题,提出一种名为随机运算的轻量级技术.它可以使标签在公共信道通信时保持匿名,并通过洗牌算法来决定秘密值更新时使用的轻量级运算.结合随机运算方法,提出了一个支持三方验证的轻量级...
关键词：无线射频识别 K-匿名 物理不可克隆函数 二次剩余 双向认证 形式化验证 
神经网络可信性的形式化验证方法综述被引量：3
《小型微型计算机系统》2022年第9期1830-1837,共8页王莉 李晓娟 关永 王瑞 王佳岳 
国家自然科学基金项目(61977040,61876111)资助;科技创新服务能力建设(20530290073)-首都师范大学交叉研究院项目(19530012005)资助.
随着神经网络技术的不断发展和完善,其应用也随之扩展,如何保证其可信性是在许多应用领域特别是安全攸关应用中部署的关键,目前对神经网络可信性研究主要体现在通过循环优化网络训练等过程和对神经网络进行验证两方面.基于形式化方法可...
关键词：神经网络 可信性属性 模型抽象 形式化方法 
使用模型检测方法对Paxos算法进行验证与改进被引量：1
《小型微型计算机系统》2022年第5期1109-1113,共5页何东炼 杨晋吉 赵淦森 管金平 
广东省自然科学基金项目(2020A1515010445)资助。
因通信的同步问题、网络分区的可靠性问题等,分布式系统难以在通信、分区等环节失效的情况下对特定的状态达成共识.Paxos是近年分布式系统中常见且有效的共识算法,本文通过使用模型检测的方法对Paxos算法进行形式化建模,分析和验证了Pa...
关键词：形式化验证 模型检测 Paxos SPIN 
SFCDSL:一种服务功能链领域专用语言
《小型微型计算机系统》2022年第5期1114-1120,共7页阮宏玮 李华 王显荣 
国家自然科学基金项目(61862047)资助;内蒙古科技计划项目(201802028,2020GG0186)资助;内蒙自然科学基金项目(2018BS06001)资助。
为满足用户服务功能链需求,加快服务功能链编程效率,设计一种面向服务功能链领域的专用语言SFCDSL.从规范化和可扩展性考虑,首先提出SFC抽象化层次框架和SFCDSL编程框架.对于SFCDSL中的服务关系采用基于面向对象设计方法,给出了基于软...
关键词：服务功能链 领域专用语言 形式化 
一种SCADE同步语言程序安全属性自动验证工具被引量：3
《小型微型计算机系统》2022年第4期858-864,共7页孙毅 陈哲 冉丹 杨志斌 
国家自然基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助;南京大学计算机软件新技术国家重点实验室开放课题项目(KFKT2020B10)资助。
安全关键领域的反应系统大都采用同步语言开发,然而,学术界尚不存在SCADE同步语言程序的形式化验证工具,为此,本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模,可...
关键词：反应系统 SCADE同步语言 形式化验证 一阶逻辑 可满足性模理论 
群机器人区域覆盖算法高阶逻辑建模与验证
《小型微型计算机系统》2022年第3期475-482,共8页尹晓娜 王国辉 施智平 关永 张倩颖 张景芝 
国家重点研发计划项目(2019YFB1309900)资助;国家自然科学基金项目(61876111,61877040,62002246)资助;特区项目(18-163-11-ZT-005-038-05)资助;北京市教委科技计划一般项目(KM20190028005)资助;科技创新服务能力建设-基本科研业务费(科研费)项目(00621530290000)资助。
区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用...
关键词：群机器人 区域覆盖 高阶逻辑 定理证明 形式化验证 
全选清除导出
共9页<123456789>
检索报告 对象比较 聚类工具 使用帮助 返回顶部