Development of Coverage Metric for Formal Property Verification

2020 Fiscal Year Final Research Report

• Project/Area Number: 17K00089
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Computer system
• Research Institution: Ishikawa National College of Technology
• Principal Investigator: Matsumoto Takeshi 石川工業高等専門学校, 電子情報工学科, 准教授 (40536140)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Keywords: プロパティ検証 / 回路検証

Outline of Final Research Achievements

Property checking, which is a kind of formal verification of state transition systems, verifies that a system under verification satisfies a given property for any input patterns. In this work, we propose a verification coverage of property checking to estimate how much sufficiently a system is verified. Our proposed coverage is based on a ratio of state transitions which affects verification results. A state transition is considered to be covered by a property when the result of property checking differs from the original result by removing the transition. We proposed a coverage metric based on this idea and showed evaluation results for example systems and properties.

Free Research Field

VLSI設計支援

Academic Significance and Societal Importance of the Research Achievements

現在、多くの電子情報機器は大規模なシステムであり、その正しさの検証を効率的に行うことが重要になっている。検証においては、検証対象システムの一部だけを検証しても誤り(バグ)を全て見つけることができないため、どの程度網羅的に検証が行われているかを把握することが必要である。本研究では、システム検証の一種であるプロパティ検証を対象として、検証がどの程度網羅的に行われているかを示す指標を提案し、いくつかの例題において評価を行った。これにより、どれ程のプロパティを検証すれば十分であるかを知る指標とすることができ、さらには、検証結果に対する信頼性・説明可能性が高まることが期待できる。