Home // VALID 2012, The Fourth International Conference on Advances in System Testing and Validation Lifecycle // View article

A Combined Formal Analysis Methodology and Towards Its Application to Hierarachical State Transition Matrix Designs

Authors:
Weiqiang Kong
Leyuan Liu
Hirokazu Yatsu
Akira Fukuda

Keywords: Interactive theorem proving; Bounded Model Checking; Invariant Properties; State Transition Matrix.

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.

Pages: 99 to 106

Copyright: Copyright (c) IARIA, 2012

Publication date: November 18, 2012

Published in: conference

ISSN: 2308-4316

ISBN: 978-1-61208-233-2

Location: Lisbon, Portugal

Dates: from November 18, 2012 to November 23, 2012