@techreport{TR-IC-05-04,
  number = {IC-05-04},
  author = {Adilson Luiz Bonifácio e Arnaldo Vieira Moura},
  title = {Formal Verification and Parameters
           Synthesis for Hybrid Real Systems},
  month = {March},
  year = {2005}, 
  institution = {Institute of Computing, University of Campinas},
  note = {In English, 42 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       A hybrid system is given by a set of real-time reactive
       components, whose dynamic behavior results from the interplay
       of continuous and discrete events.  Hybrid system have been
       modeled using formal methods and results have been obtained
       using the accompanying computational tools.  Some such formal
       methods and tools are briefly presented, emphasizing their
       different characteristics.  The Hybrid Automata formalism is
       one among such methods.  A hybrid automaton is a finite state
       automaton where each state is extended to contain a description
       of a system dynamic profile.  Transitions between states model
       a change in the system dynamics, triggered by discrete events.
       In this work, hybrid automata are used to model realistic
       hybrid systems stemming from segments of a subway mesh and
       parts of an air traffic control system.  The models constructed
       are verified in this way using the support of computational
       tools.  Moreover, some important model parameters are
       synthesized using the same tools.  The verification certified
       that the systems operate safely.  The synthesis sessions
       arrived at tighter values for some operational system
       parameters, while still guaranteeing a safe operation.
  }
}