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

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

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

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

时序逻辑控制的多席位任务协同调度算法

针对指挥控制方舱多席位任务协同的时效性问题,从时间和状态的角度,把复杂的指挥控制过程进行描述和任务编码,以任务树和任务执行甘特图的形式,建立了基于任务时序排列的多席位任务协同模型,并利用空闲事件驱动策略,提出了针对该模型的时序逻辑调度算法。实例仿真分析表明:相对于传统方式,算法使系统协同过程总的空闲时间减少了9%,任务整体并行执行时间减少了4.6%,该模型和算法能很好地描述和优化指挥控制过程中的多席位任务协同过程,减少任务协同过程中的空闲时间和任务整体并行执行时间,从而提高作战效率。     

基于线性时序逻辑的业务流程验证

目的为了解决业务流程设计与需求的不一致性问题。方法提出了一种基于XML过程定义语言和线性时序逻辑的业务流程验证方法。结果采用Promela语言描述业务流程模型,线性时序逻辑表示抽象的业务需求,通过模型检测器Spin完成流程的验证工作。结论实现了对流程正确性的判断。     

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

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

面向命题投影时序逻辑的安全协议模型检测

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.     

单向通信保密系统的时序逻辑验证

探讨了形式化验证加密协议的方法，用时序逻辑验证了单向保密协议的安全性缺陷。     

Linux 2.6内核进程调度策略与算法分析

Linux 2.6内核采用了新开发的调度器,该调度器基于O（1）算法。新的调度器基于每个CPU来分布时间片,并且取消了全局同步和重算循环。文中详细分析了新的调度器策略和算法,最后进行了总结。     

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

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

软件体系结构动态特征建模与验证

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.     

时态逻辑的比较与分析

对时态逻辑的两种重要形式———线性时态逻辑与分支时态逻辑进行了比较和分析,指出它们各自的特点及适用范围。     

基于事件逻辑的炼油企业动态调度系统

针对炼油生产动态调度问题,开发了基于事件逻辑的调度优化系统.在分析大量实际生产事件和调度专家处理经验的基础上定义动态事件,生成事件逻辑.将事件逻辑与广义析取规划相结合,建立了基于事件逻辑的动态调度模型.基于事件逻辑的动态调度建模方法增加了动态调度模型生成的快速性和灵活性,在保证调度优化性的同时获得较好的调度实时性.最后,以某炼油厂"原油供应不足"事件为例进行仿真实验.结果表明,基于事件逻辑的动态调度系统是可行、有效的.     

基于逻辑的形式化验证方法: 进展及应用

近年来, 形式化方法发展很快, 一些技术已经产生工业应用。以逻辑系统为主线, 分析几个影响力比较大的形式化验证技术和验证工具, 以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT, 谓词逻辑方面的ACL2、VDM方法和B方法, 以及高阶逻辑方面的HOL、PVS 和COQ。还介绍形式化方法在学术界和工业界的应用情况, 最后给出几个商业化的形式化验证工具。     

业务流程的形式化设计与验证

针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.      

基于时态通讯图的启发式任务调度

在基于消息传递系统的显式并行程序设计环境下,用通常的前趋任务图有时很难精确表示任务间的偏序关系．本文首先提出了时态通讯图这一基本概念,然后说明了用ＴＣＧ表示并行程序任务间相互作用关系的一般方法以及ＴＣＧ的一些基本性质,并给出了基于ＴＣＧ的启发式任务调度方法．     

基于行为时序逻辑TLA的安全协议形式化分析与检测

随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。     

一种基于超连接的一阶逻辑反演推理算法

研究一种一阶谓词逻辑公式的反演求证算法,它是应用超连接过程来处理子句集的消解的,该算法具有比Ｒｏｂｉｎｓｏｎ的传统消解方法更高的效率．以一个实例讨论了该算法的应用,结果表明此算法可以保证在预定义的相关边界内,对任意一阶逻辑的推理具有终止性     

一种基于模糊逻辑优先级的雷达任务自适应调度算法

为适应目标环境变化情况,提出了一种基于模糊逻辑优先级的雷达任务自适应调度算法.该方法基于目标运动状态和属性通过模糊逻辑推理动态确定任务的优先级,并结合时间窗的特点采用一步回溯方法调整发生冲突的任务,保证更多高优先级的任务在其期望的时间内被调度.仿真结果表明,该调度算法在保证调度率的前提下降低了任务的调度代价.     

Verification of Interdomain Routing System Based on Formal Methods

In networks,the stable path problem (SPP) usually results in oscillations in interdomain systems and may cause systems to become unstable.With the rapid development of internet technology,the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research.A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software.Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method's effectiveness.Linear temporal logic was used to model an interdomain routing system and its properties were analyzed.An example is included to demonstrate the method's reliability.