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: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings
Pages1003-1008
Number of pages6
Volume2
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

Other

Other12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010
CountryKorea, 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