[{"month":"01","title":"Automatic symbolic verification of embedded systems","date_updated":"2022-03-23T13:01:41Z","publication_identifier":{"isbn":["0-8186-4480-X"]},"date_published":"1993-01-01T00:00:00Z","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Pei","last_name":"Ho","full_name":"Ho, Pei"}],"year":"1993","conference":{"name":"RTSS: Real-Time Systems Symposium","start_date":"1993-12-01","location":"Raleigh, NC, United States of America","end_date":"1993-12-03"},"article_processing_charge":"No","page":"2 - 11","oa_version":"None","publication":"1993 Proceedings Real-Time Systems Symposium","doi":"10.1109/REAL.1993.393520 ","date_created":"2018-12-11T12:09:46Z","day":"01","publisher":"IEEE","_id":"4616","language":[{"iso":"eng"}],"status":"public","abstract":[{"lang":"eng","text":"We present a model checking procedure and its implementation for the automatic verification of embedded systems. Systems are represented by hybrid automata - machines with finite control and real-valued variables modeling continuous environment parameters such as time, pressure, and temperature. System properties are specified in a real-time temporal logic and verified by symbolic computation. The verification procedure, implemented in Mathematica, is used to prove digital controllers and distributed algorithms correct. The verifier checks safety, liveness, time-bounded, and duration properties of hybrid automata"}],"publication_status":"published","main_file_link":[{"url":"https://ieeexplore.ieee.org/document/393520"}],"publist_id":"90","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","quality_controlled":"1","scopus_import":"1","type":"conference","citation":{"ista":"Alur R, Henzinger TA, Ho P. 1993. Automatic symbolic verification of embedded systems. 1993 Proceedings Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium, 2–11.","mla":"Alur, Rajeev, et al. “Automatic Symbolic Verification of Embedded Systems.” <i>1993 Proceedings Real-Time Systems Symposium</i>, IEEE, 1993, pp. 2–11, doi:<a href=\"https://doi.org/10.1109/REAL.1993.393520 \">10.1109/REAL.1993.393520 </a>.","ama":"Alur R, Henzinger TA, Ho P. Automatic symbolic verification of embedded systems. In: <i>1993 Proceedings Real-Time Systems Symposium</i>. IEEE; 1993:2-11. doi:<a href=\"https://doi.org/10.1109/REAL.1993.393520 \">10.1109/REAL.1993.393520 </a>","chicago":"Alur, Rajeev, Thomas A Henzinger, and Pei Ho. “Automatic Symbolic Verification of Embedded Systems.” In <i>1993 Proceedings Real-Time Systems Symposium</i>, 2–11. IEEE, 1993. <a href=\"https://doi.org/10.1109/REAL.1993.393520 \">https://doi.org/10.1109/REAL.1993.393520 </a>.","ieee":"R. Alur, T. A. Henzinger, and P. Ho, “Automatic symbolic verification of embedded systems,” in <i>1993 Proceedings Real-Time Systems Symposium</i>, Raleigh, NC, United States of America, 1993, pp. 2–11.","short":"R. Alur, T.A. Henzinger, P. Ho, in:, 1993 Proceedings Real-Time Systems Symposium, IEEE, 1993, pp. 2–11.","apa":"Alur, R., Henzinger, T. A., &#38; Ho, P. (1993). Automatic symbolic verification of embedded systems. In <i>1993 Proceedings Real-Time Systems Symposium</i> (pp. 2–11). Raleigh, NC, United States of America: IEEE. <a href=\"https://doi.org/10.1109/REAL.1993.393520 \">https://doi.org/10.1109/REAL.1993.393520 </a>"},"extern":"1"}]