@inproceedings{b484c2938d9a42a19ef51e7aab5a93dc,
title = "Translating timed I/O automata specifications for theorem proving in PVS",
abstract = "Timed Input/Output Automaton (TIOA) is a mathematical framework for specification and analysis of systems that involve discrete and continuous evolution. In order to employ an interactive theorem prover in deducing properties of a TIOA, its state-transition based description has to be translated to the language of the theorem prover. In this paper, we describe a tool for translating TIOA to the language of the Prototype Verification System (PVS) - a specification system with an integrated interactive theorem prover. We describe the translation scheme, discuss the design decisions, and briefly present three case studies to illustrate the application of the translator in the verification process.",
author = "Hongping Lim and Dilsun Kaynar and Nancy Lynch and Sayan Mitra",
year = "2005",
doi = "10.1007/11603009_3",
language = "English (US)",
isbn = "3540309462",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "17--31",
booktitle = "Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings",
note = "3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005 ; Conference date: 26-09-2005 Through 28-09-2005",
}