The Timed Abstract State Machine Language : An Executable Specification Language for Reactive Real-Time Systems
Martin Ouimet, Kristina Lundqvist, Mikael Sjödin · 2006
In this paper, we present the Timed Abstract State Machine (TASM) language, which is a language for the specification of embedded real-time systems. The TASM language is an extension of Abstract State Machines (ASM), that includes facilities for specifying non-functional behavior namely time and resource consumption. In the engineering of 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 key aspects can be specified and analyzed. 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 durative instead of being instantaneous. This paradigm captures the realistic behavior of real-time systems where actions are never instantaneous. The concurrency semantics of TASM is synchronous with respect to durative steps. We present the syntax and semantics of the language and illustrate the concepts using the production cell case study.