Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit

Abstract

Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used, for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAME-based theorem proving support provided in the toolkit for proving system properties, including timing properties. Several examples are provided by way of illustration.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2006
Accession Number
ADA462155

Entities

People

  • Hongping Lim
  • Myla M. Archer
  • Nancy Lynch
  • Sayan Mitra
  • Shinya Umeno

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Artificial Intelligence
  • Automata
  • Computational Science
  • Computer Science
  • Differential Equations
  • Intervals
  • Language
  • Machines
  • Mathematical Models
  • Military Research
  • Simulations
  • Simulators
  • Specifications
  • Standards
  • Translators

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.