--- res: bibo_abstract: - 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@eng bibo_authorlist: - foaf_Person: foaf_givenName: Rajeev foaf_name: Alur, Rajeev foaf_surname: Alur - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Pei foaf_name: Ho, Pei foaf_surname: Ho bibo_doi: 10.1109/32.489079 bibo_issue: '3' bibo_volume: 22 dct_date: 1996^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/0018-9162 dct_language: eng dct_publisher: IEEE@ dct_title: Automatic symbolic verification of embedded systems@ ...