---
_id: '4616'
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
article_processing_charge: No
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.
    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>'
  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>'
  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.
  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>.
  short: R. Alur, T.A. Henzinger, P. Ho, in:, 1993 Proceedings Real-Time Systems Symposium,
    IEEE, 1993, pp. 2–11.
conference:
  end_date: 1993-12-03
  location: Raleigh, NC, United States of America
  name: 'RTSS: Real-Time Systems Symposium'
  start_date: 1993-12-01
date_created: 2018-12-11T12:09:46Z
date_published: 1993-01-01T00:00:00Z
date_updated: 2022-03-23T13:01:41Z
day: '01'
doi: '10.1109/REAL.1993.393520 '
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/393520
month: '01'
oa_version: None
page: 2 - 11
publication: 1993 Proceedings Real-Time Systems Symposium
publication_identifier:
  isbn:
  - 0-8186-4480-X
publication_status: published
publisher: IEEE
publist_id: '90'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Automatic symbolic verification of embedded systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1993'
...