Meta-modeling Architecture Based Method for Transforming UML Class Diagram into PVS Specification.

UML has become the de-facto standard for object-oriented modeling. However, it is still an informal language without a precise semantics. PVS is higher-order logic formal specification language. Transforming UML diagram into formal specification was studied in order to combine the advantages of both languages. An approach for transforming UML class diagram into PVS specification was given. Following the four-layer architecture of UML, meta-meta-model, meta-model and UML diagram are formalized in three steps, and the result of each step provides a context foundation for the next formalization. This approach is better in decreasing difficulty, ensuring correctness, and can retain much semantics. [ABSTRACT FROM AUTHOR]