命题投影时序逻辑

作品数：12被引量：43H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：段振华田聪张南王小兵张琛更多>>
相关机构：西安电子科技大学西安邮电大学郑州大学武汉大学更多>>
相关期刊：《软件学报》《西安电子科技大学学报》《西安交通大学学报》《通信学报》更多>>
相关基金：国家自然科学基金中央高校基本科研业务费专项资金国家重点基础研究发展计划国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是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)。
为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层...
关键词：命题投影时序逻辑 模型检测 形式化验证 标记范式图 分布式计算 
Verilog程序的命题投影时序逻辑符号模型检测被引量：5
《西安电子科技大学学报》2014年第2期79-84,共6页逄涛 段振华 刘晓芳 
国家重点基础研究发展计划(973)资助项目(2010CB328102);国家自然科学基金资助项目(61133001)
为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法.依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程...
关键词：时序逻辑 符号模型检测 硬件描述语言 片上系统验证 
进位保留加法器的命题投影时序逻辑组合验证被引量：2
《西安电子科技大学学报》2012年第5期192-196,共5页张南 段振华 
国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金资助项目(60910004;61133001;61003078;61202038;61272117);综合业务网国家重点实验室基金资助项目(ISN Lab Grant No.ISN1102001)
为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法.该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件...
关键词：时序逻辑 组合验证 进位保留加法器 超前进位加法器 
基于事件确定有限自动机的UML2.0序列图描述与验证被引量：8
《软件学报》2011年第11期2625-2638,共14页张琛 段振华 田聪 
国家自然科学基金(60433010;60873018;60910004;91018010;61003078;61003079;61133001);国家重点基础研究发展计划(973)(2010CB328102);国家教育部博士点基金(200807010012);中央高校基本科研业务费专项资金(JY10000903004)
为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata...
关键词：UML2.0序列图 事件确定有限自动机 模型检测 命题投影时序逻辑 验证 
应用UML2.0模型的测试用例生成方法被引量：8
《西安交通大学学报》2011年第8期18-23,共6页张琛 段振华 
国家重点基础研究发展规划资助项目(2010CB328102);国家自然科学基金资助项目(60433010;60873018;60910004;91018010;61003078;61003079);教育部高等学校博士学科点专项科研基金资助项目(200807010012);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对软件开发过程中测试自动化程度低的问题,在研究基于模型的测试用例生成技术的基础上,提出了一种基于UML2.0序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证...
关键词：测试用例 命题投影时序逻辑 模型检测 覆盖准则 
基于命题投影时序逻辑的单调速率调度算法模型检测被引量：3
《软件学报》2011年第2期211-221,共11页田聪 段振华 
国家自然科学基金(61003078;91018010;60873018;60910004);国家重点基础研究发展计划(973)(2010CB328102);教育部博士点基金(200807010012);中央高校基本科研业务费专项资金(JY10000903004)
提出了基于命题投影时序逻辑(propositional projection temporal logic,简称PPTL)的单调速率调度(rate monotonic scheduling,简称RMS)模型检测方法.该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模,使用PPTL描述系...
关键词：时序逻辑 模型检测 单调速率调度算法 验证 实时系统 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部