Luận văn: Mô hình hóa ứng dụng web bằng ngôn ngữ đặc tả Alloy - Đại học Bách Khoa Hà Nội

Luận văn mô hình hóa ứng dụng web bằng Alloy. Tìm hiểu cách sử dụng ngôn ngữ đặc tả Alloy để mô hình hóa và phân tích ứng dụng web. Tải luận văn PDF.

• Tác giả: Lê Thị Thu Trang
• Người hướng dẫn: Ts. Trần Đức Khánh
• Trường học: Trường Đại Học Bách Khoa Hà Nội
• Chuyên ngành: Công Nghệ Thông Tin
• Đề tài: Mô Hình Hóa Ứng Dụng Web Bằng Ngôn Ngữ Đặc Tả Alloy
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2014
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• DANH MỤC CÁC HÌNH
• DANH MỤC CÁC BẢNG
• 1. CHƯƠNG I: BÀI TOÁN VẤN ĐỀ VÀ GIẢI PHÁP
• 1.1. Ngôn ngữ mô hình hóa Alloy
• 1.2. Hệ quản trị cơ sở dữ liệu SQL Server
• 2. CHƯƠNG II: MÔ HÌNH HÓA FORUM BẰNG NGÔN NGỮ ALLOY
• 2.1. Nội dung, thành phần đối tượng và chính sách truy cập của forum
• 2.1.1. Nội dung trang web
• 2.1.2. Các thành phần đối tượng của forum
• 2.1.3. Các chính sách truy cập
• 2.2. Mô hình hóa forum bằng Alloy
• 2.2.1. Cấu trúc chung của một chương trình Alloy
• 2.2.2. Các thành phần forum
• 2.2.3. Các ràng buộc toàn vẹn
• 2.2.4. Chính sách truy cập
• 2.3. Phân tích, kiểm tra mô hình
• 2.3.1. Read User Password
• 3. CHƯƠNG III: CÀI ĐẶT, XÂY DỰNG HỆ THỐNG QUẢN LÝ FORUM
• 3.1. Xây dựng cơ sở dữ liệu trên SQL
• 3.2. Xây dựng lớp chính sách truy cập
• 3.3. Thiết kế giao diện forum
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan về Mô Hình Hóa Ứng Dụng Web Với Alloy 55

Ngày nay, việc bảo vệ thông tin lưu trữ trở thành yếu tố then chốt đối với mọi website, đặc biệt là những trang web lưu trữ dữ liệu nhạy cảm của người dùng như thông tin cá nhân, tài khoản ngân hàng. Để đáp ứng nhu cầu này, nhiều phương pháp đã được phát triển nhằm xây dựng các trang web có khả năng bảo mật dữ liệu cao. Luận văn này tập trung vào việc nghiên cứu một phương pháp trong số đó: Mô hình hóa ứng dụng web bằng ngôn ngữ mô hình hóa Alloy, tập trung vào các ràng buộc và chính sách truy cập nhằm đảm bảo an toàn thông tin. Phân tích mô hình sử dụng Alloy Analyzer để kiểm tra các ràng buộc và chính sách này. Tiếp theo, sử dụng công cụ lập trình ASP.NET để cài đặt website theo ba thành phần chính: cơ sở dữ liệu, chính sách truy cập và giao diện người dùng. Trang web diễn đàn cung cấp thông tin học bổng, giải thưởng của các quỹ học bổng dành cho sinh viên trường Đại học Hồng Đức sẽ được cài đặt thử nghiệm trong luận văn này. Theo Lê Thị Thu Trang trong luận văn thạc sĩ kỹ thuật, mục tiêu là xây dựng một hệ thống tin cậy thông qua mô hình hóa hình thức (Formal Modeling). Luận văn gồm hai phần chính: lý thuyết về ngôn ngữ đặc tả Alloy, phương pháp mô hình hóa ứng dụng web sử dụng Alloy; giới thiệu chung về SQL, ASP. Phần thứ hai tập trung vào thiết kế và mô hình hóa forum cung cấp thông tin học bổng theo các nguyên tắc đã nêu ở phần đầu. Cài đặt thử nghiệm hệ thống và đánh giá phương pháp xây dựng website này.Luận văn nghiên cứu về ngôn ngữ, mô hình và cách thức mô hình hóa một trang web, thúc đẩy xử lý và phân tích một trang web, áp dụng mô hình hóa forum cung cấp thông tin lọc bổng, giải thưởng của các quỹ học bổng dành cho sinh viên.

