Mutation Coverage Estimation for Symbolic Model Checking

• Main Authors: Te-Chang Lee, 李德昌
• Other Authors: Pao-Ann Hsiung
• Format: Others
• Language: en_US
• Published: 2004
• Online Access: http://ndltd.ncl.edu.tw/handle/73344078156887096871

碩士 === 國立中正大學 === 資訊工程研究所 === 92 === When people design a system, there is always a question about how exhaustive the system has been examined to be right. Coverage estimation provides an answer to this question in simulation. A model checker verifies a design exhaustively, and proves the satisfaction of specifications. However, people have noticed that errors exist even after verification is done. In recent years, formal techniques set feet to this field for the same reason "\How complete is the formal verification once done?". We proposed an intuitive way to estimate the completeness of formal verification. Once a system satisfies a specification, we estimate the coverage of completeness for a set of properties by applying some mutations to a system model and calculate its relevance to the given properties. Several mutation models are employed to exploit the estimation. Our experience on some real cases will demonstrate how our methodology helps verification engineers to find the uncovered hole.