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

Weiqiang Kong, Leyuan Liu, Hirokazu Yatsu, Akira Fukuda

研究成果: 書籍/レポート タイプへの寄稿会議への寄与

抄録

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.

本文言語英語
ホスト出版物のタイトルVALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle
ページ99-106
ページ数8
出版ステータス出版済み - 2012
イベント4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012 - Lisbon, ポルトガル
継続期間: 11月 18 201211月 23 2012

出版物シリーズ

名前VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle

その他

その他4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012
国/地域ポルトガル
CityLisbon
Period11/18/1211/23/12

!!!All Science Journal Classification (ASJC) codes

  • 制御およびシステム工学

フィンガープリント

「A combined formal analysis methodology and towards its application to hierarachical state transition matrix designs」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル