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

Fingerprint

Demonstrations
Internet
Control systems
Modeling languages

All Science Journal Classification (ASJC) codes

  • Electrical and Electronic Engineering

Cite this

Kong, W., Shiraishi, T., Mizushima, Y., Katahira, N., Fukuda, A., & Watanabe, M. (2010). Formal analysis of STM design with SAL infinite bounded model checker. In 12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings (Vol. 2, pp. 1003-1008). [5440212]

Formal analysis of STM design with SAL infinite bounded model checker. / Kong, Weiqiang; Shiraishi, Tomohiro; Mizushima, Yuki; Katahira, Noriyuki; Fukuda, Akira; Watanabe, Masahiko.

12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings. Vol. 2 2010. p. 1003-1008 5440212.

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

Kong, W, Shiraishi, T, Mizushima, Y, Katahira, N, Fukuda, A & Watanabe, M 2010, Formal analysis of STM design with SAL infinite bounded model checker. in 12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings. vol. 2, 5440212, pp. 1003-1008, 12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010, Korea, Republic of, 2/7/10.
Kong W, Shiraishi T, Mizushima Y, Katahira N, Fukuda A, Watanabe M. Formal analysis of STM design with SAL infinite bounded model checker. In 12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings. Vol. 2. 2010. p. 1003-1008. 5440212
Kong, Weiqiang ; Shiraishi, Tomohiro ; Mizushima, Yuki ; Katahira, Noriyuki ; Fukuda, Akira ; Watanabe, Masahiko. / Formal analysis of STM design with SAL infinite bounded model checker. 12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings. Vol. 2 2010. pp. 1003-1008
@inproceedings{134122c1fb644bb3bcc5175bf5ddef8c,
title = "Formal analysis of STM design with SAL infinite bounded model checker",
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.",
author = "Weiqiang Kong and Tomohiro Shiraishi and Yuki Mizushima and Noriyuki Katahira and Akira Fukuda and Masahiko Watanabe",
year = "2010",
language = "English",
isbn = "9788955191455",
volume = "2",
pages = "1003--1008",
booktitle = "12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings",

}

TY - GEN

T1 - Formal analysis of STM design with SAL infinite bounded model checker

AU - Kong, Weiqiang

AU - Shiraishi, Tomohiro

AU - Mizushima, Yuki

AU - Katahira, Noriyuki

AU - Fukuda, Akira

AU - Watanabe, Masahiko

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=77952476205&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77952476205&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:77952476205

SN - 9788955191455

VL - 2

SP - 1003

EP - 1008

BT - 12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings

ER -