A combined formal analysis methodology and towards its application to hierarachical state transition matrix designs

Weiqiang Kong, Leyuan Liu, Hirokazu Yatsu, Akira Fukuda

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationVALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle
Pages99-106
Number of pages8
Publication statusPublished - Dec 1 2012
Event4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012 - Lisbon, Portugal
Duration: Nov 18 2012Nov 23 2012

Other

Other4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012
CountryPortugal
CityLisbon
Period11/18/1211/23/12

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering

Cite this

Kong, W., Liu, L., Yatsu, H., & Fukuda, A. (2012). A combined formal analysis methodology and towards its application to hierarachical state transition matrix designs. In VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle (pp. 99-106)