形式化规约

作品数：25被引量：50H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：黄志球陈振庆张德运肖健宇祝义更多>>
相关机构：南京航空航天大学贺州学院西安交通大学北京大学更多>>
相关期刊：《计算机工程与设计》《中南林业科技大学学报》《制造业自动化》《高技术通讯》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划广西高校优秀人才计划项目江苏省高校自然科学研究项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于TLA+形式化规约的Raft协议测试
《软件学报》2024年第12期5363-5381,共19页王栋 窦文生 高钰 吴陈傲 魏峻 黄涛 
国家自然科学基金(62072444,62302493);国家自然科学基金联合基金(U20A6003)。
Raft是最为流行的分布式共识协议之一.自2014年被提出以来,Raft协议及其变体在各种分布式系统中被广泛应用.为了证明Raft协议的正确性,开发者使用TLA+形式化规约对协议设计进行了建模和验证.但由于抽象的形式化规约与实际的系统实现源...
关键词：RAFT 分布式系统 软件测试 模型检查 
一种基于无锁队列的运行时多线程并行验证方法被引量：1
《小型微型计算机系统》2024年第5期1249-1256,共8页李佳洁 陈哲 陈龙腾 
国家自然科学基金项目(62172217)资助;国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助。
运行时验证是一种动态的软件验证技术,主要包括使用形式化规约描述待验证性质、自动生成对应监控器以及监控器的插桩.然而现有的面向C语言程序的运行时验证技术存在一些局限性,主要体现在多监控器的情况下,现有的运行时验证工具只能使...
关键词：运行时验证 形式化规约 多线程 无锁队列 C语言程序 
时序逻辑及其表达能力综述
《华东交通大学学报》2023年第2期57-70,共14页杨科 肖美华 钟小妹 占东明 
国家自然科学基金项目(61562026,61962020);江西省主要学科学术和技术带头人计划项目(20172BCB22015);江西省教育厅科学技术研究项目(GJJ190326);江西省2020年度研究生创新专项资金项目(YC2020-B1141)。
时序逻辑是研究状态随时间变化系统的逻辑特性,在软硬件验证中有着广泛应用,是模型检测的基础。基于对时间模型的不同描述以及为了处理更加复杂的计算特征,衍生出各种时序逻辑,具有不同的表达能力,正确理解其表达能力对于系统模型的形...
关键词：时序逻辑 表达能力 形式化方法 逻辑系统 形式化规约 
以太坊智能合约定理证明中的形式化规约研究综述被引量：1
《信息网络安全》2022年第5期11-20,共10页华景煜 黄达明 
江苏省前沿引领技术基础研究专项[BK20202001]。
以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规...
关键词：以太坊 智能合约 形式化规约 形式化验证 定理证明 
面向无人驾驶时空同步约束制导的安全强化学习被引量：4
《计算机研究与发展》2021年第12期2585-2603,共19页王金永 黄志球 杨德艳 Xiaowei Huang 祝义 华高洋 
国家重点研发计划项目(2018YFB1003900);国家自然科学基金项目(61772270,62077029)。
无人驾驶系统综合了软件和硬件复杂的交互过程,在系统设计阶段,形式化方法可以保证系统满足逻辑规约和安全需求;在系统运行阶段,深度强化学习被广泛应用于无人驾驶系统决策中.然而,在面对没有经验的场景和复杂决策任务时,基于黑盒的深...
关键词：时空同步约束 形式化规约 安全强化学习 时序差分 智能交通仿真 无人驾驶安全 
汇编级顺序语句块的自动形式化规约及其验证被引量：1
《计算机工程》2019年第10期64-69,77,共7页祁龙云 吕小亮 路红 黄皓 
国家电网公司2018年总部科技项目“可信嵌入式操作系统关键技术研究”(SGJSNT00FZJS1800129)
软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语...
关键词：自动形式化规约 自动化验证 定理证明器 交互式定理 形式化验证 
参数化运行时验证研究和工具实现被引量：2
《小型微型计算机系统》2016年第12期2667-2672,共6页王哲民 陈哲 朱云龙 黄志球 
国家自然科学基金项目(61100034)资助;教育部留学回国人员科研启动基金项目(2013)资助
随着软件规模的不断增大,如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.运行时验证是一种新型的程序自动验证技术,弥补了静态分析和模型检测等常用方法的缺点.设计一种针对C程序的监控器规约语言,用于描述针对C程...
关键词：运行时验证 形式化规约 层次哈希森林 有限状态自动机 
基于PAT的使用控制模型的形式化规约与安全性分析被引量：1
《网络与信息安全学报》2016年第3期52-67,共16页周从华 陈伟鹤 刘志锋 
国家自然科学基金资助项目(No.61300228)~~
使用控制模型UCON是高度分布式、网络化的异构开放式计算环境下实现数字资源保护的新型访问控制模型。首先,利用态式时间进程代数TCSP#建立了每个UCON核模型的形式化规约,以及针对一般化UCON的组合规约机制。其次,提出了各种基于单会话...
关键词：UCON 形式化规约 安全性分析 模型检测 
基于形式化规约的缺陷规则库构建与检测方法被引量：1
《计算机工程与应用》2014年第13期66-72,102,共8页佟超 王建新 齐建东 
优秀青年教师科技支撑专项(No.YX2011-29);国家自然科学基金(No.61170268)
传统的源码缺陷分析方法存在缺陷规则有限,缺陷检测结果不明确等问题。以模型检测中的形式化规约为基础,提出一种积木式缺陷规则库构建和源码检测方法。利用元数据,用户能够通过简单的CTL逻辑操作,实现自定义待检测的缺陷种类。并且,在...
关键词：积木式模式 形式化规约 模型检测 
基于时序描述逻辑的UML顺序图形式化方法被引量：5
《计算机工程》2013年第3期36-40,共5页陈振庆 
广西壮族自治区教育厅基金资助项目(200911LX444);2010年度广西高等学校优秀人才资助计划基金资助项目
根据统一建模语言(UML)顺序图的时序特征,提出一种基于时序描述逻辑ALCQIUS的UML顺序图形式化方法。研究ALCQIUS时序扩展部分的语法和语义、ALCQIUS断言公式集一致性定理,给出ALCQIUS断言公式集一致性推理算法,并证明该推理算法的可判...
关键词：时序描述逻辑 统一建模语言顺序图 静态语义 动态语义 形式化规约 形式化验证 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部