Modeling an Electronic Throttle Controller using the Timed Abstract State Machine Language and Toolset
Martin Ouimet, Guillaume Berteau, Kristina Lundqvist · 2006
A key challenge in the design and analysis of real-time systems is the integration of functional and non-functional properties into a single specification. In this paper, we present an integrated toolset based on the TASM language. The toolset is used to specify and analyze reactive embedded real-time systems. The toolset implements the features of the Timed Abstract State Machine (TASM) language, a novel specification language. The non-functional properties that can be expressed in the language include timing behavior and resource consumption. The toolset enables the creation of executable specifications with well-defined execution semantics, abstraction mechanisms, and composition semantics. The toolset includes facilities for editing, analyzing, and simulating TASM specifications. The features of the toolset are demonstrated using an Electronic Throttle Controller (ETC) from a major automotive vendor. The TASM toolset is used to analyze the mode switching logic of the ETC. The ETC is used to calculate fuel injection and air intake to optimize fuel consumption. The TASM toolset is used to analyze the resource consumption resulting from the mode switching logic, and to verify the completeness and consistency of the specification.