{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T11:24:51Z","timestamp":1649071491523},"reference-count":20,"publisher":"World Scientific Pub Co Pte Lt","issue":"06","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2008,9]]},"abstract":"<jats:p> The application domain, such as communication networks and embedded controllers for telephony, automobiles, trains and avionics systems, requires very high quality reactive systems, so an important phase in the development of reactive systems is the verification of their conceptual models before implementation. Normally in the requirement analysis phase, system property can be represented as an input and output labeled transition system (IOLTS), which is a transition system labeled by inputs and outputs between the system and the environment. This paper describes an attempt to propose an approach to verify Statechart specifications for reactive systems given IOLTS property specifications. We develop a suitable semantics model \u2014 observable semantics, an abstract semantics model only which describes outside observable behavior and suffers from less state explosion problem by reducing infinite or large state spaces to small ones. Then we propose two methods to verify the conformance between a given IOLTS property specification and a Statechart specification: two-phase verification and on-the-fly verification. Compared with two-phase verification, on-the-fly verification needs less storage and computation-time, especially when the target Statechart specification is very large or likely to have many errors. <\/jats:p>","DOI":"10.1142\/s0218194008003908","type":"journal-article","created":{"date-parts":[[2008,12,16]],"date-time":"2008-12-16T11:06:41Z","timestamp":1229425601000},"page":"785-802","source":"Crossref","is-referenced-by-count":0,"title":["A NEW APPROACH TO VERIFY STATECHART SPECIFICATIONS FOR REACTIVE SYSTEMS"],"prefix":"10.1142","volume":"18","author":[{"given":"YUCHANG","family":"MO","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, Southeast University, Nanjing, Jiangsu 211198, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"XINMIN","family":"YANG","sequence":"additional","affiliation":[{"name":"28th Research Institute of China Electronics Technology Group Corporation, Nanjing, Jiangsu 210007, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","first-page":"477","volume":"13","author":"Harel D.","journal-title":"Logic and Model of Concurrent Systems"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.5009519"},{"key":"rf4","doi-asserted-by":"publisher","DOI":"10.1109\/32.317428"},{"key":"rf5","volume-title":"Object-Oriented Modeling and Design","author":"Rumbaugh J.","year":"1991"},{"key":"rf6","volume-title":"Real-Time Object-Oriented Modeling","author":"Selic B.","year":"1994"},{"key":"rf7","volume-title":"The Unified Modeling Language User Guide","author":"Booch G.","year":"1998"},{"key":"rf8","doi-asserted-by":"publisher","DOI":"10.1109\/32.708566"},{"key":"rf9","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"rf18","first-page":"677","volume":"35","author":"Bryant R. E.","journal-title":"IEEE Trans. Computers"},{"key":"rf20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"rf23","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"key":"rf27","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054174"},{"key":"rf29","unstructured":"A.\u00a0Pnueli, Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends, LNCS\u00a0224 (1985)\u00a0pp. 510\u2013584."},{"key":"rf30","first-page":"657","volume":"83","author":"Lamport L.","journal-title":"Information Processing"},{"key":"rf31","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"rf32","doi-asserted-by":"publisher","DOI":"10.1146\/annurev.cs.02.060187.001413"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194008003908","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T01:45:11Z","timestamp":1565142311000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194008003908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9]]},"references-count":20,"journal-issue":{"issue":"06","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2008,9]]}},"alternative-id":["10.1142\/S0218194008003908"],"URL":"https:\/\/doi.org\/10.1142\/s0218194008003908","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,9]]}}}