1.1. Giới thiệu về Ngôn Ngữ Đặc Tả Alloy Ưu Điểm và Hạn Chế

Ngôn ngữ đặc tả Alloy là một ngôn ngữ mô hình hóa hình thức dựa trên logic bậc nhất, cho phép mô tả cấu trúc và ràng buộc của các hệ thống phần mềm. Ưu điểm của Alloy nằm ở khả năng biểu diễn các khái niệm phức tạp một cách ngắn gọn và chính xác, cũng như khả năng tự động kiểm tra tính nhất quán và đầy đủ của mô hình bằng công cụ Alloy Analyzer. Tuy nhiên, Alloy cũng có những hạn chế nhất định, như khả năng mở rộng hạn chế và khó khăn trong việc mô hình hóa các khía cạnh động của hệ thống. Alloy thích hợp cho việc xây dựng phần mềm tin cậy và đảm bảo chất lượng phần mềm. Việc nắm vững cú pháp Alloy là rất quan trọng. Alloy cung cấp một cách tiếp cận hiệu quả cho Verification and Validation (V&V) trong phát triển phần mềm.

1.2. Tại Sao Mô Hình Hóa Ứng Dụng Web Lại Quan Trọng

Mô hình hóa ứng dụng web trở nên quan trọng hơn bao giờ hết trong bối cảnh các ứng dụng web ngày càng phức tạp và yêu cầu tính bảo mật cao. Bằng cách sử dụng các ngôn ngữ mô hình hóa như Alloy, các nhà phát triển có thể xác định và giải quyết các vấn đề tiềm ẩn trước khi chúng phát sinh trong quá trình triển khai, từ đó giảm thiểu rủi ro và chi phí. Mô hình hóa chức năng web, mô hình hóa dữ liệu web, và mô hình hóa tương tác người dùng đều đóng vai trò quan trọng. Các vấn đề về mô hình hóa bảo mật web cũng cần được xem xét kỹ lưỡng để đảm bảo an toàn cho dữ liệu và người dùng.

II. Thách Thức và Giải Pháp Ứng Dụng Alloy Cho Web 58

Việc áp dụng Ngôn ngữ đặc tả Alloy trong mô hình hóa ứng dụng web không phải là một quá trình đơn giản. Các thách thức bao gồm việc biểu diễn các khía cạnh động của ứng dụng web, quản lý độ phức tạp của mô hình, và đảm bảo tính khả mở rộng của mô hình. Tuy nhiên, bằng cách sử dụng các kỹ thuật và phương pháp phù hợp, những thách thức này có thể được vượt qua. Một giải pháp là tập trung vào các khía cạnh quan trọng nhất của ứng dụng web, sử dụng các trừu tượng hóa để giảm độ phức tạp, và sử dụng các công cụ và kỹ thuật hỗ trợ phân tích mô hình Alloy. Theo luận văn, các bước bao gồm: Xây dựng nội dung trang web, xác định các thành phần đối tượng của forum, xây dựng các chính sách truy cập, bao gồm xây dựng các Facts (yêu cầu mà mô hình hệ thống luôn phải đáp ứng), xây dựng các Capabilities (phân quyền), xây dựng các Preconditions và Post-conditions (điều kiện trước và sau khi thêm/xóa dữ liệu), và xây dựng các Triggers (điều kiện khi thêm/xóa dữ liệu). Sau đó sử dụng Alloy Analyzer để kiểm tra.

