@Phdthesis{Muthiayen:2000:PHD,
  author =       "Darmalingum Muthiayen",
  title =        "Real-Time Reactive System Development - A Formal Approach
                  Based on {UML} and {PVS}",
  school =       "Department of Computer Science at Concordia University,
                  Montreal, Canada",
  year =         "2000",
  month =         jan,
  abstract =     "The  scope  of this thesis   encompasses  three  major
                  components.   We develop a visual  technique for
                  object-oriented modeling  of real-time reactive  systems,
                  based on a minimal  set of extensions to UML, along with
                  a set of well-formedness rules for the real-time models. 
                  We then present a formalization of  the Real-Time UML
                  (RTUML) notation, making use of the abstract syntax and
                  well-formedness rules of UML metamodel, and provide
                  formal denotational  and operational semantics for 
                  RTUML. Finally, we introduce a   methodology for
                  mechanized   verification of time-dependent  properties
                  in  the RTUML design  of real-time reactive systems, 
                  within   the   PVS verification  environment.    The 
                  formal semantics   of   RTUML provides a    foundation  
                  for the verification methodology, and for rigorous
                  analysis and validation techniques.  The novelty of the
                  development  methodology for real-time systems  lies in
                  the    mechanized    verification   approach  
                  superimposed   on   the object-oriented modeling
                  technique.",
}