| Summary: | 碩士 === 國立臺灣師範大學 === 資訊教育研究所 === 92 === Model Checking techniques have improved considerably in past decades. In practice, there are some difficulties to apply model checking technology to software, particularly to source code directly. Not only software has more states, but also it is not easy to narrow the gap between an implementation and its model. One of the problems is how to deal with the abstract data type in source code. In this thesis we present examples to show different modeling choices can result in great differences in analysis when process behaviors are complicated by array data type. In other words, software verification is very sensitive to modeling choices. To lessen the sensitivity, we advocated the support of abstract data types in model description languages and suppressing the use of array. Encouraging the use of abstract data types can lessen the sensitivity of analysis to modeling choices and converge the process behaviors to their best for analysis.
In this work, we implement a tool named COCOV (Compositional Concurrency Verifier) supports abstract data types. We show that analysis (particularly, compositional analysis and our refactoring technique) can benefit from this tool support in an obvious way.
|
|---|
