research-article

Formal semantics of extended hierarchical state transition matrix by CSP

Authors:

Kenji TaguchiAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 37, Issue 4

Pages 1 - 8

https://doi.org/10.1145/2237796.2237815

Published: 16 July 2012 Publication History

Get Access

Abstract

The Extended Hierarchical State Transition Matrix (EHSTM) is a table-based modeling language frequently used in industry for specifying behaviors of a system. However, assuring correctness, i.e., having a design satisfy certain desired properties, is a non-trivial task. To address this problem, a model checker dedicated to EHSTMs called Garakabu2 is developed. However, there is no formal justification of Garakabu2, since its semantics has never been fully formalized. In this paper, we give a formal semantics to EHSTM by translating it into CSP, Communicating Sequential Processes. Our semantics covers most of the features supported by Garakabu2. We manually translate the small examples of EHSTM to CSP, and verify them by PAT, a CSP based model checker. We also verify the examples directly using Garakabu2 and show the result are same. The experiments also show that verification using our translation and PAT is much faster than that of Garakabu2 for checking message type EHSTM.

References

[1]

Japan Embedded System Technology Association. A tantative report on questionnaires of spread of design methods 2011 (japanese). et2011_questionnaire.pdf file on JASA web site, 2012.

Google Scholar

[2]

C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Handbook of Satisability, chapter 26, pages 825--885.

Google Scholar

[3]

D. Harel and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293--333, October 1996.

Digital Library

Google Scholar

[4]

C. A. R. Hoare. Communicating Sequential Processes. By C.A.R. Hoare. Prentice-Hall International, London, 1985, viii+256 pages., volume 9. August 2004.

Google Scholar

[5]

W. Kong, N. Katahira, W. Qian, M. Watanabe, T. Katayama, and A. Fukuda. An SMT-based approach to bounded model checking of designs in communicating state transition matrix. In the 11th International Conference on Computational Science and Its Application (ICCSA 2011), pages 159--167. IEEE CS, 2011.

Digital Library

Google Scholar

[6]

W. Kong, T. Shiraishi, N. Katahira, M. Watanabe, T. Katayama, and A. Fukuda. An SMT-based approach to bounded model checking of design in state transition matrix. IEICE Transactions on Information and Systems, E94-D(5):946--957, 2011.

Google Scholar

[7]

A.W. Roscoe, C.A.R. Hoare, and R. Bird. The theory and practice of concurrency, volume 216. Prentice Hall,1998.

Google Scholar

[8]

J. Sun, Y. Liu, and J.S. Dong. Model checking CSP revisited: Introducing a process analysis toolkit. Leveraging Applications of Formal Methods, Verification and Validation, pages 307--322, 2009.

Google Scholar

[9]

A. Uselton and Scott A. Smolka. A compositional semantics for Statecharts using labeled transition systems. CONCUR'94: Concurrency Theory, 1994.

Digital Library

Google Scholar

[10]

M. Watanabe. Extended Hierarchy State Transition Matrix Design Method-Version 2.0. Technical report, CATS Technical Report, 1998.

Google Scholar

[11]

S. J. Zhang and Y. Liu. An Automatic Approach to Model Checking UML State Machines. In Secure Software Integration and Reliability Improvement Companion (SSIRI-C), 2010 Fourth International Conference on, pages 1--6. IEEE, 2010.

Digital Library

Google Scholar

Cited By

View all

Kong WLiu LYamagata YTaguchi KOhsaki HFukuda A(2012)On Accelerating SMT-based Bounded Model Checking of HSTM DesignsProceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 0110.1109/APSEC.2012.38(614-623)Online publication date: 4-Dec-2012
https://dl.acm.org/doi/10.1109/APSEC.2012.38

Recommendations

A formal semantics of extended hierarchical state transition matrices using CSP#
Abstract
The extended hierarchical state transition matrices (EHSTMs) are a table-based modelling language frequently used in industry for specifying behaviours of systems. However, assuring correctness, i.e., having a design satisfy certain desired ...
Formal Verification of Software Designs in Hierarchical State Transition Matrix with SMT-based Bounded Model Checking
APSEC '11: Proceedings of the 2011 18th Asia-Pacific Software Engineering Conference

Hierarchical State Transition Matrix (HSTM) is a table-based modeling language for developing designs of software systems. Although widely used and adopted by (particularly Japanese) software industry, there is still lack of mechanized formal ...
Formal semantics, modular specification, and symbolic verification of product-line behaviour

Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 37, Issue 4

July 2012

182 pages

ISSN:0163-5948

DOI:10.1145/2237796

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 July 2012

Published in SIGSOFT Volume 37, Issue 4

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
84
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kong WLiu LYamagata YTaguchi KOhsaki HFukuda A(2012)On Accelerating SMT-based Bounded Model Checking of HSTM DesignsProceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 0110.1109/APSEC.2012.38(614-623)Online publication date: 4-Dec-2012
https://dl.acm.org/doi/10.1109/APSEC.2012.38

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

A formal semantics of extended hierarchical state transition matrices using CSP#

Formal Verification of Software Designs in Hierarchical State Transition Matrix with SMT-based Bounded Model Checking

Formal semantics, modular specification, and symbolic verification of product-line behaviour