论文部分内容阅读
随着系统设计复杂度的提高,设计验证已成为系统设计的瓶颈;传统验证技术已不能满足需要,形式化验证技术是适应这种需求而产生的新技术。形式化验证方法包括算法验证、属性验证和等价性验证等方法。论文的研究领域为属性验证。属性验证又包括定理证明、语言包含、符号模型检测等方法。常见的符号模型检测器有CTL模型检测器如SMV验证工具;LTL模型检测器如SPIN验证工具。 SPIN这一软件验证工具,是于1989年由贝尔实验室J.Holzmann等开发的模型检测器。主要面向分布式软件和协议系统的验证。SPIN使用PROMELA作为验证的模型语言,并使用线性时态逻辑（LTL）公式描述属性,应用自动机理论实现系统的模拟运行和正确性验证。 SPIN对系统的验证过程是首先用PROMELA语言建立系统的状态机模型,然后抽象出用LTL公式表示的系统需求属性的形式化描述,系统的正确性需求属性也可以在PROMELA中通过特殊标记来描述。验证的目标是判断系统模型与其抽象属性是否相符。 SystemCFL是基于进程代数ACP的SystemC语言的形式化语言。既表示了SystemC模型的语义,又是对SystemC模型中进程的行为分析。SystemCFL的目的是对SystemC设计的形式化描述以及SystemC进程的形式化行为分析。SystemCFL可对各种各样的系统建模（有限状态系统、实时系统等）。 为验证SystemCFL建模的并行及硬件系统,选择SPIN模型检测器作为验证工具。论文中通过将硬件系统的SystemCFL模型转换成PROMELA模型,然后用SPIN验证工具对模型进行验证。通过论文中研究的验证方法,可以在一定程度上实现应用SPIN模型检测器对硬件系统设计的验证。