2.1. Vượt Qua Khó Khăn trong Mô Hình Hóa Tương Tác Người Dùng

Một trong những thách thức lớn nhất trong mô hình hóa ứng dụng web là biểu diễn các tương tác phức tạp giữa người dùng và ứng dụng. Điều này đòi hỏi phải mô hình hóa trạng thái của ứng dụng, các sự kiện do người dùng kích hoạt, và các hành động mà ứng dụng thực hiện để đáp ứng các sự kiện đó. Để giải quyết vấn đề này, có thể sử dụng các kỹ thuật như máy trạng thái hữu hạn (finite state machines) hoặc các mô hình dựa trên sự kiện (event-based models) để mô tả các tương tác người dùng một cách chính xác và dễ hiểu. Quan trọng là phải xác định rõ các chính sách truy cập và ràng buộc liên quan đến từng loại tương tác.

2.2. Giải Quyết Vấn Đề Mở Rộng và Hiệu Năng Performance and Scalability

Khi mô hình hóa ứng dụng web, cần xem xét đến khả năng mở rộng và hiệu năng của ứng dụng. Mô hình cần phải có khả năng thích ứng với sự gia tăng về số lượng người dùng, dữ liệu, và chức năng. Điều này đòi hỏi phải sử dụng các kỹ thuật như phân vùng dữ liệu, cân bằng tải, và bộ nhớ đệm (caching). Bên cạnh đó, cần phải đánh giá hiệu năng của mô hình bằng cách sử dụng các công cụ Performance analysis Alloy và Scalability Alloy, từ đó xác định các điểm nghẽn và tối ưu hóa mô hình.

III. Phương Pháp Xây Dựng Mô Hình Alloy Cho Ứng Dụng Web 57

Để xây dựng một mô hình Alloy hiệu quả cho ứng dụng web, cần tuân thủ một quy trình rõ ràng và có cấu trúc. Quy trình này thường bao gồm các bước sau: xác định phạm vi và mục tiêu của mô hình, thu thập yêu cầu, thiết kế mô hình, cài đặt mô hình, kiểm tra mô hình và xác nhận mô hình. Trong quá trình thiết kế mô hình, cần xác định các thành phần chính của ứng dụng web, các mối quan hệ giữa chúng, và các ràng buộc mà chúng phải tuân thủ. Việc áp dụng mô hình hóa hình thức (Formal Modeling) giúp đảm bảo tính chính xác và tin cậy của mô hình. Sử dụng các ví dụ Alloy và case study Alloy sẽ giúp hiểu rõ hơn về cách áp dụng Alloy trong thực tế.

3.1. Xác Định Nội Dung Đối Tượng và Chính Sách Truy Cập

Theo luận văn, việc mô hình hóa forum bắt đầu bằng việc xây dựng nội dung trang web, xác định các thành phần đối tượng (ví dụ: người dùng, bài viết, bình luận), và xác định các chính sách truy cập (ví dụ: ai có quyền đọc, sửa, xóa bài viết). Sau khi xác định được các yếu tố này, có thể bắt đầu xây dựng mô hình Alloy bằng cách sử dụng các chữ ký (signatures) để biểu diễn các thành phần, các trường (fields) để biểu diễn các thuộc tính, và các ràng buộc (constraints) để biểu diễn các quy tắc. Việc xây dựng các Faets (yêu cầu mà mô hình hệ thống luôn phải đáp ứng), Capabilities (phân quyền), Preconditions và Post-conditions (điều kiện trước và sau khi thêm/xóa dữ liệu), và Triggers (điều kiện khi thêm/xóa dữ liệu) là rất quan trọng.

3.2. Sử Dụng Alloy Analyzer Để Phân Tích và Kiểm Tra Mô Hình

