Developing Linear-time Model-checking Technology

点击翻译按钮获取中文摘要

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.