{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T04:09:53Z","timestamp":1648872593541},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T00:00:00Z","timestamp":1409529600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-013-0282-7","type":"journal-article","created":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T08:48:05Z","timestamp":1379321285000},"page":"943-962","source":"Crossref","is-referenced-by-count":5,"title":["A formal semantics of extended hierarchical state transition matrices using CSP#"],"prefix":"10.1145","volume":"26","author":[{"given":"Yoriyuki","family":"Yamagata","sequence":"first","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology (AIST), Nakoji 3-11-46, 661-0974, Amagasaki, Hyogo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiqiang","family":"Kong","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akira","family":"Fukuda","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nguyen","family":"Van Tang","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology (AIST), Nakoji 3-11-46, 661-0974, Amagasaki, Hyogo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hitoshi","family":"Ohsaki","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology (AIST), Nakoji 3-11-46, 661-0974, Amagasaki, Hyogo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenji","family":"Taguchi","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology (AIST), Nakoji 3-11-46, 661-0974, Amagasaki, Hyogo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Japan Embedded System Technology Association. A tentative report on questionnaires of spread of design methods 2011 (Japanese). et2010_questionnaire.pdf file on JASA web site 2012."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Biere A Cimatti A Clarke E Zhu Y (1999) Symbolic model checking without BDDs. In: 5th TACAS. Springer Berlin pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_2_4_2","unstructured":"Bhaduri P Ramesh S (2004) Model checking of statechart models: survey and research directions. CoRR cs.SE\/0407038"},{"key":"e_1_2_1_2_5_2","unstructured":"Barrett C Sebastiani R Seshia S Tinelli C (2011) Handbook of Satisfiability chapter 26. Elsevier Amsterdam pp 825\u2013885"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barrett C Tinelli C (2007) CVC3. In: 19th CAV. Springer Berlin pp 298\u2013302","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"e_1_2_1_2_7_2","volume-title":"Principle of model checking","author":"Katoen J-P","year":"2008"},{"key":"e_1_2_1_2_8_2","volume-title":"Model Checking","author":"Clarke E","year":"1999"},{"key":"e_1_2_1_2_9_2","unstructured":"Groote JF Mathijssen A ReniersHelle MA Usenko YS van Weerdenburg M (2007) The formal specification language mCRL2. In: Proceedings of methods for modelling software systems volume 06351 of Dagstuhkl Seminar"},{"issue":"1","key":"e_1_2_1_2_10_2","first-page":"83","article-title":"Towards model checking executable UML specifications in mCRL2","volume":"6","author":"Hansen HH","year":"2010","journal-title":"ISSE"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"e_1_2_1_2_12_2","unstructured":"Hoare CAR (2004) Communicating sequential processes vol 9 viii+256 p. By C.A.R. Hoare Prentice-Hall International London 1985"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_2_14_2","volume-title":"The SPIN model checker: primer and reference manual","author":"Holzmann GJ","year":"2008"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Kong W Katahira N Qian W Watanabe M Katayama T Fukuda A (2011) An SMT-based approach to bounded model checking of designs in communicating state transition matrix. In: IEEE CS 11th ICCSA pp 159\u2013167.","DOI":"10.1109\/ICCSA.2011.30"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Kong W Liu L Yamagata Y Taguchi K Ohsaki H Fukuda A (2012) On accelerating SMT-based bounded model checking of HSTM designs. In: IEEE CS 19th APSEC pp 614\u2013623","DOI":"10.1109\/APSEC.2012.38"},{"key":"e_1_2_1_2_17_2","unstructured":"Koike T (2008) Model checking support environment based on state transition matrix. IPSJ SIG Technical Report"},{"issue":"5","key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"946","DOI":"10.1587\/transinf.E94.D.946","article-title":"An SMT-based approach to bounded model checking of design in state transition matrix","volume":"94","author":"Kong W","year":"2011","journal-title":"IEICE Trans Inform Syst E"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Liu Y Sun J Dong J (2011) PAT3: An extensible architecture for building multi-domain model checkers. In: IEEE 22th ISSRE pp 190\u2013199","DOI":"10.1109\/ISSRE.2011.19"},{"key":"e_1_2_1_2_20_2","volume-title":"Executable UML: a foundation for model-driven architecture","author":"Mellor SJ","year":"2002"},{"key":"e_1_2_1_2_21_2","unstructured":"Ng MY Butler M (2003) Towards formalizing UML state diagrams in CSP. In: IEEE CS 1st SEFM pp 138\u2013147"},{"key":"e_1_2_1_2_22_2","unstructured":"Nomura T (2009) Trial of model checking by spreadsheet. In: SQiP Symposium pp 1\u20134"},{"key":"e_1_2_1_2_23_2","unstructured":"Roscoe AW Hoare CAR Bird (1998) The theory and practice of concurrency volume 216. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Dong JS (2009) Model checking CSP revisited: introducing a process analysis toolkit. Leveraging Applications of Formal Methods Verification and Validation. IEEE Computer Society Los Alamitos pp 307\u2013322","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Dong JS Pang J (2009) PAT: towards flexible verification under fairness. In: 21th CAV volume 5643 of LNCS. Springer Berlin pp 709\u2013714","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Sekerinski E Zurob R (2002) Translating Statecharts to B. In: 3rd IFM volume 2335 of LNCS. Springer Berlin pp 128\u2013144","DOI":"10.1007\/3-540-47884-1_8"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Uselton A Smolka SA (1994) A compositional semantics for statecharts using labeled transition systems. CONCUR\u201994: concurrency Theory","DOI":"10.1007\/978-3-540-48654-1_2"},{"key":"e_1_2_1_2_28_2","unstructured":"Watanabe M (1998) Extended hierarchy state transition matrix design method-version 2.0. Technical report CATS Technical Report"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Zhang SJ Liu Y (2010) An automatic approach to model checking UML state machines. In: IEEE 4th SSIRI pp 1\u20136","DOI":"10.1109\/SSIRI-C.2010.11"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0282-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0282-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0282-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:57:23Z","timestamp":1641484643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0282-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9]]},"references-count":29,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["10.1007\/s00165-013-0282-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0282-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9]]}}}