Hybrid System Verification Is not a Sinecure - the Electronic Throttle Control Case Study

Ansgar Fehnker, Bruce H. Krogh

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)
14 Downloads (Pure)

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 languageEnglish
Pages (from-to)885-902
Number of pages18
JournalInternational journal of foundations of computer science
Volume17
Issue number4
DOIs
Publication statusPublished - 2006
Externally publishedYes

Fingerprint

Model checking
Hybrid systems
Systems analysis
Control systems

Cite this

@article{48232a05e67346ccbc38ba3e0a225d1b,
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 = "2006",
doi = "10.1142/S0129054106004169",
language = "English",
volume = "17",
pages = "885--902",
journal = "International journal of foundations of computer science",
issn = "0129-0541",
publisher = "World Scientific Publishing Co. Pte Ltd",
number = "4",

}

Hybrid System Verification Is not a Sinecure - the Electronic Throttle Control Case Study. / Fehnker, Ansgar; Krogh, Bruce H.

In: International journal of foundations of computer science, Vol. 17, No. 4, 2006, p. 885-902.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Hybrid System Verification Is not a Sinecure - the Electronic Throttle Control Case Study

AU - Fehnker, Ansgar

AU - Krogh, Bruce H.

PY - 2006

Y1 - 2006

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.

U2 - 10.1142/S0129054106004169

DO - 10.1142/S0129054106004169

M3 - Article

VL - 17

SP - 885

EP - 902

JO - International journal of foundations of computer science

JF - International journal of foundations of computer science

SN - 0129-0541

IS - 4

ER -