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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Ouimet, M., & Lundqvist, K. (2007). The TASM toolset: Specification, simulation, and formal verification of real-time systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4590 LNCS, pp. 126–130). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_15
Mendeley helps you to discover research relevant for your work.