Model checking timed systems with urgencies

Pao Ann Hsiung, Shang Wei Lin, Yean-Ru Chen, Chun Hsian Huang, Jia Jen Yeh, Hong Yu Sun, Chao Sheng Lin, Hsiao Win Liao

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

Computation tree logic (CTL) model checkers either allow modeling of only lazy semantics in the timed system model or consider at most a simple as soon as possible semantics. However, the design of real-time systems requires different types of urgencies, which have been modeled by several urgency variants of the timed automata model. Except for the IF toolset that model checks timed automata with urgency against observers, the urgency variants of timed automata have not yet been used for verifying the satisfaction of CTL properties in real-time systems. This work is targeted at proposing a zone-based urgency semantics that is time-reactive and at model checking timed automata models that have been extended with such urgency semantics for delayable and eager transition types. Interactions among these different types of transition urgencies are also investigated. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings
PublisherSpringer Verlag
Pages67-81
Number of pages15
ISBN (Print)3540472371, 9783540472377
Publication statusPublished - 2006 Jan 1
Event4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China
Duration: 2006 Oct 232006 Oct 26

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4218 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006
CountryChina
CityBeijing
Period06-10-2306-10-26

Fingerprint

Model checking
Model Checking
Timed Automata
Real time systems
Semantics
Logic
Real-time
State Space
Model
Embedded systems
Embedded Systems
Observer
Interaction
Modeling
Experiment
Experiments

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hsiung, P. A., Lin, S. W., Chen, Y-R., Huang, C. H., Yeh, J. J., Sun, H. Y., ... Liao, H. W. (2006). Model checking timed systems with urgencies. In Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings (pp. 67-81). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4218 LNCS). Springer Verlag.
Hsiung, Pao Ann ; Lin, Shang Wei ; Chen, Yean-Ru ; Huang, Chun Hsian ; Yeh, Jia Jen ; Sun, Hong Yu ; Lin, Chao Sheng ; Liao, Hsiao Win. / Model checking timed systems with urgencies. Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Springer Verlag, 2006. pp. 67-81 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{e20d3071b82b4707aef304d992f61b3b,
title = "Model checking timed systems with urgencies",
abstract = "Computation tree logic (CTL) model checkers either allow modeling of only lazy semantics in the timed system model or consider at most a simple as soon as possible semantics. However, the design of real-time systems requires different types of urgencies, which have been modeled by several urgency variants of the timed automata model. Except for the IF toolset that model checks timed automata with urgency against observers, the urgency variants of timed automata have not yet been used for verifying the satisfaction of CTL properties in real-time systems. This work is targeted at proposing a zone-based urgency semantics that is time-reactive and at model checking timed automata models that have been extended with such urgency semantics for delayable and eager transition types. Interactions among these different types of transition urgencies are also investigated. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.",
author = "Hsiung, {Pao Ann} and Lin, {Shang Wei} and Yean-Ru Chen and Huang, {Chun Hsian} and Yeh, {Jia Jen} and Sun, {Hong Yu} and Lin, {Chao Sheng} and Liao, {Hsiao Win}",
year = "2006",
month = "1",
day = "1",
language = "English",
isbn = "3540472371",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "67--81",
booktitle = "Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings",
address = "Germany",

}

Hsiung, PA, Lin, SW, Chen, Y-R, Huang, CH, Yeh, JJ, Sun, HY, Lin, CS & Liao, HW 2006, Model checking timed systems with urgencies. in Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4218 LNCS, Springer Verlag, pp. 67-81, 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006, Beijing, China, 06-10-23.

Model checking timed systems with urgencies. / Hsiung, Pao Ann; Lin, Shang Wei; Chen, Yean-Ru; Huang, Chun Hsian; Yeh, Jia Jen; Sun, Hong Yu; Lin, Chao Sheng; Liao, Hsiao Win.

Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Springer Verlag, 2006. p. 67-81 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4218 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Model checking timed systems with urgencies

AU - Hsiung, Pao Ann

AU - Lin, Shang Wei

AU - Chen, Yean-Ru

AU - Huang, Chun Hsian

AU - Yeh, Jia Jen

AU - Sun, Hong Yu

AU - Lin, Chao Sheng

AU - Liao, Hsiao Win

PY - 2006/1/1

Y1 - 2006/1/1

N2 - Computation tree logic (CTL) model checkers either allow modeling of only lazy semantics in the timed system model or consider at most a simple as soon as possible semantics. However, the design of real-time systems requires different types of urgencies, which have been modeled by several urgency variants of the timed automata model. Except for the IF toolset that model checks timed automata with urgency against observers, the urgency variants of timed automata have not yet been used for verifying the satisfaction of CTL properties in real-time systems. This work is targeted at proposing a zone-based urgency semantics that is time-reactive and at model checking timed automata models that have been extended with such urgency semantics for delayable and eager transition types. Interactions among these different types of transition urgencies are also investigated. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.

AB - Computation tree logic (CTL) model checkers either allow modeling of only lazy semantics in the timed system model or consider at most a simple as soon as possible semantics. However, the design of real-time systems requires different types of urgencies, which have been modeled by several urgency variants of the timed automata model. Except for the IF toolset that model checks timed automata with urgency against observers, the urgency variants of timed automata have not yet been used for verifying the satisfaction of CTL properties in real-time systems. This work is targeted at proposing a zone-based urgency semantics that is time-reactive and at model checking timed automata models that have been extended with such urgency semantics for delayable and eager transition types. Interactions among these different types of transition urgencies are also investigated. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.

UR - http://www.scopus.com/inward/record.url?scp=33845202913&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845202913&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540472371

SN - 9783540472377

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 67

EP - 81

BT - Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings

PB - Springer Verlag

ER -

Hsiung PA, Lin SW, Chen Y-R, Huang CH, Yeh JJ, Sun HY et al. Model checking timed systems with urgencies. In Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Springer Verlag. 2006. p. 67-81. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).