Formal analysis of STM design with SAL infinite bounded model checker

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

Formal analysis of STM design with SAL infinite bounded model checker

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

Advanced Software Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - Proceedings
Pages	1003-1008
Number of pages	6
Volume	2
Publication status	Published - 2010
Event	12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 - , Korea, Republic of Duration: Feb 7 2010 → Feb 10 2010

Other

Other	12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010
Country/Territory	Korea, Republic of
Period	2/7/10 → 2/10/10

All Science Journal Classification (ASJC) codes

Electrical and Electronic Engineering

Cite this

Formal analysis of STM design with SAL infinite bounded model checker. / Kong, Weiqiang; Shiraishi, Tomohiro; Mizushima, Yuki et al.
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 proceeding › Conference 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.

@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",

note = "12th International Conference on Advanced Communication Technology: ICT for Green Growth and Sustainable Development, ICACT 2010 ; Conference date: 07-02-2010 Through 10-02-2010",

}

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

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

Y2 - 7 February 2010 through 10 February 2010

ER -

Formal analysis of STM design with SAL infinite bounded model checker

Abstract

Other

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this