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

摘要

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.