检索结果-南通市图书馆

利用投影时序逻辑的多内核进程调度建模与验证

在线全文

学校读者我要写书评

暂无评论

西安交通大学学报 2010年第3期44卷 52-57页

作者：舒新峰段振华西安电子科技大学计算理论与技术研究所西安710071

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公... 详细信息

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.

关键词：投影时序逻辑进程调度定理证明多核处理器调度验证

在线全文

学校读者我要写书评

暂无评论

有穷时间投影时序逻辑的完备公理系统

软件学报 2011年第3期22卷 366-380页

作者：舒新峰段振华西安电子科技大学计算理论与技术研究所陕西西安710071 西安电子科技大学ISN国家重点实验室陕西西安710071 西安邮电学院计算机学院陕西西安710121

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称... 详细信息

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.

关键词：投影时序逻辑公理系统完备性证明定理证明形式化方法

在线全文

学校读者我要写书评

暂无评论

投影时序逻辑在系统建模中的应用

西北大学学报（自然科学版） 2010年第3期40卷 410-414页

作者：舒新峰段振华西安电子科技大学计算理论与技术研究所陕西西安710071

目的为了解决形式化验证时需要分别使用不同工具进行系统建模和性质描述的问题。方法利用投影时序逻辑PTL(projection temporal logic)在同一逻辑框架内完成待验证系统的建模和性质的描述。结果对PTL投影操作符的特点和用途进行了详细分... 详细信息

目的为了解决形式化验证时需要分别使用不同工具进行系统建模和性质描述的问题。方法利用投影时序逻辑PTL(projection temporal logic)在同一逻辑框架内完成待验证系统的建模和性质的描述。结果对PTL投影操作符的特点和用途进行了详细分析,并结合实例展示了PTL系统建模的使用。结论 PTL具备强大的表达能力,可广泛的应用于各类软硬件系统的验证。

关键词：投影时序逻辑系统建模形式化验证

基于扩展投影时序逻辑的组合Web服务描述与验证

在线全文

学校读者我要写书评

暂无评论

西安交通大学学报 2007年第10期41卷 1155-1159页

作者：雷丽晖段振华西安电子科技大学计算理论与技术研究所西安710071

针对编制方式生成的组合Web服务需要用一个工作流引擎执行这个特征,对投影时序逻辑进行了扩展,并用扩展投影时序逻辑描述和验证组合Web服务.将组合Web服务视为一个基于过程的工作流,将工作流引擎与组合Web服务组成部分的一次不可分割的... 详细信息

针对编制方式生成的组合Web服务需要用一个工作流引擎执行这个特征,对投影时序逻辑进行了扩展,并用扩展投影时序逻辑描述和验证组合Web服务.将组合Web服务视为一个基于过程的工作流,将工作流引擎与组合Web服务组成部分的一次不可分割的消息交互抽象为一个原子过程.用扩展投影时序逻辑公式描述原子过程,用扩展投影时序逻辑操作符定义过程组合规则、连接过程描述公式,得到组合Web服务描述公式.通过模拟组合Web执行,可验证组合Web服务满足系统的需求和性质,为提高组合Web服务设计的可靠性提供了依据.

关键词：组合Web服务投影时序逻辑形式化验证

在线全文

学校读者我要写书评

暂无评论

面向投影时序逻辑的Web服务模型检测

西安交通大学学报 2009年第4期43卷 39-43,124页

作者：王小兵段振华西安电子科技大学计算理论与技术研究所

为了满足Web服务的可靠性,利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模,用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定... 详细信息

为了满足Web服务的可靠性,利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模,用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定M和非P的合取的不可满足性,亦利用M和非P的正则形可构造合取式的正则图,判定合取的不可满足性,从而达到模型检测的目的.通过运行实例表明,所提模型检测器可验证Web服务系统性质,保证Web服务的可靠性.

关键词：形式逻辑投影时序逻辑 Web服务模型检测

在线全文

学校读者我要写书评

暂无评论

命题投影时序逻辑的判定性和表达性

命题投影时序逻辑的判定性和表达性

作者：张丽西安电子科技大学

学位级别：硕士

本文在研究了命题投影时序逻辑PPTL(Propositional Projection Temporal Logic)的语义和语法的基础上,详细阐述了它的判定过程和表达性。首先介绍了命题投影时序逻辑,包括基本的语法、语义和一些派生公式及常用逻辑等式,该逻辑除了包含... 详细信息

本文在研究了命题投影时序逻辑PPTL(Propositional Projection Temporal Logic)的语义和语法的基础上,详细阐述了它的判定过程和表达性。首先介绍了命题投影时序逻辑,包括基本的语法、语义和一些派生公式及常用逻辑等式,该逻辑除了包含有常用的逻辑操作符∨(或)和?(非)外,还包含了两个时序操作符○(next)和prj(投影操作符)。其次,本文定义了命题投影时序逻辑公式的正则形(normal form),根据公式的结构采用归纳的方法证明了任意PPTL公式都可以转换为正则形定理的正确性并且给出了相应的转换算法。该算法将所有逻辑公式都归结为一种统一的形式,这是采用Tableau方法进行判定的前提和基础。再次,为了找到给定公式的模型,本文介绍了正则图(normal form graph)的概念,给出了为PPTL公式构造正则图的算法和命题投影时序逻辑的判定过程,该方法简单实用。最后,本文介绍和比较了区间时序逻辑中两个版本的投影结构并研究了这两个投影结构的表达性,结果表明prj投影结构比原始的投影结构proj的表达性更强。

关键词：投影时序逻辑正则形正则图判定过程投影结构

基于投影时序逻辑的片上系统形式化描述和验证

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于投影时序逻辑的片上系统形式化描述和验证

作者：张鹏飞西安电子科技大学

学位级别：硕士

随着大规模集成电路技术和EDA技术的发展，片上系统(SoC)成为嵌入式系统的发展方向。片上系统带来了一些技术上的问题，对设计正确性的要求更加迫切。如何减少系统设计中的错误，提高系统设计的可靠性成为备受关注的问题。传统的设计方... 详细信息

随着大规模集成电路技术和EDA技术的发展，片上系统(SoC)成为嵌入式系统的发展方向。片上系统带来了一些技术上的问题，对设计正确性的要求更加迫切。如何减少系统设计中的错误，提高系统设计的可靠性成为备受关注的问题。传统的设计方法由于系统规范缺少精确性，而验证也不能提供百分之百的覆盖，出错的可能性很大。为了解决这个问题，形式化方法被应用在软硬件设计中。所谓形式化方法，就是利用严格的数学方法，从给出系统设计的规范开始并逐步地推导或者验证系统的方法。投影时序逻辑PTL(projection temporal logic)是一种具有离散的时间模型的时序逻辑，可处理同时具有顺序和并行的复合计算，为复杂系统的设计提供了强大的规范和证明技术。程序设计语言Extended Tempura是PTL的一个可执行的子集，可用来开发系统的原型，对系统进行模拟。本文介绍了形式化方法及投影时序逻辑和其可执行子集的基本内容，讨论了PTL对SoC不同层次的描述方法，对把状态图转换为PTL公式的问题进行了探讨，在此基础上提出基于PTL的SoC设计方法。这种方法强调系统设计中的形式描述和验证，通过在不同的设计阶段引入形式化的方法，提高系统设计的可靠性。

关键词：投影时序逻辑片上系统形式化方法