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)

52 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

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

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 -

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

Abstract

Access to Document

Fingerprint

Cite this