---
_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'
...