左正康

作品数：29被引量：63H指数：5
导出分析报告
供职机构：江西师范大学更多>>
发文主题：APLA循环不变式机械化形式化证明泛型更多>>
发文领域：自动化与计算机技术电子电信更多>>
发文期刊：《计算机时代》《郑州大学学报（理学版）》《电子学报》《江西师范大学学报（自然科学版）》更多>>
所获基金：国家自然科学基金江西省自然科学基金江西省教育厅科学技术研究项目国家留学基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于关系闭集的模糊互模拟算法函数式建模及其机械化验证
《江西师范大学学报(自然科学版)》2024年第6期640-645,共6页吴嘉伟 游珍 左正康 张晗庆 程着 
国家自然科学基金(62462036,62102171);江西省自然科学基金(20232BAB202010,20212BAB202018);江西省教育厅科学技术研究重点课题(GJJ210340,GJJ2409405)资助项目.
该文在基于关系提升的模糊互模拟算法基础上,设计了一种基于关系闭集的模糊互模拟函数式算法,并使用Isabelle/HOL定理证明器对算法的终止性和正确性进行了机械化证明,为模糊互模拟算法的形式化和自动化验证提供了参考.
关键词：模糊互模拟算法 不确定型模糊迁移系统 函数式建模 机械化验证 
多维区域匹配算法的通用验证方法
《江西师范大学学报(自然科学版)》2024年第6期646-651,共6页张晗庆 游珍 左正康 吴嘉伟 程着 
国家自然科学基金(62462036,62102171);江西省自然科学基金(20232BAB202010,20242BAB26017);江西省教育厅科学技术研究课题(GJJ210340,GJJ2409405)资助项目.
区域匹配算法通常用于多维数据空间中快速匹配特定区域或数据集,被广泛应用于数据库系统、数据分发管理系统等.目前大多数区域匹配算法的实现方法效率较低且未得到正确性验证.因此,该文提出了一种多维区域匹配算法的通用验证规约,以威...
关键词：多维区域匹配算法 威胁辐射源匹配算法 函数式建模 机械化验证 
LLRB算法的函数式建模及其机械化验证
《软件学报》2024年第11期5016-5039,共24页左正康 黄志鹏 黄箐 孙欢 曾志城 胡颖 王昌晶 
国家自然科学基金(61862033,62262031);江西省自然科学基金(20212BAB202018);江西省教育厅科技重点项目(GJJ210307)。
基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时...
关键词：LLRB 函数式建模 机械化验证 Isabelle定理证明器 二叉搜索树 
抢占式调度问题的PPTA模型与验证方法
《软件学报》2024年第10期4533-4554,共22页左正康 赵帅 王昌晶 谢武平 黄箐 
国家自然科学基金(61862033,62262031);江西省教育厅科技项目(GJJ210307,GJJ210334)。
优先级用于解决诸如在资源共享和安全设计等方面的冲突,已经成为实时系统设计中不可或缺的一部分.对于引入优先级的实时系统,每个任务都会被分配优先级,这就导致低优先级的任务在运行时可能会被高优先级的任务抢占资源,进而给实时系统...
关键词：优先级抢占式调度 抢占式优先级时间自动机 多核多任务实时系统 UPPAAL 
基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证
《通信学报》2024年第10期225-242,共18页王昌晶 欧阳俊媛 张取发 左正康 程着 卢家兴 
国家自然科学基金资助项目(No.62462037,No.62462036);江西省主要学科学术与技术带头人培养基金资助项目(No.20232BCJ22013);江西省自然科学基金资助项目(No.20242BAB26017);江西省教育厅科技基金资助项目(No.GJJ2200303,No.GJJ210340)。
为提升拍卖合约时间安全性验证效率及验证公平性,提出基于角色的拍卖合约抽象建模及其验证方法。首先,对合约源代码进行基于账户角色的抽象建模,转换为时间自动机网络模型,并对时间安全性进行形式化描述,用UPPAAL工具验证。其次,提取合...
关键词：拍卖合约 时间安全性 公平性 时间自动机 UPPAAL 
命令式动态规划类算法程序推导及机械化验证
《软件学报》2024年第9期4218-4241,共24页左正康 孙欢 王昌晶 游珍 黄箐 王唱唱 
国家自然科学基金(62262031);江西省自然科学基金(20232BAB202010,20212BAB202018);江西省教育厅科技项目(GJJ210307,GJJ210333,GJJ2200302);江西省主要学科学术与技术带头人培养项目(20232BCJ22013)。
动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Is...
关键词：Isabelle/HOL 机械化验证 动态规划 命令式 VCG 
Trie+结构函数式建模、机械化验证及其应用被引量：1
《软件学报》2024年第9期4242-4264,共23页左正康 柯雨含 黄箐 王玥坤 曾志城 王昌晶 
国家自然科学基金(62262031);江西省自然科学基金(20232BAB202010);江西省教育厅科技重点项目(GJJ210307,GJJ2200302);江西省主要学科学术与技术带头人培养项目(20232BCJ22013)。
Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.Nipkow等人给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,基...
关键词：Trie+ 函数式建模 机械化验证 多模式匹配算法 
基于模型驱动的分治并行函数式程序生成及自动验证
《信息安全学报》2023年第3期85-102,共18页王昌晶 王忠文 潘丞 黄箐 左正康 
国家自然科学基金项目(No.62262031);江西省教育厅科技重点项目(No.GJJ2200302,No.GJJ210307);江西省研究生创新基金项目(No.YC2022-s349)资助。
并行计算作为人工智能发展的动力,使得并行算法的可解释性和安全性成为人工智能领域重要研究方向。形式化方法以数理逻辑为基础,已经成为复杂安全苛求系统可信构建的重要方法,而函数式编程则在算法领域中具有更强的数学表达性。本文旨...
关键词：模型驱动 分治并行 函数式程序 程序生成 自动验证 
一种基于UPPAAL的智能合约属性形式化验证方法被引量：2
《江西师范大学学报（自然科学版）》2023年第1期45-51,共7页张取发 王昌晶 左正康 卢家兴 廖云燕 王渊 
江西省教育厅科技重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ2200304)资助项目.
针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性,...
关键词：智能合约 UPPAAL 时间自动机 安全性 活性 
基于模型驱动的Web服务建模与三阶段模型转换方法被引量：2
《计算机科学》2022年第S02期787-800,共14页王昌晶 丁希龙 陈茜 罗海梅 左正康 
国家自然科学基金(11804133,61862033);江西省教育厅科技重点项目(GJJ210307)
精确的描述Web服务的语义对Web服务的发现、执行、动态组合和交互至关重要。为支持Web服务建模,提出从抽象到具体4个模型:Radl-WS服务需求模型、Apla服务设计模型、Java可执行代码、WSDL/RESTful API。为支持模型转换,进一步提出一种三...
关键词：代数规范 模型驱动 WEB服务 建模语言 模型转换 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部