Developing Linear-time Model-checking Technology

项目编号：CCR-9988322PI姓名：Vardi， Moshe y .机构：Rice university题目：开发线性时间模型检查技术项目摘要-段落：模型检查是形式验证的关键技术。正如今天普遍实践的那样，模型检查基本上是一种基于定点计算的有效符号搜索过程，用于检查设计的模型是否满足给定的ctl规范。尽管基于CTL的模型检查取得了惊人的成功，但CTL作为规范语言存在一些基本的限制，所有这些限制都源于CTL是分支时间形式主义的事实：该语言不直观且难以使用，它不适合组合推理，并且从根本上与动态验证不兼容。相比之下，线性时间框架具有表现力和直观性，支持组合推理和半形式化验证，并且可以结合枚举和符号搜索方法。令人惊讶的是，线性时间框架，即使它先于CTL，并且不受其弱点的影响，也没有享受到与CTL相同的密集研究重点，导致技术不太成熟。该项目建立在线性时间框架的理论基础上，该框架已在过去20年中奠定，并专注于产生一个知识体系，行业可以转换为强大的技术。

Proposal Number: CCR-9988322PI's Name: Vardi, Moshe Y.Institution: Rice UniversityTitle: Developing Linear-Time Model-Checking TechnologyProject-summary-paragraph:Model checking is a key technology in formal verification.As it is generally practiced today, model checking is basicallyan efficient symbolic search procedure based on fixed-point computationthat checks whether a model of the design satisfies given CTLspecifications. In spite of the phenomenal success of CTL-based modelchecking, CTL suffers from several fundamental limitations asa specification language, all stemming from the fact that CTL is abranching-time formalism: the language is unintuitive and hard touse, it does not lend itself to compositional reasoning, and it isfundamentally incompatible with dynamic validation.In contrast, the linear-time framework is expressive and intuitive,supports compositional reasoning and semi-formal verification, andis amenable to combining enumerative and symbolic search methods.Surprisingly, the linear-time framework, even though it preceded CTL,and does not suffer from its weaknesses, has not enjoyed the same intensive research focus as CTL, resulting in a much less maturetechnology. This projects builds upon the theoretical foundations ofthe linear-time framework that have been laid over the last 20 years, and focuses on generating a body of knowledge that industry can convertinto a robust technology.