TY - GEN
T1 - A combined formal analysis methodology and towards its application to hierarachical state transition matrix designs
AU - Kong, Weiqiang
AU - Liu, Leyuan
AU - Yatsu, Hirokazu
AU - Fukuda, Akira
PY - 2012
Y1 - 2012
N2 - Interactive theorem proving and model checking are known as two formal verification techniques that have complementary features and aims, but overlapping application areas. In this paper, we investigate a procedure (methodology) called Combined Falsification and Verification (CFV), by which the benefits of both interactive theorem proving and model checking could be enjoyed for formal analysis of software systems against invariant properties. We have been developing a SMT-based Bounded Model Checker called Garakabu2 for falsification of HSTM designs. Interfaces necessary for enabling the procedure CFV is planned to be introduced into Garakabu2 for providing an auxiliary functionality for users of Garakabu2 who are experts in formal methods.
AB - Interactive theorem proving and model checking are known as two formal verification techniques that have complementary features and aims, but overlapping application areas. In this paper, we investigate a procedure (methodology) called Combined Falsification and Verification (CFV), by which the benefits of both interactive theorem proving and model checking could be enjoyed for formal analysis of software systems against invariant properties. We have been developing a SMT-based Bounded Model Checker called Garakabu2 for falsification of HSTM designs. Interfaces necessary for enabling the procedure CFV is planned to be introduced into Garakabu2 for providing an auxiliary functionality for users of Garakabu2 who are experts in formal methods.
UR - https://www.scopus.com/pages/publications/84881581177
UR - https://www.scopus.com/pages/publications/84881581177#tab=citedBy
M3 - Conference contribution
AN - SCOPUS:84881581177
SN - 9781612082332
T3 - VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle
SP - 99
EP - 106
BT - VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle
T2 - 4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012
Y2 - 18 November 2012 through 23 November 2012
ER -