--- _id: '4611' abstract: - lang: eng text: Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms acknowledgement: "We thank Costas Courcoubetis, Nicolas Halbwachs, Peter Kopke, Joseph Sifakis, and Howard Wong-Toi for helpful\r\ndiscussions and valuable comments. Thomas A. Henzinger's research was supported in part by the U.S. Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by National Science Foundation grants CCR-9200794 and CCR-9504469, by U.S. Air Force Office of Scientific Research contract F49620-93-1- 0056, and by Advanced Research Projects Agency grant NAG2-892. " article_processing_charge: No article_type: original author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Pei full_name: Ho, Pei last_name: Ho citation: ama: Alur R, Henzinger TA, Ho P. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 1996;22(3):181-201. doi:10.1109/32.489079 apa: Alur, R., Henzinger, T. A., & Ho, P. (1996). Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. IEEE. https://doi.org/10.1109/32.489079 chicago: Alur, Rajeev, Thomas A Henzinger, and Pei Ho. “Automatic Symbolic Verification of Embedded Systems.” IEEE Transactions on Software Engineering. IEEE, 1996. https://doi.org/10.1109/32.489079. ieee: R. Alur, T. A. Henzinger, and P. Ho, “Automatic symbolic verification of embedded systems,” IEEE Transactions on Software Engineering, vol. 22, no. 3. IEEE, pp. 181–201, 1996. ista: Alur R, Henzinger TA, Ho P. 1996. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 22(3), 181–201. mla: Alur, Rajeev, et al. “Automatic Symbolic Verification of Embedded Systems.” IEEE Transactions on Software Engineering, vol. 22, no. 3, IEEE, 1996, pp. 181–201, doi:10.1109/32.489079. short: R. Alur, T.A. Henzinger, P. Ho, IEEE Transactions on Software Engineering 22 (1996) 181–201. date_created: 2018-12-11T12:09:45Z date_published: 1996-03-01T00:00:00Z date_updated: 2022-07-04T12:47:05Z day: '01' doi: 10.1109/32.489079 extern: '1' intvolume: ' 22' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://ecommons.cornell.edu/handle/1813/7170 month: '03' oa: 1 oa_version: Published Version page: 181 - 201 publication: IEEE Transactions on Software Engineering publication_identifier: issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '96' quality_controlled: '1' scopus_import: '1' status: public title: Automatic symbolic verification of embedded systems type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 22 year: '1996' ...