Alloy Analyzer là một công cụ mạnh mẽ cho phép tự động phân tích và kiểm tra các mô hình Alloy. Bằng cách sử dụng Alloy Analyzer, có thể tìm ra các lỗi tiềm ẩn trong mô hình, như các ràng buộc không nhất quán, các trường hợp không mong muốn, hoặc các lỗ hổng bảo mật. Alloy Analyzer hoạt động bằng cách tìm kiếm các thể hiện (instances) của mô hình thỏa mãn tất cả các ràng buộc. Nếu không tìm thấy thể hiện nào, điều đó có nghĩa là mô hình có lỗi. Việc kiểm chứng mô hình Alloy bằng Alloy Analyzer là một bước quan trọng trong quy trình xây dựng mô hình.

IV. Ứng Dụng Thực Tiễn Mô Hình Hóa Forum Học Bổng Bằng Alloy 60

Luận văn minh họa cách áp dụng ngôn ngữ đặc tả Alloy để mô hình hóa một diễn đàn học bổng, nơi cung cấp thông tin về các chương trình học bổng và giải thưởng cho sinh viên. Mô hình Alloy của diễn đàn này bao gồm các thành phần như người dùng (sinh viên, quản trị viên), bài viết (thông báo học bổng, câu hỏi), bình luận, và các chính sách truy cập (ai có quyền tạo bài viết, ai có quyền bình luận). Bằng cách sử dụng Alloy Analyzer, tác giả đã kiểm tra và xác nhận tính đúng đắn của mô hình, đảm bảo rằng các chính sách truy cập được thực thi một cách chính xác và không có lỗ hổng bảo mật. Diễn đàn này cung cấp thông tin lọc bổng, giải thưởng của các quỹ học bổng dành cho sinh viên trường Đại học Hồng Đức.

4.1. Xây Dựng Cơ Sở Dữ Liệu và Lớp Chính Sách Truy Cập

Sau khi phân tích và kiểm tra mô hình Forum, luận văn tiếp tục với việc xây dựng cơ sở dữ liệu dựa trên các Signature của mô hình. Sau đó, xây dựng lớp chính sách truy cập, đảm bảo rằng các quyền hạn được thực thi một cách chính xác. Việc xây dựng cơ sở dữ liệu phải phản ánh chính xác cấu trúc và các mối quan hệ được mô tả trong mô hình Alloy. Việc đảm bảo tính nhất quán giữa mô hình và cơ sở dữ liệu là rất quan trọng để đảm bảo tính tin cậy của ứng dụng web.

4.2. Thiết Kế Giao Diện Forum Dựa Trên Mô Hình Alloy

Giao diện người dùng của diễn đàn được thiết kế dựa trên mô hình Alloy, đảm bảo rằng người dùng chỉ có thể thực hiện các hành động mà họ được phép theo chính sách truy cập. Ví dụ, chỉ có quản trị viên mới có quyền tạo bài viết thông báo học bổng, trong khi sinh viên chỉ có quyền bình luận và đặt câu hỏi. Thiết kế giao diện phải trực quan và dễ sử dụng, đồng thời tuân thủ các nguyên tắc bảo mật. Luận văn trình bày các hình ảnh về giao diện trang chủ, section, topic, panel tạo topic, và panel xem thông tin user.

V. Kết Luận và Hướng Phát Triển Luận Văn Về Alloy 55

Luận văn Alloy này đã trình bày một phương pháp tiếp cận hiệu quả để mô hình hóa ứng dụng web bằng ngôn ngữ đặc tả Alloy, tập trung vào việc đảm bảo tính bảo mật và tin cậy của ứng dụng. Bằng cách sử dụng Alloy Analyzer, tác giả đã kiểm tra và xác nhận tính đúng đắn của mô hình, từ đó giảm thiểu rủi ro và chi phí trong quá trình phát triển. Trong tương lai, có thể mở rộng nghiên cứu này bằng cách khám phá các kỹ thuật tích hợp Alloy vào quy trình phát triển phần mềm, hoặc bằng cách áp dụng Alloy cho các loại ứng dụng web khác nhau. Nghiên cứu sâu hơn về so sánh Alloy với các ngôn ngữ đặc tả khác như Z, B, TLA+ cũng rất hữu ích.

