IEICE TRANSACTIONS on Information
Temporal Verification of Real-Time Systems
Summary :
This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.
- Publication
- IEICE TRANSACTIONS on Information Vol.E78-D No.7 pp.796-801
- Publication Date
- 1995/07/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Verification, Test and Diagnosis of VLSI Systems)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Sérgio V. CAMPOS, Edmund M. CLARKE, Wilfredo MARRERO, Marius MINEA, Hiromi HIRAISHI, "Temporal Verification of Real-Time Systems" in IEICE TRANSACTIONS on Information,
vol. E78-D, no. 7, pp. 796-801, July 1995, doi: .
Abstract: This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.
URL: https://global.ieice.org/en_transactions/information/10.1587/e78-d_7_796/_p
Copy
@ARTICLE{e78-d_7_796,
author={Sérgio V. CAMPOS, Edmund M. CLARKE, Wilfredo MARRERO, Marius MINEA, Hiromi HIRAISHI, },
journal={IEICE TRANSACTIONS on Information},
title={Temporal Verification of Real-Time Systems},
year={1995},
volume={E78-D},
number={7},
pages={796-801},
abstract={This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.},
keywords={},
doi={},
ISSN={},
month={July},}
Copy
TY - JOUR
TI - Temporal Verification of Real-Time Systems
T2 - IEICE TRANSACTIONS on Information
SP - 796
EP - 801
AU - Sérgio V. CAMPOS
AU - Edmund M. CLARKE
AU - Wilfredo MARRERO
AU - Marius MINEA
AU - Hiromi HIRAISHI
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E78-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 1995
AB - This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.
ER -
English
