@mastersthesis{UmenoSMThesis,
   author = "Shinya Umeno",
   title =  "Proving safety properties of an aircraft landing protocol using timed and untimed {I/O} automata: a case study",
   school="Massachusetts Institute of Technology",
   ADDRESS="Cambridge, MA",
   year   = "2006"
}