Formal analysis of STM design with SAL infinite bounded model checker

Weiqiang Kong, Tomohiro Shiraishi, Yuki Mizushima, Noriyuki Katahira, Akira Fukuda, Masahiko Watanabe

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

Abstract

State Transition Matrix (STM) is a flexible table-like modeling language that has been frequently used for specifying behavior of distributed systems. In this paper, we first present a formalization of the static and dynamic aspects of a STM design (i.e., design written in STM). Consequentially, based on this formalization, we investigate how a STM design can be formally analyzed using SAL, precisely SAL infinite bounded model checker, through a language translation. Specifically, the formal analysis is conducted focusing on four kinds of safety properties related to: (1) Invalid Cells, (2) Static Constraints, (3) Dynamic Constraints, and (4) Deadlock, respectively, since the fulfillment of these properties is commonly desired by industrial practitioners for a STM design. A simple Internet Connection Control system is used as our demonstration example.

Original languageEnglish
Title of host publication12th International Conference on Advanced Communication Technology
Subtitle of host publicationICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings
Pages1003-1008
Number of pages6
Publication statusPublished - 2010
Event12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - , Korea, Republic of
Duration: Feb 7 2010Feb 10 2010

Publication series

NameInternational Conference on Advanced Communication Technology, ICACT
Volume2
ISSN (Print)1738-9445

Other

Other12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010
Country/TerritoryKorea, Republic of
Period2/7/102/10/10

All Science Journal Classification (ASJC) codes

  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Formal analysis of STM design with SAL infinite bounded model checker'. Together they form a unique fingerprint.

Cite this