5.1. Đánh Giá Ưu Điểm và Hạn Chế Của Phương Pháp Mô Hình Hóa

Phương pháp mô hình hóa bằng Alloy có nhiều ưu điểm, như khả năng biểu diễn các khái niệm phức tạp một cách ngắn gọn và chính xác, khả năng tự động kiểm tra tính nhất quán và đầy đủ của mô hình, và khả năng tìm ra các lỗi tiềm ẩn trong mô hình. Tuy nhiên, phương pháp này cũng có những hạn chế, như độ phức tạp của ngôn ngữ Alloy, khó khăn trong việc mô hình hóa các khía cạnh động của ứng dụng web, và yêu cầu kiến thức chuyên môn về mô hình hóa hình thức. Cần cân nhắc kỹ lưỡng các ưu điểm và hạn chế này trước khi quyết định áp dụng phương pháp này.

5.2. Hướng Nghiên Cứu Tiếp Theo và Ứng Dụng Thực Tế Mở Rộng

Hướng nghiên cứu tiếp theo có thể tập trung vào việc phát triển các công cụ và kỹ thuật hỗ trợ mô hình hóa ứng dụng web bằng Alloy, hoặc vào việc áp dụng Alloy cho các lĩnh vực khác, như mô hình hóa hệ thống phân tán, mô hình hóa hệ thống nhúng, hoặc mô hình hóa hệ thống an toàn. Ngoài ra, có thể nghiên cứu các phương pháp tích hợp Alloy vào quy trình phát triển phần mềm, từ đó giúp các nhà phát triển xây dựng các ứng dụng web bảo mật và tin cậy hơn. Nghiên cứu về khóa luận tốt nghiệp Alloy và đề tài Alloy sẽ giúp thúc đẩy ứng dụng Alloy trong học thuật và thực tế.

Trích đoạn nội dung tài liệu

BO GIAO DUC VA BAO TAO TRUONG DAI HQC BACH KHOA HA NOI # LÊ THỊ THU TRANG MÔ HÌNH HÓA ỨNG DỤNG WEB BẰNG NGÔN NGỮ ĐẶC TẢ ALLOY Chuyên ngành: CÔNG NGHỆ THÔNG TIN LUẬN VĂN THẠC SĨ KỸ THUẬT NGƯỜI HƯỚNG DẪN KHOA HỌC TS. TRAN DUC KHANH HaNoi Năm 2014 LOI CAM ON 8 hoan thành được luận văn nảy tôi đã nhận được rất nhiều sự động viên, giúp đỡ của nhiều cá nhân và tập thể. Trước hết, tôi xin bảy tổ lòng biết ơn sâu sắc dén thay giao TS. Tran Đức Khánh đã giao dé tai va tan tinh hướng đẫn tỏi trong suốt quá trinh hoản thành luận văn này Xin cùng hảy tỏ làng biết ơn chân thành tới các thảy cô giáo, người đã đem lại cho tôi những kiên thúc bỗ trợ vô cùng có ích trong những nắm học vừa qua.

Cũng xin gửi lời cảm ơn chân thành tới Ban lãnh đạo Viện Sau Đại Học, Viện Công Nghệ Thông Tin & Truyền Thông uủa trường Đại Học Bách Khoa Hà Nội đã tạo điều kiện cho tôi trong quá trình học tập. Cuối cùng tôi xin gửi lời cam on dén gia dinh, bạn bẻ, những người đã luôn bên tối, động viên và khuyến khích tôi trong quả trình thực hiện đề tài nghiên cửu. của mình Tủ đã có rất nhiều cổ gắng, xong luận văn không tránh khối những hạn chế, thiểu xót. Kính mong nhận được sự chia sẻ và những ý kiên chỉ dẫn, góp ý quý bau của quý thầy cô và bạn be đồng nghiệp.

