投影时序逻辑

作品数：25被引量：71H指数：5
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：段振华田聪王小兵张南舒新峰更多>>
相关机构：西安电子科技大学郑州大学西安邮电学院淮北师范大学更多>>
相关期刊：《西安电子科技大学学报》《计算机技术与发展》《安徽科技学院学报》《网络安全技术与应用》更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划中央高校基本科研业务费专项资金国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
面向SQLite3数据库API调用序列的并行运行时验证方法被引量：8
《软件学报》2022年第8期2755-2768,共14页于斌 陆旭 田聪 段振华 张南 
国家重点研发计划(2018AAA0103202);国家自然科学基金(61732013,62172322,62002290);中央高校基本科研业务费专项基金(XJS210305);陕西省自然科学基础研究计划(2021JQ-208)。
作为轻量级的高可靠嵌入式数据库,SQLite3已被广泛应用于航空航天和操作系统等多个安全攸关领域,其提供了丰富灵活API函数以支持用户快速实现项目构建.然而,不正确的API函数调用序列会导致严重后果,包括运行错误、内存泄露和程序崩溃等...
关键词：SQLITE3 API调用序列 命题投影时序逻辑 并行 运行时验证 
支持索引式的PPTL定理证明器的实现被引量：1
《软件学报》2022年第6期2172-2188,共17页王小兵 寇蒙莎 李春奕 赵亮 
国家自然科学基金(61672403,61972301);陕西省重点研发计划(2020GY-043,2020GY-210)。
定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表...
关键词：定理证明 COQ 索引式 命题投影时序逻辑 公理系统 
基于运行时验证的边缘服务器DoS攻击检测方法被引量：3
《通信学报》2021年第9期75-86,共12页于斌 张南 陆旭 段振华 田聪 
国家重点研发计划基金资助项目(No.2018AAA0103202);国家自然科学基金资助项目(No.61732013,No.61806158);中央高校基本科研业务费专项资金资助项目(No.XJS210305);陕西省自然科学基础研究计划基金资助项目(No.2021JQ-208)。
针对边缘计算系统中边缘服务器面临的拒绝服务(DoS)攻击问题,提出了一种基于并行运行时验证的DoS攻击检测方法。首先,使用命题投影时序逻辑(PPTL)公式形式化描述边缘服务器预期行为和DoS攻击特征;进而,针对待验证PPTL公式,采用并行运行...
关键词：边缘计算 边缘服务器 命题投影时序逻辑 拒绝服务攻击 运行时验证 
芯片开发功能验证的形式化方法被引量：2
《软件学报》2021年第6期1799-1817,共19页姚广宇 张南 田聪 段振华 刘灵敏 孙风津 
国家重点研发计划(2018AAA0103202);国家自然科学基金(61751207,61732013);陕西省重点科技创新团队(2019TD-001)。
在芯片设计领域,采用模型驱动的FPGA设计方法是目前较为安全可靠的一种方法.但是,基于模型驱动的FPGA设计需要证明FPGA设计模型和生成Verilog/VHDL代码的一致性;同时,芯片设计的正确性、可靠性和安全性也至关重要.目前,多采用仿真方法...
关键词：芯片设计 模型驱动 功能一致性 MSVL建模 命题投影时序逻辑 
一种命题投影时序逻辑的分布式模型检测方法被引量：4
《西安电子科技大学学报》2020年第4期39-47,共9页舒新峰 王昌太 王燕 张丽丽 
国家自然科学基金(61672403,61972301);陕西省重点研发计划(2020GY-210);咸阳市科学技术研究计划(2017K01-25-8)。
为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层...
关键词：命题投影时序逻辑 模型检测 形式化验证 标记范式图 分布式计算 
一种嵌套中断系统的建模和分析方法被引量：7
《软件学报》2018年第6期1670-1680,共11页崔进 段振华 田聪 张南 
国家自然科学基金(61420106004,61732013,61572386)
在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌...
关键词：嵌套中断系统 投影时序逻辑 MSVL(modeling simulation and VERIFICATION language) 形式化建模与验证 
RTL数字系统的形式化描述
《安徽科技学院学报》2014年第6期41-46,共6页张鹏飞 
淮北市科技局人才基金项目(20120309)
本文提出对寄存器传送语言(RTL)描述的数字系统运用投影时序逻辑进行形式化描述并验证的方法。通过使用投影时序逻辑对RTL的形式语义进行定义,可把一个用寄存器传输语言描述的系统转换成投影时序逻辑的公式,从而使用投影时序逻辑可执行...
关键词：投影时序逻辑 形式化描述 寄存器传送语言 
Verilog程序的命题投影时序逻辑符号模型检测被引量：5
《西安电子科技大学学报》2014年第2期79-84,共6页逄涛 段振华 刘晓芳 
国家重点基础研究发展计划(973)资助项目(2010CB328102);国家自然科学基金资助项目(61133001)
为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法.依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程...
关键词：时序逻辑 符号模型检测 硬件描述语言 片上系统验证 
数字系统投影时序逻辑描述及验证被引量：1
《淮北师范大学学报（自然科学版）》2013年第4期61-66,共6页张鹏飞 叶永升 
淮北市科技局基金项目(20120309)
投影时序逻辑是一种具有离散时间模型的时序逻辑,其部分子集又是一种程序设计语言,可处理顺序和并发计算.文章讨论应用投影时序逻辑对数字系统进行形式描述和验证的方法,该方法可在数字系统的不同层级设计过程中,使用投影时序逻辑对其...
关键词：投影时序逻辑 形式化描述 系统验证 
进位保留加法器的命题投影时序逻辑组合验证被引量：2
《西安电子科技大学学报》2012年第5期192-196,共5页张南 段振华 
国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金资助项目(60910004;61133001;61003078;61202038;61272117);综合业务网国家重点实验室基金资助项目(ISN Lab Grant No.ISN1102001)
为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法.该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件...
关键词：时序逻辑 组合验证 进位保留加法器 超前进位加法器 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部