@techreport{TR-IC-09-31,
   number = {IC-09-31},
   author = {Adilson Luiz Bonifácio and Arnaldo Vieira Moura},
   title  =  {A  New  Timed  Discretization  Method for Automatic Test
                   Generation for Timed Systems},
   month = {September},
   year = {2009},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 33 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       Devising  formal  techniques and methods that can automatically
       generate  test  case  suites  for  timed systems has remained a
       challenge.  In  this  work  we  use Timed Input/Output Automata
       (TIOA)  as  a  formal specification model for timed systems. We
       propose  and  prove  the  correctness of a new and more general
       discretization  method that can be used to obtain grid automata
       corresponding   to   specification   TIOA,   using  almost  any 
       granularity  of  interest.  We also show how test purposes, for
       modeling  specific system properties, can be used together with
       the  specification TIOA in order to generate grid automata that
       captures  the  behavior  of both the specification and the test
       purpose. From such grid automata one can, then, algorithmically
       extract  test  suites  that can be used to verify whether given
       implementations  conform  to  the specification and reflect the
       desired properties.
  }
}