In this paper, we present the Timed Abstract State Machine (TASM) language, which is a language for the specification of embedded real-time systems. In the engineering of embedded real-time systems, the correctness of the system is defined in terms of three aspects - function, time, and resource consumption. The goal of the TASM language and its associated toolset is to provide a basis for specification-based real-time system engineering where these three aspects can be specified and analyzed. The TASM language is built on top of Abstract State Machines (ASM) by including facilities for compact and legible specification of non-functional behavior, namely time and resource consumption. The TASM language provides a notation which is well-suited to the specification needs of embedded real-time systems. We begin the presentation of the language with a historical survey on the use of ASM in specifying real-time systems. The core difference between the TASM language and ASM is that steps are inherently durative instead of being instantaneous and steps consume resources. These concepts capture the reality of physical systems in a flexible abstract model. We present the syntax and semantics of the language and illustrate the concepts using an extended version of the production cell case study.

real-time systems, embedded systems, specification, verification, formal methods, Abstract State Machines