TY - GEN
T1 - Formal verification of communicating HSTM designs
AU - Liu, Leyuan
AU - Kong, Weiqiang
AU - Zhou, Shijie
AU - Qin, Zhiguang
AU - Fukuda, Akira
N1 - Copyright:
Copyright 2013 Elsevier B.V., All rights reserved.
PY - 2012
Y1 - 2012
N2 - State Transition Matrix (STM) is a table-based modeling language for developing software system designs. Each STM abstracts a function module of the design in the form of a table, in which the behavior of the module is specified according to the dispatch of certain events on certain states. A Hierarchical STM (HSTM) consists of several STMs that are structured in a hierarchical way. A HSTM Design denote a system developed with HSTM. The STMs in a HSTM design execute asynchronously and communicate with each other through shared variables or message passing. In this paper, we present a formalization of HSTM designs that utilize message passing as the means of communication in the first place. Furthermore, based on this formalization, we propose a symbolic encoding approach, through which correctness of a HSTM design with respect to LTL properties could be represented as Bounded Model Checking (BMC) problems that could consequentially be determined by Satisfiability Modulo Theories (SMT) solving. Moreover we have implemented our encoding approach in a tool called Garakabu2 with the SMT solver CVC3 as its back-ended solver. Preliminary experiments show that counterexamples (design errors) could be discovered effectively with our method.
AB - State Transition Matrix (STM) is a table-based modeling language for developing software system designs. Each STM abstracts a function module of the design in the form of a table, in which the behavior of the module is specified according to the dispatch of certain events on certain states. A Hierarchical STM (HSTM) consists of several STMs that are structured in a hierarchical way. A HSTM Design denote a system developed with HSTM. The STMs in a HSTM design execute asynchronously and communicate with each other through shared variables or message passing. In this paper, we present a formalization of HSTM designs that utilize message passing as the means of communication in the first place. Furthermore, based on this formalization, we propose a symbolic encoding approach, through which correctness of a HSTM design with respect to LTL properties could be represented as Bounded Model Checking (BMC) problems that could consequentially be determined by Satisfiability Modulo Theories (SMT) solving. Moreover we have implemented our encoding approach in a tool called Garakabu2 with the SMT solver CVC3 as its back-ended solver. Preliminary experiments show that counterexamples (design errors) could be discovered effectively with our method.
UR - http://www.scopus.com/inward/record.url?scp=84872324284&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84872324284&partnerID=8YFLogxK
U2 - 10.1109/CIT.2012.91
DO - 10.1109/CIT.2012.91
M3 - Conference contribution
AN - SCOPUS:84872324284
SN - 9780769548586
T3 - Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012
SP - 383
EP - 390
BT - Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012
T2 - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012
Y2 - 27 October 2012 through 29 October 2012
ER -