Formal verification of communicating HSTM designs

Leyuan Liu, Weiqiang Kong, Shijie Zhou, Zhiguang Qin, Akira Fukuda

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012
Pages383-390
Number of pages8
DOIs
Publication statusPublished - 2012
Event2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012 - Chengdu, Sichuan, China
Duration: Oct 27 2012Oct 29 2012

Publication series

NameProceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012

Other

Other2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012
CountryChina
CityChengdu, Sichuan
Period10/27/1210/29/12

All Science Journal Classification (ASJC) codes

  • Information Systems

Fingerprint Dive into the research topics of 'Formal verification of communicating HSTM designs'. Together they form a unique fingerprint.

Cite this