The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems

Abstract. In this paper, we describe the features of the Timed Abstract State Machine toolset. The toolset implements the features of the Timed Abstract State Machine (TASM) language, a specification language for reactive real-time systems. The TASM language enables the specification of functional and non-functional properties using a unified language. The toolset incorporates features to create specifications, simulate specifications, and verify formal properties of specifications. Properties that can be verified using the toolset include completeness, consistency, worst-case execution time, and best-case execution time. The toolset is being developed as part of an architecture-based framework for embedded realtime system engineering. We describe how the features of the toolset were used successfully to model and analyze case studies from the aerospace and automotive communities.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Martin Ouimet, Kristina Lundqvist
• Keywords: Abstract State Machine, CAV 2007, Hardware, Toolset Include Completeness, Toolset Incorporates Features