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

5Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

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 properties, is a non-trivial task. To address this problem, a model checker dedicated to EHSTMs called Garakabu2 has been developed. However, there is no formal justification for Garakabu2, since its semantics has never been fully formalised. In this paper, we give a formal semantics to EHSTMs by translating them into CSP, Communicating Sequential Processes. Among the variants of CSP, we use CSP#, which is the modelling language used by PAT model checker, as a target of translation. Our semantics covers most of the features supported by Garakabu2. We manually translate the small examples of EHSTMs to CSP#, and verify them by PAT. We also verify the examples directly using Garakabu2 and show that the results are same. The experiments also indicate that verification using our translation and PAT is much faster than that of Garakabu2 in some cases. © 2013 British Computer Society.

References Powered by Scopus

The model checker SPIN

2895Citations
N/AReaders
Get full text

Symbolic model checking without BDDs

1608Citations
N/AReaders
Get full text

Symbolic model checking: 10<sup>20</sup> States and beyond

1179Citations
N/AReaders
Get full text

Cited by Powered by Scopus

Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC

9Citations
N/AReaders
Get full text

Towards sustainable information infrastructure platform for smart mobility - Project overview

9Citations
N/AReaders
Get full text

Toward sustainable smart mobility information infrastructure platform: Project overview

2Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

Yamagata, Y., Kong, W., Fukuda, A., Van Tang, N., Ohsaki, H., & Taguchi, K. (2014). A formal semantics of extended hierarchical state transition matrices using CSP#. Formal Aspects of Computing, 26(5), 943–962. https://doi.org/10.1007/s00165-013-0282-7

Readers over time

‘15‘16‘17‘18‘19‘2000.511.52

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 4

80%

Researcher 1

20%

Readers' Discipline

Tooltip

Computer Science 6

75%

Engineering 2

25%

Save time finding and organizing research with Mendeley

Sign up for free
0