论文部分内容阅读
时序逻辑是一种规范语言,适合于并发系统的规范与验证,已经广泛的应用于数字电路、软件工程等领域的形式化验证中。时序逻辑程序设计语言是时序逻辑的一个可执行子集,可以将程序的书写、性质描述和验证统一在时序逻辑的框架中进行。对软硬件系统使用时序逻辑程序设计语言进行建模,对系统期望的性质采用时序逻辑公式来描述,将模型和性质统一在时序逻辑的框架中,从而实现对软硬件系统的形式化验证。现有的时序逻辑程序设计语言与传统的高级程序设计语言相比,存在形式化程度过高、缺少指针数据结构和面向对象机制等不足之处,使用这些语言进行程序设计较为不便。另外,组合Web服务的形式化验证是目前研究的一个热点,使用时序逻辑程序设计语言对组合Web服务进行建模和验证,能够将模型和性质统一在时序逻辑的框架中,给形式化验证带来了方便。本文以框架时序逻辑语言MSVL为研究对象,提出了指针数据结构的形式化方法和实现方案,给出了对象、类和继承等面向对象概念的形式化定义,并在MSVL解释器中实现了指针数据结构和面向对象机制。为了应用MSVL,研究了以OWL-S为过程描述模型的组合Web服务,提出了组合Web服务的基于MSVL的建模方法和验证方法。本文的主要贡献如下:(1)以框架时序逻辑语言MSVL为研究对象,从逻辑语言的角度出发,提出了基于名字常量的指针形式化方法和实现方案;从命令式语言的角度出发,提出了基于内容变量的指针形式化方法和实现方案。(2)在MSVL解释器中实现了基于内容变量的指针,使用指针模拟实现了引用调用的参数传递方式,使用指针实现了原地逆置单链表的程序,并使用解释器对该程序进行了基于模型检测的形式化验证。(3)对投影时序逻辑进行扩展,基于变量集合的层次化和谓词的分组,给了对象、类和继承等面向对象概念的形式化定义,并将扩展投影时序逻辑的一个可执行子集定义为面向对象MSVL。(4)提出了面向对象MSVL的解释器基本框架和实现方案,使用VisualC++/Flex/Bison实现了该解释器;使用面向对象MSVL编写数字信号处理程序,使用面向对象MSVL的解释器在仿真模式下执行该程序,从而实现了数字信号处理的仿真。(5)使用面向对象MSVL语言描述以OWL-S为过程描述模型的组合Web服务,使用命题投影时序逻辑描述期望的性质,使用面向对象MSVL的解释器在验证模式下执行带性质描述的程序,从而实现了组合Web服务基于模型检测的形式化验证。