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

Yoriyuki Yamagata, Weiqiang Kong, Akira Fukuda, Nguyen Van Tang, Hitoshi Ohsaki, Kenji Taguchi

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)943-962
Number of pages20
JournalFormal Aspects of Computing
Issue number5
Publication statusPublished - Sept 2014

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science


Dive into the research topics of 'A formal semantics of extended hierarchical state transition matrices using CSP#'. Together they form a unique fingerprint.

Cite this