UML[1] là ngôn ngữ được sử dụng phổ biến nhất trong ngành công nghiệp phần mềm vì tính dễ hiểu, trực quan và dễ thể hiện bằng công cụ. Trong những năm gần đây, OCL[5] được phát triển với mục đích là ngôn ngữ mô tả các ràng buộc cho các yếu tố mô hình UML[1] để mô hình UML[1] có ngữ nghĩa chặt chẽ hơn. Cho đến nay, để kiểm tra các ràng buộc của mô hình UML[1], chúng ta phải chuyển đặc tả UML[1] sang đặc tả bằng các ngôn ngữ có tính hình thức hóa cao hơn như là Z, B, OWL, Alloy[2].Alloy[2] đã được phát triển khá hoàn thiện cả về ngôn ngữ và công cụ phân tích tự động. Chúng ta có thể chuyển đổi mô hình UML[1] với đặc tả OCL[5] sang mô hình Alloy[2] và sử dụng công cụ phân tích AlloyAnalyzer để phân tích các yếu tố mô hình. Hiện nay, đã có nhiều nhóm tham gia nghiên cứu lý thuyết chuyển đổi đặc tả UML[1] và OCL[5] sang đặc tả Alloy[2] và xây dựng công cụ chuyển đổi tự động. Có thể kể đến công cụ UML2ALLOY[7]. Tuy nhiên, vẫn còn nhiều hạn chế trong việc nghiên cứu lý thuyết chuyển đổi đặc tả UML[1] với OCL[5] sang đặc tả Alloy[2] ví dụ như việc chuyển đổi quan hệ tam phân (hoặc lớn hơn quan hệ tam phân) giữa các lớp trong biểu đồ lớp sang đặc tả Alloy[2]. Khóa luận này tập trung vào tìm hiểu các quy tắc chuyển đổi các yếu tố mô hình UML[1] sang mô hình Alloy[2] đã được đề xuất trong các nghiên cứu khác và có đề xuất một số quy tắc chuyển đổi mới cho một số trường hợp đặc biệt. Khóa luận cũng thực hiện một ví dụ minh họa là “hệ thống quản lý các tài khoản và các giao dịch trên máy ATM”. Kết cấu của khóa luận như sau: Chương 1: Tổng quan UML và OCL Chương 2: Giới thiệu Alloy và công cụ phân tích Alloy Analyzer Chương 3: Chuyển đổi biểu đồ lớp UML với đặc tả OCL sang Alloy Chương4: Bài toán minh họa