Powered by OpenAIRE graph
Found an issue? Give us feedback
addClaim

On formal verification of Toyota's electronic throttle controller

Authors: Jim Ras; Albert M. K. Cheng;

On formal verification of Toyota's electronic throttle controller

Abstract

This practice paper examines Toyota's electronic throttle controller (ETC) problem. ETC for passenger cars is a safety-critical, embedded control system and it must meet very high reliability and safety requirements. ETC systems continue to increase in complexity, making formal specification and verification processes an essential component of the development of safer systems. There are two ways to represent the real-time system. Firstly, we can describe the system's structure and function by detailing its electrical, mechanical, and other components. Secondly, the real-time system's behavior as it responds to actions and events can be described. Then we can compare the system's specification to the safety assertion to show that the system meets the safety properties. This paper describes two research threads. In the first, we present the specification of Toyota's electronic throttle control (ETC) system including the timing constraints. The second thread, which will be explored in a longer version of this paper, evaluates the use of conventional design versus electronic engine control by applying classical control theory.1

Related Organizations
  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    1
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
1
Average
Average
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!