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

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

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

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

命题投影时序逻辑并发建模与自动验证

针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.     

基于PPTL的着色Petri网的模型检测方法

为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法。通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足。利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力。     

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

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

基于安全灰箱演算的物联网移动性建模验证

物联网的建模和验证是物联网研究的一个重要领域。由于集成了物理进程,物联网表现出传统软件系统所不具备的物理特性。这些性质作为物联网系统中必不可少的一部分,必须在物联网模型中进行描述。移动性作为一种物理属性,能够描述物联网中物理实体的移动以及信息的流动,本文对物联网的移动性进行研究,提出了一种基于安全灰箱演算的物联网模型,并且使用灰箱逻辑对其进行分析验证。该方法能够对物联网的移动性进行描述分析,适用于具有移动特征的物联网应用。以欧洲火车控制系统(ETCS)为例,验证了本文建模和验证方法的可行性。     

PPTL模型检测器实现的一个关键技术

针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.     

基于原型验证系统的自稳定算法形式化验证

介绍了分布式系统的自稳定性以及原型验证系统(PVS),阐述了从形式化角度验证系统性质的方法.使用PVS对分布式系统及系统中的自稳定算法进行形式化描述和建模,并成功地证明了系统的自稳定性.同时,通过机械化的验证和分析结果,可以得出形式化证明的优势.     

铁路系统的模型检查和参数分析

研究铁路系统的自动验证技术，建立火车和控制器的混合自动机模型，用时态逻辑ＩＣＴＬ描述铁路系统的性质规范，使用模型检查技术自动验证铁路系统，并且对铁路系统的一些参数进行分析。     

用于C语言程序验证的性质描述语言C-PDL

为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式.