Hybrid system verification is not a sinecure: the electronic throttle control case study

Ansgar Fehnker; Bruce H. Krogh

doi:10.1007/978-3-540-30476-0_23

Hybrid system verification is not a sinecure: the electronic throttle control case study

Ansgar Fehnker^*
, Bruce H. Krogh

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

9 Citations (Scopus)

Abstract

Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings
Editors	Farn Wang
Publisher	Springer
Pages	263-277
Number of pages	15
ISBN (Print)	9783540236108
DOIs	https://doi.org/10.1007/978-3-540-30476-0_23
Publication status	Published - 2004
Externally published	Yes
Event	2nd International Conference on Automated Technology for Verification and Analysis, ATVA 2004 - Taipei, Taiwan Duration: 31 Oct 2004 → 3 Nov 2004 Conference number: 2

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3299
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Conference on Automated Technology for Verification and Analysis, ATVA 2004
Abbreviated title	ATVA 2004
Country/Territory	Taiwan
City	Taipei
Period	31/10/04 → 3/11/04

Access to Document

10.1007/978-3-540-30476-0_23

Cite this

Fehnker, A., & Krogh, B. H. (2004). Hybrid system verification is not a sinecure: the electronic throttle control case study. In F. Wang (Ed.), Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings (pp. 263-277). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3299). Springer. https://doi.org/10.1007/978-3-540-30476-0_23

Fehnker, Ansgar ; Krogh, Bruce H. / Hybrid system verification is not a sinecure : the electronic throttle control case study. Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings. editor / Farn Wang. Springer, 2004. pp. 263-277 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{3d7dd4b4252d4cc1aa56a72dfdd478f4,

title = "Hybrid system verification is not a sinecure: the electronic throttle control case study",

abstract = "Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration.",

author = "Ansgar Fehnker and Krogh, \{Bruce H.\}",

year = "2004",

doi = "10.1007/978-3-540-30476-0\_23",

language = "English",

isbn = "9783540236108",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "263--277",

editor = "Farn Wang",

booktitle = "Automated Technology for Verification and Analysis",

address = "Germany",

note = "2nd International Conference on Automated Technology for Verification and Analysis, ATVA 2004, ATVA 2004 ; Conference date: 31-10-2004 Through 03-11-2004",

}

Fehnker, A & Krogh, BH 2004, Hybrid system verification is not a sinecure: the electronic throttle control case study. in F Wang (ed.), Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3299, Springer, pp. 263-277, 2nd International Conference on Automated Technology for Verification and Analysis, ATVA 2004, Taipei, Taiwan, 31/10/04. https://doi.org/10.1007/978-3-540-30476-0_23

Hybrid system verification is not a sinecure: the electronic throttle control case study. / Fehnker, Ansgar; Krogh, Bruce H.
Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings. ed. / Farn Wang. Springer, 2004. p. 263-277 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3299).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Hybrid system verification is not a sinecure

T2 - 2nd International Conference on Automated Technology for Verification and Analysis, ATVA 2004

AU - Fehnker, Ansgar

AU - Krogh, Bruce H.

N1 - Conference code: 2

PY - 2004

Y1 - 2004

N2 - Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration.

AB - Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration.

UR - https://www.scopus.com/pages/publications/34147183175

U2 - 10.1007/978-3-540-30476-0_23

DO - 10.1007/978-3-540-30476-0_23

M3 - Chapter

AN - SCOPUS:34147183175

SN - 9783540236108

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

SP - 263

EP - 277

BT - Automated Technology for Verification and Analysis

A2 - Wang, Farn

PB - Springer

Y2 - 31 October 2004 through 3 November 2004

ER -

Fehnker A, Krogh BH. Hybrid system verification is not a sinecure: the electronic throttle control case study. In Wang F, editor, Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings. Springer. 2004. p. 263-277. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-30476-0_23

Hybrid system verification is not a sinecure: the electronic throttle control case study

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this