Sciweavers

CAV
2007
Springer

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

13 years 7 months ago
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.
Martin Ouimet, Kristina Lundqvist
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where CAV
Authors Martin Ouimet, Kristina Lundqvist
Comments (0)