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

Weiqiang Kong; Leyuan Liu; Hirokazu Yatsu; Akira Fukuda

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
出版ステータス	出版済み - 12月 1 2012
イベント	4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012 - Lisbon, ポルトガル継続期間: 11月 18 2012 → 11月 23 2012

その他

その他	4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012
国/地域	ポルトガル
City	Lisbon
Period	11/18/12 → 11/23/12

!!!All Science Journal Classification (ASJC) codes

制御およびシステム工学

他のファイルとリンク

引用スタイル

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, 4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012, Lisbon, ポルトガル, 11/18/12.

@inproceedings{b22e3a9ec10445209801f1bae83277c1,

title = "A combined formal analysis methodology and towards its application to hierarachical state transition matrix designs",

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.",

author = "Weiqiang Kong and Leyuan Liu and Hirokazu Yatsu and Akira Fukuda",

year = "2012",

month = dec,

day = "1",

language = "English",

isbn = "9781612082332",

pages = "99--106",

booktitle = "VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle",

note = "4th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2012 ; Conference date: 18-11-2012 Through 23-11-2012",

}

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/12/1

Y1 - 2012/12/1

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 - http://www.scopus.com/inward/record.url?scp=84881581177&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84881581177&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84881581177

SN - 9781612082332

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 -

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

抄録

その他

!!!All Science Journal Classification (ASJC) codes

他のファイルとリンク

フィンガープリント

引用スタイル