| Abstract | When designing critical applications using the Unified Modeling Language, the system models are frequently projected into various mathematical domains (such as Petri nets, transition systems, process algebras, etc.) by model transformations to carry out a formal analysis of the system under design. In the current thesis, I introduce a general, visual yet mathematically precise framework for uniformly specifying a large scale of model transformations within and between modeling languages. I also propose automated means to reason about the correctness of transformations, and to generate a transformation program as the implementation from such high-level specifications. |
