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 - Dec 1 2012
Event2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012 - Chengdu, Sichuan, China
Duration: Oct 27 2012Oct 29 2012

Other

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

Fingerprint

Message passing
Model checking
Formal verification
Systems analysis
Communication
Experiments
Modeling languages

All Science Journal Classification (ASJC) codes

  • Information Systems

Cite this

Liu, L., Kong, W., Zhou, S., Qin, Z., & Fukuda, A. (2012). Formal verification of communicating HSTM designs. In Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012 (pp. 383-390). [6391931] https://doi.org/10.1109/CIT.2012.91

Formal verification of communicating HSTM designs. / Liu, Leyuan; Kong, Weiqiang; Zhou, Shijie; Qin, Zhiguang; Fukuda, Akira.

Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012. 2012. p. 383-390 6391931.

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

Liu, L, Kong, W, Zhou, S, Qin, Z & Fukuda, A 2012, Formal verification of communicating HSTM designs. in Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012., 6391931, pp. 383-390, 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012, Chengdu, Sichuan, China, 10/27/12. https://doi.org/10.1109/CIT.2012.91
Liu L, Kong W, Zhou S, Qin Z, Fukuda A. Formal verification of communicating HSTM designs. In Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012. 2012. p. 383-390. 6391931 https://doi.org/10.1109/CIT.2012.91
Liu, Leyuan ; Kong, Weiqiang ; Zhou, Shijie ; Qin, Zhiguang ; Fukuda, Akira. / Formal verification of communicating HSTM designs. Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012. 2012. pp. 383-390
@inproceedings{a645709a7e644fb08602adc43eef5019,
title = "Formal verification of communicating HSTM designs",
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.",
author = "Leyuan Liu and Weiqiang Kong and Shijie Zhou and Zhiguang Qin and Akira Fukuda",
year = "2012",
month = "12",
day = "1",
doi = "10.1109/CIT.2012.91",
language = "English",
isbn = "9780769548586",
pages = "383--390",
booktitle = "Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012",

}

TY - GEN

T1 - Formal verification of communicating HSTM designs

AU - Liu, Leyuan

AU - Kong, Weiqiang

AU - Zhou, Shijie

AU - Qin, Zhiguang

AU - Fukuda, Akira

PY - 2012/12/1

Y1 - 2012/12/1

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

SP - 383

EP - 390

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

ER -