DOCUMENTATION PUBLICATIONS TECHNICAL REPORTS DOWNLOADS

The Timed Abstract State Machine (TASM) Language and Toolset

The TASM Language was developed as an extension to the theory of Abstract State Machines (ASM). Information about current ASM research can be found at the ASM Research Center and past information can be found on the ASM web site.

The core idea behind the TASM language is to incorporate functional and non-functional properties into a single specification language. More specifically, the TASM language can specify functional behavior, timing behavior, and resource consumption. Through the TASM language, it is possible to develop literate, reusable, executable, and verifiable embedded real-time system specifications. The associated TASM Toolset implements the language features and provides a set of functionality to support the engineering of embedded real-time systems across lifecycle phases.    

Downloads

   
Documentation

  • Language Reference

    This document gives the concepts behind the TASM language and serves as the central reference for the syntax and semantics of the language. While this document is the authoritative reference for the TASM language, it is quite long. Those unfamiliar with the TASM language could use the Language Introduction Technical Report as a good starting point.

   
Publications

  1. Ouimet, M., Berteau G., and Lundqvist, K. Modeling an Electronic Throttle Controller using the Timed Abstract State Machine Language and Toolset. In Proceedings of the Satellite Events of the 2006 MoDELS Conference, LNCS, Genoa, Italy, October 2006.

  2. Ouimet, M., Lundqvist, K., and Nolin, M. The Timed Abstract State Machine Language and the Hi-Five Framework. In Proceedings of the 27th IEEE International Real-Time Systems Symposium (RTSS '06) - Work in Progress Session, Rio De Janeiro, Brazil, December 2006.

  3. Ouimet, M. and Lundqvist, K. The Timed Abstract State Machine Language: An Executable Specification Language for Reactive Real-Time Systems. In Proceedings of the 15th International Conference on Real-Time and Network Systems (RTNS '07), Nancy, France, March 2007.

  4. Ouimet, M. and Lundqvist, K. Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver. In Proceedings of the 3rd International Workshop on Model-Based Testing (MBT '07), Satellite Workshop of ETAPS '07, Braga, Portugal, April 2007.

  5. Ouimet, M. and Lundqvist, K. The Timed Abstract State Machine Language: Abstract State Machines for Real-Time System Engineering. In Proceedings of the 14th International Workshop on Abstract State Machines (ASM '07), Grimstad, Norway, June 2007.

  6. Ouimet, M. and Lundqvist, K. The Timed Abstract State Machine Toolset: Specification, Simulation, and Verification of Real-Time Systems. In Proceedings of the 19th International Conference on Computer-Aided Verification (CAV '07), Berlin, Germany, July 2007.

  7. Ouimet, M. and Lundqvist, K. Bi-Directional Traceability: The Hi-Five Framework Approach to Reliable Validation of Early System Designs. Presented at the ARTIST International Workshop on Tool Platforms for Modeling, Analysis and Validation of Embedded systems, Satellite Workshop of CAV '07, Berlin, Germany, July 2007.

  8. Ouimet, M. and Lundqvist, K. TASM Language and the Hi-Five Framework: Specification, Validation, and Verification of Embedded Real-Time Systems. Presented at the Real-Time in Sweden (RTiS) Conference, Västerås, Sweden, August 2007.

  9. Ouimet, M. and Lundqvist, K. Engineering Real-Time Systems using the TASM language and toolset. In Proceedings of the 14th Asia-Pacific Software Engineering Conference (APSEC '07), Nagoya, Japan, December 2007.

  10. Ouimet, M. and Lundqvist, K. Combining Syntactic Traceability and Refinement Theory. Submitted for review to the Traceability Workshop of the 4th European Conference on Model-Driven Architecture (ECMDA '08), Berlin, Germany, June 12th 2007.

  11. Ouimet, M. and Lundqvist, K. The Timed Abstract State Machine Language: Abstract State Machines for Real-Time Systems Engineering.. Submitted for publication to the Journal of Universal Computer Science (JUCS), August 31st 2007.

   
Technical Reports

  • Technical Report ESL-TIK-00193: Language Introduction

    This paper introduces the TASM language and its relation to the ASM language. In a way, this paper is an abridged version of the Language Reference. Its reading is a good starting point for those not familiar with the TASM Language.

    This technical report has been superceded by the publication "The Timed Abstract State Machine Language: An Executable Specification Language for Reactive Real-Time Systems", presented at RTNS 2007.

  • Technical Report ESL-TIK-00204: Modeling an Electronic Throttle Controller

    This paper introduces the TASM Toolset and models an example embedded real-time system - an Electronic Throttle Controller.

    This technical report has been superceded by the publication "Modeling an Electronic Throttle Controller using the Timed Abstract State Machine Language and Toolset", presented at CSDUML 2006.

  • Technical Report ESL-TIK-00209: The Production Cell System

    This paper models the famous "production cell system", a case study used to evaluate formal methods.

  • Technical Report ESL-TIK-00211: A Mapping between the Timed Abstract State Machine Language and UPPAAL's Timed Automata

    This paper describes a translation from the TASM language to the Timed Automata formalism of UPPAAL. The translation is accomplished in order to verify timing properties of TASM specifications using the UPPAAL suite of tools.

  • Technical Report ESL-TIK-00212: Verifying Execution Time using the TASM Toolset and UPPAAL

    This paper uses the translation from TASM to UPPAAL to analyze the best-case and worst-case execution times of TASM models.

   
Questions or Comments ?     tasm <at> mit <dot> edu