TIOA to PVS Translator
The TIOA to PVS translator (tioa2pvs) is a tool for translating TIOA descriptions to the language of PVS for the purpose of theorem proving.
NOTE: This site is outdated. Please refer to Veromodo.com for updated information.
Installation
Examples
Documentation
About the TIOA toolkit and TIOA to PVS translator
The TIOA toolkit, currently under
development, is a formal framework for system development
based on specifications in the TIOA language.
The TIOA toolkit aims to provide a specification simulator,
a code generator, and both model checking and theorem
proving support for analyzing specifications.
The TIOA framework for theorem proving, provides an approach for writing
a system specification in the TIOA language, translating the TIOA
description into the language of PVS, and then using PVS to verify
properties of the system.
The framework makes use of a PVS theory template which is
instantiated with the states, actions and transitions of an
automaton.
To perform this translation and instantiation automatically,
a translator tool has been developed as part of the TIOA
toolkit.
The TIOA methodology for theorem proving involves (1)
writing the specification of a system and its properties in
the TIOA language, (2) using the translator tool to generate
the PVS equivalent of the system, and then (3) proving the
properties in PVS using TAME strategies developed for TIOA.
The user describes the system in the TIOA language using the
state-transition structure.
The user writes simple program statements to describe
transitions, and specifies trajectories using differential
equations.
Once the TIOA description is type-checked by the front end of
the toolkit, the translator generates a set of PVS files.
Together with the TAME library containing PVS definitions
for timed I/O automata
and any additional data type theories, these
generated files specify the automaton and its properties.
The user then uses TAME strategies developed for TIOA to
prove the properties of the system in PVS.
Last modified April 18, 2006.
Please send questions and comments to Hongping Lim at hongping (at) mit (dot) edu.