Formal Verification of Communicating HSTM Designs

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.