{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:03Z","timestamp":1750306803672,"version":"3.41.0"},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,12,1]],"date-time":"2013-12-01T00:00:00Z","timestamp":1385856000000},"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":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2013,12]]},"abstract":"<jats:p>An infrared sensor is modeled and analyzed in Uppaal. The sensor typifies the sort of component that engineers regularly integrate into larger systems by writing interface hardware and software.<\/jats:p>\n          <jats:p>In all, three main models are developed. In the first model, the timing diagram of the sensor is interpreted and modeled as a timed safety automaton. This model serves as a specification for the complete system. A second model that emphasizes the separate roles of driver and sensor is then developed. It is validated against the timing diagram model using an existing construction that permits the verification of timed trace inclusion, for certain models, by reachability analysis (i.e., model checking). A transmission correctness property is also stated by means of an auxiliary automaton and shown to be satisfied by the model.<\/jats:p>\n          <jats:p>A third model is created from an assembly language driver program, using a direct translation from the instruction set of a processor with simple timing behavior. This model is validated against the driver component of the second timing diagram model using the timed trace inclusion validation technique. The approach and its limitations offer insight into the nature and challenges of programming in real time.<\/jats:p>","DOI":"10.1145\/2539036.2539040","type":"journal-article","created":{"date-parts":[[2013,12,20]],"date-time":"2013-12-20T19:50:46Z","timestamp":1387569046000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Analyzing an embedded sensor with timed automata in uppaal"],"prefix":"10.1145","volume":"13","author":[{"given":"Timothy","family":"Bourke","sequence":"first","affiliation":[{"name":"INRIA and \u00c9cole normale sup\u00e9rieure, Paris"}]},{"given":"Arcot","family":"Sowmya","sequence":"additional","affiliation":[{"name":"University of New South Wales, Sydney"}]}],"member":"320","published-online":{"date-parts":[[2013,12,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28412-0_12"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450068"},{"key":"e_1_2_1_6_1","unstructured":"Griebling E. T. 1999. GP2D02 assembly language driver for 68HC12B32 microcontroller. http:\/\/home.earthlink.net\/&sim;tdickens\/68hc11\/code\/sharpirhc12.asm.  Griebling E. T. 1999. GP2D02 assembly language driver for 68HC12B32 microcontroller. http:\/\/home.earthlink.net\/&sim;tdickens\/68hc11\/code\/sharpirhc12.asm."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_1_8_1","unstructured":"Intel Corporation. 1994. MCS\u00ae51 microcontroller family user's manual.  Intel Corporation. 1994. MCS\u00ae51 microcontroller family user's manual."},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Jensen H. E. Larsen K. G. and \n      Skou A\n  . \n  2000\n  . Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In Proceedings of the 6th International Symposium on Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT'00). M. Joseph Ed. Lecture Notes in Computer Science Series vol. \n  1926 Springer-Verlag Berlin 19--30.   Jensen H. E. Larsen K. G. and Skou A. 2000. Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In Proceedings of the 6th International Symposium on Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT'00). M. Joseph Ed. Lecture Notes in Computer Science Series vol. 1926 Springer-Verlag Berlin 19--30.","DOI":"10.1007\/3-540-45352-0_4"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Kaynar D. K. Lynch N. Segala R. and Vaandrager F. 2006. The Theory of Timed I\/O Automata. Synthesis Lectures on Computer Science. Morgan & Claypool Publishers San Rafael CA.   Kaynar D. K. Lynch N. Segala R. and Vaandrager F. 2006. The Theory of Timed I\/O Automata. Synthesis Lectures on Computer Science. Morgan & Claypool Publishers San Rafael CA.","DOI":"10.1007\/978-3-031-01794-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_2_1_13_1","unstructured":"Ramsey A. 2001. Interfacing the GP2D02 to a Microchip PIC. Encoder: Newslet. Seattle Robotics Soc.  Ramsey A. 2001. Interfacing the GP2D02 to a Microchip PIC. Encoder: Newslet. Seattle Robotics Soc."},{"key":"e_1_2_1_15_1","unstructured":"Sharp Corporation. 1997. GP2D02: Compact high sensitive distance measuring sensor.  Sharp Corporation. 1997. GP2D02: Compact high sensitive distance measuring sensor."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0008-1"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2539036.2539040","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2539036.2539040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:50Z","timestamp":1750232090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2539036.2539040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["10.1145\/2539036.2539040"],"URL":"https:\/\/doi.org\/10.1145\/2539036.2539040","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2013,12]]},"assertion":[{"value":"2011-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-12-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}