@techreport{TR-IC-12-09,
   number = {IC-12-09},
   author = {Adilson L. Bonifacio and Arnaldo V. Moura},
   title  =  {{Attaining a more Flexible and Manageable Discretization
                   for Complex Timed Systems}},
   month = {March},
   year = {2012},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 39 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       Complex  systems  have  been  widely  investigated using formal
       techniques  for testing and verifying critical aspects of their
       reactive  behavior.  Such  behavior  is usually captured by the
       notion  of  context  transformations  that  interact  with  the 
       environment. Other aspects require timed models to describe the
       systems' continuous evolution in time. In this work, we propose
       a timed context formalism able to model the combination of time
       evolution  and  context  transformations.  Further, we derive a
       more flexible and manageable strategy to discretize such models
       and  prove  correctness  of  the  discretized model against the
       original  one.  The  flexibility to find suitable granularities
       both  to  time  evolution  as  well  as  to  values  of context
       variables  opens  the possibility for constructing more compact
       grid automata. Based on this discretizing approach we present a
       testing  framework  to  automatically generate test suites from
       the  resulting  automata.  The  test suites can then be used to
       verify  properties of candidate implementations with the aid of
       test purposes.
  }
}