【作者】 王小兵；

【导师】 段振华；

【作者基本信息】 西安电子科技大学 ， 计算机应用技术， 2009， 博士

【摘要】 时序逻辑是一种规范语言,适合于并发系统的规范与验证,已经广泛的应用于数字电路、软件工程等领域的形式化验证中。时序逻辑程序设计语言是时序逻辑的一个可执行子集,可以将程序的书写、性质描述和验证统一在时序逻辑的框架中进行。对软硬件系统使用时序逻辑程序设计语言进行建模,对系统期望的性质采用时序逻辑公式来描述,将模型和性质统一在时序逻辑的框架中,从而实现对软硬件系统的形式化验证。现有的时序逻辑程序设计语言与传统的高级程序设计语言相比,存在形式化程度过高、缺少指针数据结构和面向对象机制等不足之处,使用这些语言进行程序设计较为不便。另外,组合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服务基于模型检测的形式化验证。更多还原

【Abstract】 Temporal logic is a specification language which is suitable for specification andverification of concurrent systems, and it has been widely used in the formalverification of digital circuits and software engineering. A temporal logic programminglanguage is an executable subset of temporal logic, and it provides a framework inwhich writing of programs, properties of programs, and verification of programs canall be treated within temporal logic. The temporal logic programming languages areused to model software and hardware, and temporal logic formulas are used to describedesired properties, thus the model and properties are both in temporal logic, and thenthe formal verification of software and hardware can be performed.Compared with traditional high-level programming languages, the existingtemporal logic programming languages have some shortages such as highformalization, lack of the pointers and object-oriented mechanisms, and it isinconvenience to program in these languages. In addition, the formal verification ofcomposite Web Services is a research focus at present. The temporal logicprogramming languages can be used to model and verify composite Web Services, thusthe model and properties are both in temporal logic which brings conveniences to theformal verification.This dissertation mainly focuses on the framed temporal logic programminglanguage MSVL, and proposes the formalization and implementation of pointers. Theformal definitions of object-oriented concepts such as objects, classes and inheritancesare given. Then an interpreter for MSVL has been developed to support pointers andobject-oriented mechanisms. In order to apply MSVL, the composite Web Servicesbased on the OWL-S process model are analyzed, and a modeling and verificationmethod of composite Web Services based on MSVL is proposed.The main contributions of this dissertation are as follows:(1) The framed temporal logic programming language MSVL is analyzed, and theformalization and implementation of pointers based on name constants are proposedfrom the point of view of logic languages, then the formalization and implementation ofpointers based on content variables are also proposed from the point of view ofimperative languages.(2) The pointers based on content variables are implemented in the interpreter forMSVL. Pointers are used to simulate parameter passing by reference and are used in theprogram for in place reversal of singly linked list, and then the program is verified via model checking with the interpreter.(3) Projection Temporal Logic is extended, and then formal definitions ofobject-oriented concepts such as objects, classes and inheritances are given based on thehierarchical variable sets and grouping predicates. Object-oriented MSVL is defined asan executable subset of Extended Projection Temporal Logic.(4) The basic framework and design plan of the interpreter for object-orientedMSVL are proposed, and the interpreter has been developed in Visual C++/Flex/Bison.A program for digital signal processing is written in object-oriented MSVL, and theinterpreter for object-oriented MSVL is used to execute it in simulation mode tosimulate digital signal processing.(5) Object-oriented MSVL is used to model the composite Web Services based onthe OWL-S process model, and Propositional Projection Temporal Logic is used todescribe desired properties, thus the interpreter for object-oriented MSVL executes theprograms with properties in verification mode to verify the composite Web Servicesvia model checking.更多还原