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

Ansgar Fehnker; Bruce H. Krogh

doi:10.1142/S0129054106004169

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

Ansgar Fehnker, Bruce H. Krogh

Research output: Contribution to journal › Article › Academic › peer-review

1 Citation (Scopus)

30 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 language	English
Pages (from-to)	885-902
Number of pages	18
Journal	International journal of foundations of computer science
Volume	17
Issue number	4
DOIs	https://doi.org/10.1142/S0129054106004169
Publication status	Published - 2006
Externally published	Yes

Access to Document

10.1142/S0129054106004169

hybridFinal published version, 1.04 MB

Fingerprint Dive into the research topics of 'Hybrid System Verification Is not a Sinecure - the Electronic Throttle Control Case Study'. Together they form a unique fingerprint.

Cite this

Fehnker, A., & Krogh, B. H. (2006). Hybrid System Verification Is not a Sinecure - the Electronic Throttle Control Case Study. International journal of foundations of computer science, 17(4), 885-902. https://doi.org/10.1142/S0129054106004169

@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",

}

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 -