{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:08:44Z","timestamp":1761487724627},"reference-count":20,"publisher":"Wiley","issue":"2","license":[{"start":{"date-parts":[[2006,10,30]],"date-time":"2006-10-30T00:00:00Z","timestamp":1162166400000},"content-version":"vor","delay-in-days":4654,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Pract Exp"],"published-print":{"date-parts":[[1994,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe a toolset, consisting of a graphical editor, a simulator, and an assertion checker, for prototyping real\u2010time systems that are specified as Communicating Real\u2010Time State machines (CRSMs). CRSMs are timed state machines that communicate synchronously over unidirectional channels. The system behavior of CRSMs is characterized by a time\u2010stamped trace of communication events. Safety and timing assertions on the trace of communication events are expressed in a notation based on Real\u2010Time Logic. We illustrate the simulator and assertion checker by specifying a traffic\u2010light controller and other real\u2010time systems. There are two main contributions in this work: first, the prototyping environment serves as a validation of the model, the execution algorithm and paper design of example CRSMs, demonstrating that the ideas are realizable and potentially useful. Secondly, the paper presents a novel and useful method of specifying safety and timing properties, and checking them during simulation.<\/jats:p>","DOI":"10.1002\/spe.4380240203","type":"journal-article","created":{"date-parts":[[2006,11,17]],"date-time":"2006-11-17T16:55:23Z","timestamp":1163782523000},"page":"175-195","source":"Crossref","is-referenced-by-count":22,"title":["A prototyping environment for specifying, executing and checking communicating real\u2010time state machines"],"prefix":"10.1002","volume":"24","author":[{"given":"Sitaram C. V.","family":"Raju","sequence":"first","affiliation":[]},{"given":"Alan C.","family":"Shaw","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2006,10,30]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.6186"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1982.235254"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.159840"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6313045"},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.31537"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_8_2","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/FTCS.1990.89350"},{"key":"e_1_2_1_10_2","first-page":"74","volume-title":"Proc. IEEE Real\u2010Time Systems Symposium","author":"Chodrow S.","year":"1991"},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1992.242676"},{"key":"e_1_2_1_12_2","volume-title":"Xsim 2.0 User's Guide","author":"Thomas G.","year":"1990"},{"key":"e_1_2_1_13_2","first-page":"221","volume-title":"Proc. Winter Usenix Conference","author":"Swick R.","year":"1988"},{"key":"e_1_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"e_1_2_1_16_2","first-page":"254","volume-title":"Proc. IEEE Real\u2010Time Systems Symposium","author":"Stuart D. A.","year":"1991"},{"key":"e_1_2_1_17_2","first-page":"6","volume-title":"Proc. International Workshop on Computer\u2010Aided Software Eng.","author":"Selic B.","year":"1992"},{"key":"e_1_2_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/103167.103173"},{"key":"e_1_2_1_19_2","first-page":"45","volume-title":"Real\u2010Time: Theory in Practice, Proc. REX Workshop, Lecture Notes in Computer Science 600","author":"Alur R.","year":"1991"},{"key":"e_1_2_1_20_2","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1109\/REAL.1989.63580","volume-title":"Proc. IEEE Real\u2010Time Systems Symposium","author":"Attiya H.","year":"1989"},{"key":"e_1_2_1_21_2","unstructured":"S.Raju \u2018An automatic verification technique for Communicating Real\u2010Time State Machines\u2019 TR 93\u201304\u201308.Department of Computer Science and Engineering University of Washington Seattle 1993. (This is part of S. Raju's Ph.D. Thesis which is forthcoming.)"}],"container-title":["Software: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fspe.4380240203","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.4380240203","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T18:26:31Z","timestamp":1698171991000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/spe.4380240203"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,2]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,2]]}},"alternative-id":["10.1002\/spe.4380240203"],"URL":"https:\/\/doi.org\/10.1002\/spe.4380240203","archive":["Portico"],"relation":{},"ISSN":["0038-0644","1097-024X"],"issn-type":[{"value":"0038-0644","type":"print"},{"value":"1097-024X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,2]]}}}