国家自然科学基金(61163001)

作品数：16被引量：13H指数：2
导出分析报告
相关作者：龙士工杨世平潘怀宇郑涵张珺铭更多>>
相关机构：贵州大学贵州商学院毕节学院中国人民大学更多>>
相关期刊：《计算机工程与设计》《计算机与数字工程》《计算机应用研究》《贵州大学学报（自然科学版）》更多>>
相关主题：行为时序逻辑语言UML模型UML敏捷开发更多>>
相关领域：自动化与计算机技术经济管理更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种基于双线性对的云存储数据安全保护协议被引量：2
《贵州大学学报（自然科学版）》2017年第5期66-70,共5页刘田天 龙士工 冯金明 
国家自然科学基金项目资助(61163001)
针对支持公开验证的云存储模式中用户的数据隐私有可能泄露给第三方审计(TPA)的问题,为保护用户云端数据隐私和数据完整,提出一个基于双线性映射的云端数据完整性检测协议。该协议利用哈希函数单向性的性质,云存储服务器收到第三方审计...
关键词：云存储 数据完整性 数据隐私保护 双线性映射 公开验证 
基于新型分割技术的文件云存储被引量：2
《贵州大学学报（自然科学版）》2017年第2期76-79,共4页刘昊 杨世平 
国家自然科学基金项目(61163001)
本文探讨了云存储的常规安全机制上的一些漏洞,针对这些问题,通过改进现行的文件分割技术,提出了一种新的文件分割方法。并从理论的角度论述了新方案的可行性和优缺点,同时论证了新方案可以进一步增强文件云存储的安全性。
关键词：文件分割技术 云存储 云安全 
基于Zigbee和BPLC双模的智慧家庭自动化系统设计被引量：2
《贵州大学学报（自然科学版）》2017年第1期66-71,共6页张乾 杨世平 
国家自然科学基金(61163001)安全协议行为时序逻辑验证与公平约束下的模型检测
根据我国智慧产业的需求与发展方向,以智慧家庭引领智慧生活,提出了一种基于Zigbee和宽带电力线载波通信技术(BPLC)双模的智慧家庭自动化系统方案,给出了其系统模型图,介绍了Zigbee和BPLC关键技术,并结合二者的特点,采用CC2420芯片和QCA...
关键词：智慧家庭 ZIGBEE BPLC 自动化系统 控制 
模型检测空间分解分布式算法的优化与研究
《贵州大学学报（自然科学版）》2016年第3期86-90,共5页潘怀宇 龙士工 郑涵 
国家自然科学基金(61163001)
模型检测对于系统的校验有着适用范围广、自动化验证程度高、验证速度快等优势。但是其状态爆炸问题制约了其应用,使用分布式技术缓解状态爆炸问题引来了新的问题——如何对状态空间进行分解。本文介绍了分布式SCC分解的两个算法:FB与MP...
关键词：模型检测 状态爆炸 OWCTY 分布式技术 
基于DivinE的分布式模型检测及协议验证被引量：1
《贵州大学学报（自然科学版）》2016年第3期91-95,共5页郑涵 龙士工 潘怀宇 刘照祥 
国家自然科学基金(61163001)
模型检测是一个高效且简单的方法来检测一个并发程序是否满足一个时序逻辑公式,它基于对系统状态空间的穷举搜索,通常采用深度优先搜索算法(DFS)。然而由于DFS算法固有的连续性,并且需要用到某些数据结构和同步机制,使得计算机的资源被...
关键词：模型检测 DFS 状态爆炸 分布式 DivinE 
一种基于TLA的解决N皇后问题的方法
《贵州大学学报（自然科学版）》2016年第1期86-88,共3页台亚非 龙士工 
国家自然科学基金项目资助(61163001)
行为时序逻辑语言(TLA+)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。N皇后问题是一个久远的问题,回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA+去描述N皇后问题,然后使用Toolbox工具去检测n=5...
关键词：行为时序逻辑 模型检测 N皇后问题 TOOLBOX 
基于行为时序逻辑TLA的Pastry协议的规约与验证
《贵州大学学报（自然科学版）》2015年第6期79-82,87,共5页刘照洋 龙士工 
国家自然科学基金项目资助(61163001)
本文研究基于行为时序逻辑TLA的模型检测技术,阐述TLA的语义、语法和公平性问题。用基于TLA的系统描述语言TLA+对Pastry协议及其属性进行规约并用模型检测工具TLC对其进行验证。
关键词：模型检测 PASTRY TLA TLC 
基于偏序规约技术的网络程序JPF验证
《计算机工程与设计》2014年第6期2004-2008,共5页杨翰文 龙士工 谢光颖 
国家自然科学基金项目(61163001)
为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案。针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案。该方...
关键词：模型检测 状态爆炸 偏序规约 on-the-fly技术 程序验证 
无线移动终端的SAV协议的形式化建模与模型检测
《计算机应用研究》2014年第6期1877-1879,1882,共4页谢光颖 龙士工 杨翰文 
国家自然科学基金资助项目(61163001)
公钥数字签名方案中验证方是低运算能力的移动智能设备时,验证方在验证过程中需要借助于服务器来辅助验证。SAV(server-aided verification)协议是一个对无线移动终端实现辅助计算和签名验证的协议,利用有限状态机对该协议中签名方、验...
关键词：服务器辅助验证协议 模型检测 NuSMV工具 有限状态机 计算树逻辑 
一种安全转移系统模型的构造及其运用
《计算机应用研究》2014年第2期558-562,共5页万良 肖源 
国家自然科学基金资助项目(61163001);中国人民大学科学研究基金(中央高校基本科研业务费专项资金资助)项目成果(+12 XNLF06);贵州自然科学基金项目(J[2011]2328)
为提高安全性,一般利用密码技术,但系统运行过程的安全尚显不足,为此基于行为时序逻辑TLA提出一种安全转移系统模型。通过设置安全属性,构造安全行为,使得系统在运行过程中的每次转移都满足安全属性,从而提高过程的安全性。为此,定义初...
关键词：形式化方法 行为时序逻辑 安全性 安全行为 安全转移系统 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部