{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T21:10:08Z","timestamp":1737234608296,"version":"3.33.0"},"reference-count":13,"publisher":"Wiley","issue":"5","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":4097,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp; Computers in Japan"],"published-print":{"date-parts":[[1996,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A verification system of asynchronous real\u2010time software including timing constraints, which supports both model\u2010checking algorithms and language inclusion algorithms, does not exist. In a language inclusion algorithm, verification specification is described by a timed automaton from the standpoint of both states and behaviors. On the other hand, in a model\u2010checking algorithm, verification specification is described by real\u2010time temporal logic from the standpoint of state relation. It is necessary to specify verification property by both timed automaton and real\u2010time temporal logic. A hybrid verification method, which supports both verification methods, is proposed here. In order to realize it, a timed Kripke structure is generated from timed automaton through an augmented region graph. The method is shown to be effective using the example of a clock problem.<\/jats:p>","DOI":"10.1002\/scj.4690270501","type":"journal-article","created":{"date-parts":[[2007,7,8]],"date-time":"2007-07-08T10:50:47Z","timestamp":1183891847000},"page":"1-14","source":"Crossref","is-referenced-by-count":1,"title":["Proposal of hybrid verification method in asynchronous real\u2010time software including timing constraints specification"],"prefix":"10.1002","volume":"27","author":[{"given":"Satoshi","family":"Yamane","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2007,3,21]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4016-8"},{"key":"e_1_2_1_3_2","first-page":"660","volume-title":"Real\u2010Time Systems, Abstraction, Languages, and Design Methodologies","author":"Kavi K. M.","year":"1992"},{"key":"e_1_2_1_4_2","unstructured":"S.Davidson Proc. of Real\u2010Time Systems Symposiium. IEEE Computer Society p.320(1993)."},{"key":"e_1_2_1_5_2","series-title":"LNCS 600","first-page":"74","volume-title":"Logics and Models of Real Time: A Survey","author":"Alur R.","year":"1992"},{"key":"e_1_2_1_6_2","series-title":"LNCS 600","first-page":"45","volume-title":"The Theory of Timed Automata","author":"Alur R.","year":"1992"},{"key":"e_1_2_1_7_2","first-page":"995","article-title":"Formal Models and Semantics","author":"Emerson E. A.","year":"1990","journal-title":"Handbook of Theoretical Computer Science"},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","unstructured":"R.Alur T.FederandH. A.Henzinger.The Benefits of Relaxing Punctuality.Proc. 10th ACM Symp. on Principles of Distributed Computing pp.139\u2013152(1991).","DOI":"10.1145\/112600.112613"},{"key":"e_1_2_1_9_2","doi-asserted-by":"crossref","unstructured":"R.Alur C.CourcoubetisandD.Dill.Model\u2010Checking for Real Time Systems.Proc. 5th IEEE Symp. on Logic In Computer Science pp.414\u2013425(1990).","DOI":"10.1109\/LICS.1990.113766"},{"key":"e_1_2_1_10_2","unstructured":"E. M.Clarke I. A.DraghicescuandR. P.Kurshan.A Unified Approach for Showing Language Containment and Equivalence Between Various Types of \u03c9\u2010Automata.CMU\u2010CS\u201089\u2010192 pp.1\u201314(1989)."},{"key":"e_1_2_1_11_2","first-page":"256","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"e_1_2_1_13_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357237"}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690270501","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690270501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T20:42:52Z","timestamp":1737232972000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690270501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,1]]},"references-count":13,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1996,1]]}},"alternative-id":["10.1002\/scj.4690270501"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690270501","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"type":"print","value":"0882-1666"},{"type":"electronic","value":"1520-684X"}],"subject":[],"published":{"date-parts":[[1996,1]]}}}