{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:50:37Z","timestamp":1750308637358,"version":"3.41.0"},"reference-count":10,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,7,16]],"date-time":"2012-07-16T00:00:00Z","timestamp":1342396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2012,7,16]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/2237796.2237815","type":"journal-article","created":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T17:35:16Z","timestamp":1343842516000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal semantics of extended hierarchical state transition matrix by CSP"],"prefix":"10.1145","volume":"37","author":[{"given":"Yoriyuki","family":"Yamagata","sequence":"first","affiliation":[{"name":"National Institute of Advanced Science and Technology, Amagasaki"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiqiang","family":"Kong","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akira","family":"Fukuda","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Van Tang","family":"Nguyen","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Science and Technology, Amagasaki"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hitoshi","family":"Ohsaki","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Science and Technology, Amagasaki"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenji","family":"Taguchi","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Science and Technology, Amagasaki"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,7,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"A tantative report on questionnaires of spread of design methods 2011 (japanese). et2011_questionnaire.pdf file on JASA web site","author":"Japan Embedded System Technology Association","year":"2012","unstructured":"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 . 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."},{"key":"e_1_2_1_2_1","first-page":"825","volume-title":"Handbook of Satisability","author":"Barrett C.","unstructured":"C. Barrett , R. Sebastiani , S. Seshia , and C. Tinelli . Handbook of Satisability , chapter 26, pages 825 -- 885 . C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Handbook of Satisability, chapter 26, pages 825--885."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"e_1_2_1_4_1","volume-title":"Communicating Sequential Processes. By C.A.R. Hoare","author":"Hoare C. A. R.","year":"1985","unstructured":"C. A. R. Hoare . Communicating Sequential Processes. By C.A.R. Hoare . Prentice-Hall International , London , 1985 , viii+256 pages., volume 9 . August 2004. C. A. R. Hoare. Communicating Sequential Processes. By C.A.R. Hoare. Prentice-Hall International, London, 1985, viii+256 pages., volume 9. August 2004."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCSA.2011.30"},{"key":"e_1_2_1_6_1","author":"Kong W.","year":"2011","unstructured":"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 . 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.","journal-title":"IEICE Transactions on Information and Systems, E94-D(5):946--957"},{"key":"e_1_2_1_7_1","volume-title":"The theory and practice of concurrency","author":"Roscoe A.W.","year":"1998","unstructured":"A.W. Roscoe , C.A.R. Hoare , and R. Bird . The theory and practice of concurrency , volume 216 . Prentice Hall , 1998 . A.W. Roscoe, C.A.R. Hoare, and R. Bird. The theory and practice of concurrency, volume 216. Prentice Hall,1998."},{"key":"e_1_2_1_8_1","first-page":"307","volume-title":"Verification and Validation","author":"Sun J.","year":"2009","unstructured":"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 . 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."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646729.703535"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SSIRI-C.2010.11"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2237796.2237815","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2237796.2237815","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:08:07Z","timestamp":1750273687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2237796.2237815"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,16]]},"references-count":10,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,7,16]]}},"alternative-id":["10.1145\/2237796.2237815"],"URL":"https:\/\/doi.org\/10.1145\/2237796.2237815","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,7,16]]},"assertion":[{"value":"2012-07-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}