Trân trong! LOI CAM DOAN Tôi xin cam đoan đây là đề tài nghiên cứu của bản thân tôi, được xuất phat th những vẫn đề cấp thiết trong xã hội và sự phát triển của công nghệ thông tu. Các số liệu cỏ nguồn gốc rõ ràng, tuân thủ đúng nguyên tắc và kết quả trình bày trong luận văn được thu thập trong quá trình nghiên cứu là trưng thực và chính xáo 1Hà Nội, ngày 20 tháng 09 năm 2014 Tác giả luận văn Lê Thị Thu Trang nm Hinh 35 - Panel xem théng tin User. aa wo n Hinh 36 - Panel lao User mt. TOM TAT NOI DUNG LUAN VAN Nội đụng của luận văn gồm các phân chính sau: 1.

Nghiên cửu ngôn ngữt mô hình hóa Alloy. Nghiễn cửu về ngôn ngữ, mô hình. Cách thức mô hình hỏa một trang web. thúc xú lý và phân tích một trang web, để từ đó áp dụng mô hình hóa forum cung cấp thông tim lọc bổng, giải thưởng của các quỹ học bỏng dành cho sinh viên trường Đại học Hồng Đức 2.

Mô hình hóa Forum bang Alloy: Mô hình dược mô bình hỏa dựa trên các bước sau: « Xây dụng nội dung Irang web «Xác định các thành phần đối tượng của [run «_- Xây dụng các chính sách truy cập bao gồm: © Xây dựng các Faets: Các yên cầu mà mô hình hệ thống luôn luôn phải đắp ứng, o Xây đựng cáo Capabililes: Các capabilitiss này phân quyển cho các kiểu người đảng dưới các quyền đọc, sửa, lạo mới, xóa o Xây dựng các Precondiions vả Post-conditions: Các diểu kiện trước và sau khi ađd hoặc đelete đữ liệu o_ Xây đựng các Triggera: Các điêu kiện khi add bolic delete dit én Sau khi đã mô hình hóa forau. Sử dụng bộ phân tích tự động Alloy Analyzer trong việc phần tích, kiểm tra với tắt cả các trường hợp đọc, thêm, sửa, xóa các thành phẩn trong forum. Xây dựng cơ sở đữ liệu Sau khi phan tích và kiếm tra mô hình Forum, ta sẽ dựa vào các Signature của mô hình và xảy dựng được cơ sở dữ liệu. Xây dựng lớp chính sách truy cập 5.

Thiết kế giao điện forum. DANIIMYC CAC TINH Hinh 1 - Vi đụ về quan hệ trong Alloy 13 Hình 2 - Quan bệ hàm 14 Hình 3 - Phân tích mỏ hình Alloy. 20 Hình 4 - Các thánh phần Forum. 27 Hình 5 - Các faet của mô hình sen.

20 Hinh 6 - Predicate show Forum 30 Hình 7 - Kết quả show Forum 31 Hinh 8 - Capabilities 32 Ilinh 9 - Pre-conditions & Post-conditions & Triggers. 33 Ilinh 10 - Add Topic. 3⁄4 Hinh 11 - Kết quả pred AddTopie. ¬— ¬— seen IS Hinh 12 - Ket qua assertion Add/opicPolicy 35 Hinh 13 - Add Reply.-- Hình 14 - Kết quả pred AddReply 37 Hinh 15 - Két qua assertion AddReplyPolicy 37 Hinh 16 - Predicate DelReply 38 Ilinh 17 - Két qua Predicate DelReply 38 Ilinh 18 - Predicate DelTopic 39 Hinh 19- Két qua Predicate DelTepie.

39 Hinh 20- Predieate readUserPassword & Assertion. co see 40 Hinh 21 - Kết qua Predicate readUserPassword voi trường hợp ngngười dùng, la User 4 Hình 22 - Kết qué Prodicale readUserPassword với trường hợp người dùng là Admin 4 Ilinh 23 - Két qua Assertion readUserPassword al Ilinh 24 - Predicate editReadOnly 42 Hinh 25 - Kết quả Predicate editteadOnhy 42 Hinh 26 - Predicate edit Topic. AB Hinh 27 - Kết quả Predicate edifLopic. ¬— ¬— see Hình 28 - Lược để quan hệ CSDI, 7 Hình 29 - Hàm checkCapabilities 48 Tình 30 - Cac ham RPC 50 Hình 31 - Giao điên trang chủ 52 Ilinh 32 - Giao điện Sectien 53 Ilinh 33 - Giao điện Tapie 34 Hinh 34 - Panel tạo Topic mới.

58 DANIIMUC CAC BANG Bang User trong CSDL 44 Bang Section trong CSDL. 44 Bang ‘Lopic trong CSDL 45 Bang Reply tong CSDL 45 Bang My¥he tong CSDL. 46 MỤC LỤC LOI CAM DOAN. DANH MỤC CÁC HÌNH.

DANH MỤC CÁC BANG. - CHUONG I: BAT VẤN ĐÈ VẢ GIẢI PHÁP. Ngôn ngữ mô hình hóa Allyy. Hệ quân trị cơ sỡ dữ liệu SỢL Server 2.

CHƯƠNG II: MÔ HÌNH HÓA FORUM BẰNG NGÔN NGỮ ALLOY. Nội dung, thành phan đối tượng và chính sách truy cập của forum 24 1. Nội dung trang web. Các thành phản đối tượng của forum.

Các chính sách truy cập 2. Mô hình hóa forum bằng Alloy 2. Cấu trúc chung của một chương trình Alloy. Các thành phân ferum 2.

Các ràng buộc toàn vẹn 2. Chỉnh sách truy cập 3. Phân (ích, kiểm tra mô hình 3. Read User Password 3.

MỤC LỤC LOI CAM DOAN. DANH MỤC CÁC HÌNH. DANH MỤC CÁC BANG. - CHUONG I: BAT VẤN ĐÈ VẢ GIẢI PHÁP.

Ngôn ngữ mô hình hóa Allyy. Hệ quân trị cơ sỡ dữ liệu SỢL Server 2. CHƯƠNG II: MÔ HÌNH HÓA FORUM BẰNG NGÔN NGỮ ALLOY. Nội dung, thành phan đối tượng và chính sách truy cập của forum 24 1.

Nội dung trang web. Các thành phản đối tượng của forum. Các chính sách truy cập 2. Mô hình hóa forum bằng Alloy 2.

Cấu trúc chung của một chương trình Alloy. Các thành phân ferum 2. Các ràng buộc toàn vẹn 2. Chỉnh sách truy cập 3.

Phân (ích, kiểm tra mô hình 3. Read User Password 3. Hinh 35 - Panel xem théng tin User. aa wo n Hinh 36 - Panel lao User mt.

CHƯƠNG TH: CẢI ĐẠT, XÂY DUNG THE THONG QUAN LY FORUM 44 1. Xây dựng cơ sở đữ liệu trên SQLL. Xây dựng kín chính sách Iruy cập 48 3. Thiết kế gìao điện forum.

TẢI LIỆU THAM KHÃO. - 58 DANIIMYC CAC TINH Hinh 1 - Vi đụ về quan hệ trong Alloy 13 Hình 2 - Quan bệ hàm 14 Hình 3 - Phân tích mỏ hình Alloy. 20 Hình 4 - Các thánh phần Forum. 27 Hình 5 - Các faet của mô hình sen.

20 Hinh 6 - Predicate show Forum 30 Hình 7 - Kết quả show Forum 31 Hinh 8 - Capabilities 32 Ilinh 9 - Pre-conditions & Post-conditions & Triggers. 33 Ilinh 10 - Add Topic. 3⁄4 Hinh 11 - Kết quả pred AddTopie. ¬— ¬— seen IS Hinh 12 - Ket qua assertion Add/opicPolicy 35 Hinh 13 - Add Reply.-- Hình 14 - Kết quả pred AddReply 37 Hinh 15 - Két qua assertion AddReplyPolicy 37 Hinh 16 - Predicate DelReply 38 Ilinh 17 - Két qua Predicate DelReply 38 Ilinh 18 - Predicate DelTopic 39 Hinh 19- Két qua Predicate DelTepie.

39 Hinh 20- Predieate readUserPassword & Assertion. co see 40 Hinh 21 - Kết qua Predicate readUserPassword voi trường hợp ngngười dùng, la User 4 Hình 22 - Kết qué Prodicale readUserPassword với trường hợp người dùng là Admin 4 Ilinh 23 - Két qua Assertion readUserPassword al Ilinh 24 - Predicate editReadOnly 42 Hinh 25 - Kết quả Predicate editteadOnhy 42 Hinh 26 - Predicate edit Topic. AB Hinh 27 - Kết quả Predicate edifLopic. ¬— ¬— see Hình 28 - Lược để quan hệ CSDI, 7 Hình 29 - Hàm checkCapabilities 48 Tình 30 - Cac ham RPC 50 Hình 31 - Giao điên trang chủ 52 Ilinh 32 - Giao điện Sectien 53 Ilinh 33 - Giao điện Tapie 34 Hinh 34 - Panel tạo Topic mới.

58 MO DAU Ngày nay, khi Internet ngay cảng phát triển, vẫn dễ bảo vệ thông tin lưu trữ là vẫn đề thiết yếu cúa một website, nhất lá đối với những website có chứa nhiều đữ liệu người dùng ( vi dụ : thông tin cá nhân, lài khoản ngân háng. Chính vị nhụ cầu đỏ, rất nhiều phương pháp đã ra dời nhằm xây dựng những website có khá năng, bảo mật đữ liệu cao. Luận văn của em sẽ tập trung nghiên cứu một phương pháp trong số đó : mô hình hóa website bằng ngôn ngữ mô hinh hóa Alloy với các ràng. buộc vả chính sách truy cập nhằm đảm báo an toàn thông tin dữ liệu, phân tích mô hình sử dụng Alloy Analyzer để kiểm tra các rằng buộc và chính sách đó, sau đó sử dụng công cụ lập trình ASP.NET để cài đãi website theo 3 thành phản chính : cơ sở dữ liệu, chính sách truy cập, giao diện người dừng, Thư đã nói ở trên, website em sẽ thục biện cài đặt thử nghiệm trong luận văn nay 14 mat website điễn đản cúng cấp thông tin học bồng, giải thưởng của các quỹ học béng danh cho sinh viễn trường Đại học Hồng Đức.

Luận văn gảm 2 phân chính : * Phản 1 : Lý tuyết về ngôn ngữ đặc tả Alloy, phương pháp mô hình hoa website sứ dụng Alloy. Giới thiệu chung về SQL, ASP. * Phan2 : Thiết kế, mö hình hỗ y dung forun cúng câp thông Lin học bổng, giải thưởng của các quỹ học bóng dành cho sinh viên trường Đại học Léng Dire thes các nguyên tắc đã nêu ở phần 1. Cài đặt thử nghiệm hệ thống và qua đó đánh giá phương pháp xây dựng website này.

MO DAU Ngày nay, khi Internet ngay cảng phát triển, vẫn dễ bảo vệ thông tin lưu trữ là vẫn đề thiết yếu cúa một website, nhất lá đối với những website có chứa nhiều đữ liệu người dùng ( vi dụ : thông tin cá nhân, lài khoản ngân háng. Chính vị nhụ cầu đỏ, rất nhiều phương pháp đã ra dời nhằm xây dựng những website có khá năng, bảo mật đữ liệu cao. Luận văn của em sẽ tập trung nghiên cứu một phương pháp trong số đó : mô hình hóa website bằng ngôn ngữ mô hinh hóa Alloy với các ràng.