@InProceedings{LKLM:formats05,
  author       = {Hongping Lim and Dilsun Kaynar and Nancy Lynch and Sayan Mitra},
  title        = {Translating timed {I/O} automata specifications for theorem proving in {PVS}},
  booktitle    = {Proceedings of Formal Modelling and Analysis of Timed Systems ({FORMATS'05})},
  year         = {2005},
  number       = {3829},
  series       = {LNCS},
  address      = {Uppsala, Sweden},
  month        = {September},
  publisher    = {Springer},
  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 the the translator in the verification process.},
  biburl       = {http://users.crhc.illinois.edu/mitras/research.html},
  keywords     = {Specification languages, Verification},
  optvolume    = {3829},
  pdfslidesurl = {research/presentations/FORMATS.pdf},
  pdfurl       = {research/2005/formats05.pdf},
  ppturl       = {research/presentations/FORMATS.pdf},
  url          = {http://www.springerlink.com/content/f715l136524q6527/},
}