Tài liệu Nghiên cứu và xây dựng công cụ hỗ trợ mô hình hóa hệ thống Triggers bằng event -B

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NÔNG THỊ OANH NGHIÊN CỨU VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ MÔ HÌNH HÓA HỆ THỐNG TRIGGERS BẰNG EVENT-B LUẬN VĂN THẠC SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội – 2013 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NÔNG THỊ OANH NGHIÊN CỨU VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ MÔ HÌNH HÓA HỆ THỐNG TRIGGERS BẰNG EVENT-B Ngành: Công nghệ thông tin Chuyên ngành: Hệ thống thông tin Mã số: 60 48 05 LUẬN VĂN THẠC SĨ NGÀNH CÔNG NGHỆ THÔNG TIN NGƢỜI HƢỚNG DẪN KHOA HỌC: PGS.TS TRƢƠNG NINH THUẬN Hà Nội – 2013 -1- MỤC LỤC Danh mục bảng biểu .......................................................................................... 3 Danh mục hình vẽ ............................................................................................. 4 Danh mục từ viết tắt .......................................................................................... 6 Mở đầu............................................................................................................... 6 Chƣơng 1: TỔNG QUAN VỀ TRIGGER CƠ SỞ DỮ LIỆU .......................... 8 1.1 KHÁI NIỆM........................................................................................ 8 1.2 TẠO TRIGGER .................................................................................. 9 1.3 CÁC THÀNH PHẦN CỦA TRIGGER ............................................. 11 1.3.1 Sự kiện hoặc câu lệnh trigger........................................................ 11 1.3.2 Điều kiện trigger ........................................................................... 13 1.3.3 Hành động trigger ......................................................................... 13 1.4 PHÂN LOẠI TRIGGER .................................................................... 14 1.5 QUẢN LÝ TRIGGER ....................................................................... 15 1.5.1 Phân biệt trigger cơ sở dữ liệu ...................................................... 16 1.5.2 Thay đổi trạng thái của trigger cơ sở dữ liệu ................................ 17 1.5.3 Hủy bỏ trigger cơ sở dữ liệu ......................................................... 17 1.6 KHÁC NHAU GIỮA CÁC RÀNG BUỘC VÀ TRIGGER ............. 17 Chƣơng 2 : NGÔN NGỮ EVENT – B ............................................................ 19 2.1 NGÔN NGỮ EVENT – B ................................................................ 19 2.1.1 Máy và Ngữ cảnh .......................................................................... 20 2.1.1. Cấu trúc của máy ..................................................................... 20 2.1.2 Cấu trúc của Ngữ cảnh .............................................................. 21 2.2 Sự kiện.............................................................................................. 22 2.3 Quá trình làm mịn .............................................................................. 24 2.3.1 Tái sử dụng biến ............................................................................ 25 2.3.2 Giới thiệu sự kiện mới .................................................................. 25 2.3.3 Witness .......................................................................................... 25 2.4 Phân rã và kết hợp .............................................................................. 25 Học viên: Nông Thị Oanh - K18HTTT -2- Chƣơng 3: MÔ HÌNH HÓA VÀ KIỂM CHỨNG HỆ THỐNG TRIGGER BẰNG EVENT – B .................................................................................. 27 3.1 MÔ HÌNH HÓA HỆ THỐNG CƠ SỞ DỮ LIỆU ............................. 27 3.2 HÌNH THỨC HÓA TRIGGER.......................................................... 28 3.3 KIỂM CHỨNG THUỘC TÍNH HỆ THỐNG ................................... 28 3.4 VÍ DỤ ................................................................................................. 29 3.4.1 Mô tả ví dụ .................................................................................... 30 3.4.2 Mô hình hóa ví dụ ......................................................................... 30 3.4.3 Kiểm tra thuộc tính ....................................................................... 32 3.5 CÁC NGHIÊN CỨU LIÊN QUAN ................................................... 32 Chƣơng 4: XÂY DỰNG CÔNG CỤ HỖ TRỢ MÔ HÌNH HÓA TRIGGER BẰNG EVENT – B ............................................................... 33 4.1 PHÂN TÍCH BÀI TOÁN .................................................................. 33 4.2 THIẾT KẾ HỆ THỐNG .................................................................... 33 4.3 ĐÁNH GIÁ MỘT SỐ KẾT QUẢ ĐẠT ĐƢỢC CỦA CHƢƠNG TRÌNH...................................................................................................... 42 Kết luận ............................................................................................................ 42 Tài liệu tham khảo ........................................................................................... 44 Phụ lục ............................................................................................................. 45 Học viên: Nông Thị Oanh - K18HTTT -3- DANH MỤC BẢNG BIỂU Bảng 2.1 Luật sinh mệnh đề cần chứng minh để bảo toàn bất biến 27 Bảng 3.1 Sự chuyển đổi giữa hệ thống cơ sở dữ liệu và các khái niệm Event-B 29 Bảng 3.2 Mô hình hóa một trigger bằng sự kiện Event - B 29 Bảng 3.3: Chuyển đổi các câu lệnh SQL sang sự kiện Event – B 30 Bảng 3.4: Bảng EMPLOYEES và BONUS 31 Học viên: Nông Thị Oanh - K18HTTT -4- DANH MỤC HÌNH VẼ Hình 1.1: Ứng dụng cơ sở dữ liệu có sử dụng các trigger 9 Hình 1.2: Các thành phần của trigger 11 Hình 2.1: Mối quan hệ giữa Máy và Ngữ cảnh 20 Hình 2.2: Ví dụ một cấu trúc của Ngữ cảnh. 21 Hình 2.3: Ví dụ một cấu trúc của máy 23 Hình 2.4: Cấu trúc tổng quát của sự kiện 26 Hình 2.5: Sự phân rã và kết hợp 26 Hình 4.1: Kiến trúc của chƣơng trình hỗ trợ mô hình hóa hệ thống trigger 33 Hình 4.2: Sơ đồ phân cấp chức năng của hệ thống mô hình hóa trigger 34 Hình 4.3: Biểu đồ luồng dữ liệu mức ngữ cảnh 34 Hình 4.4: Luồng công việc chính của chƣơng trình 35 Hình 4.5: Giao diện chính của chƣơng trình hỗ trợ mô hình hóa hệ thống trigger bằng Event-B 36 Hình 4.6: Giao diện kết nối hệ thống cơ sơ dữ liệu 37 Hình 4.7: Giao diện tạo ràng buộc hệ thống 37 Hình 4.8: Giao diện tạo trigger 38 Hình 4.9: Giao diện thêm trigger vào danh sách thành công 39 Hình 4.10: Giao diện phân tích và chuyển đổi tự động 40 Hình 4.11: Giao diện chỉnh sửa mô hình Event-B 40 Hình 4.12: Giao diện xuất ra file XML 41 Học viên: Nông Thị Oanh - K18HTTT -5- DANH MỤC TỪ VIẾT TẮT Từ viết tắt Tiếng Anh Tiếng Việt DML Data Manipulation Language Ngôn ngữ thao tác dữ liệu DDL Data Definition Language Ngôn ngữ định nghĩa dữ liệu ECA Event - Condition - Action Sự kiện – Điều kiện – Hành động Học viên: Nông Thị Oanh - K18HTTT -6- MỞ ĐẦU Triggers là các luật hoạt động trong hệ thống cơ sở dữ liệu thƣơng mại nhƣ Orcacle, SyBase,…đƣợc hình thành trong cấu trúc Event - Condition Action (ECA). Triggers đƣợc sử dụng thƣờng xuyên và rộng rãi trong hệ thống cơ sở dữ liệu của nhiều ứng dụng để thực hiện các thao tác tự động và đảm bảo tính ràng buộc toàn vẹn. Trong một số cơ sở dữ liệu thƣơng mại, triggers có hai loại: triggers DML và triggers hệ thống. Triggers DML đƣợc kích hoạt khi các sự kiện DELETING, UPDATING, INSERTING xuất hiện, còn triggers hệ thống giống nhƣ thủ tục lƣu trữ có chứa các đoạn mã PL/SQL. Các đoạn mã này con ngƣời có thể đọc đƣợc và không có ngữ nghĩa hình thức. Vì vậy, chúng ta chỉ có thể kiểm chứng nếu trigger kết thúc hoặc xung đột với tính ràng buộc toàn vẹn sau khi thi hành nó hoặc kiểm tra từng bƣớc một. Do đó mô hình hoá triggers bằng các phƣơng pháp hình thức là hết sức cần thiết. Một số công trình đã cố gắng giải quyết vấn đề này bằng cách áp dụng các giải thuật tìm kiếm tính dừng hoặc kiểm chứng mô hình [4], [5]. Tuy nhiên, hầu hết các kết quả đều tập trung vào tính chất dừng, trong khi một số ít giải quyết cả hai tính dừng và ràng buộc toàn vẹn của hệ thống cơ sở dữ liệu. Hơn nữa, các phƣơng pháp tiếp cận dƣờng nhƣ rất phức tạp mà chúng ta không thể áp dụng vào trong phát triển cơ sở dữ liệu. Phƣơng pháp B [6] là phƣơng pháp phát triển phần mềm hình thức, ban đầu đƣợc J.-R. Abrial viết. Ký hiệu của phƣơng pháp B dựa trên lý thuyết tập hợp, phép thay thế tổng quát và logic bậc nhất. Event – B [7] đƣợc kế thừa từ phƣơng pháp B, phù hợp hơn cho phát triển hệ thống phân tán và phản hồi lớn. Phát triển phần mềm trong Event – B bắt đầu bằng mô tả các yêu cầu của hệ thống ở mức trừu tƣợng và sau đó làm mịn chúng qua các bƣớc để đạt đƣợc sự mô tả hệ thống chi tiết của hệ thống để có thể chuyển đổi sang mã nguồn. Tính nhất quán của mỗi mô hình và mối quan hệ giữa mô hình trừu tƣợng và mô hình làm mịn thu đƣợc bằng chứng minh hình thức. Các công cụ hỗ trợ đƣợc cung cấp cho đặc tả Event – B và chứng minh trong nền tảng Rodin. Từ yêu cầu kiểm chứng các triggers và ƣu điểm của Event-B, việc phát triển các công cụ phần mềm hỗ trợ quá trình mô hình hoá bằng Event-B có ý nghĩa thực tiễn quan trọng trong qui trình phát triển các ứng dụng cơ sở dữ liệu. Học viên: Nông Thị Oanh - K18HTTT -7- Trên cơ sở những phân tích trên, đƣợc sự định hƣớng và chỉ bảo của PGS.TS Trƣơng Ninh Thuận, tôi đã lựa chọn đề tài: “Nghiên cứu và xây dựng công cụ hỗ trợ mô hình hóa hệ thống triggers bằng Event-B” làm luận văn tốt nghiệp của mình. Trong luận văn này, chúng tôi dựa vào một cách tiếp cận hình thức hóa hệ thống trigger cơ sở dữ liệu bằng phƣơng pháp chứng minh Event – B [5]. Ý tƣởng tiếp cận này đƣợc xuất phát từ sự tƣơng quan giữa cấu trúc của sự kiện Event – B và ECA. Đầu tiên, chúng tôi chuyển đổi hệ thống cơ sở dữ liệu sang mô hình Event – B. Bƣớc tiếp theo chúng tôi đƣa mô hình tiếp cận thực tế bằng cách sử dụng nền tảng Rodin để kiểm chứng thuộc tính là tính dừng và các ràng buộc khác dựa trên công cụ chứng minh tự động. Ƣu điểm của cách tiếp cận này là hệ thống cơ sở dữ liệu thực bao gồm các trigger và các ràng buộc đƣợc mô hình hóa dễ dàng bằng cụm từ diễn tả logic trong Event – B nhƣ INVARIANTS và EVENTS. Do đó, tính đúng đắn của hệ thống có thể đƣợc chứng minh bằng phƣơng pháp hình thức. Điều đó đặc biệt quan trọng cho các nhà phát triển cơ sở dữ liệu khi mà biết chắc chắn hệ thống trigger tránh đƣợc các vấn đề nghiêm trọng ở thời gian thiết kế. Hơn nữa, cách tiếp cận gần với thực tế mà chúng tôi có thể triển khai một công cụ theo ý tƣởng chính để chuyển đổi mô hình cơ sở dữ liệu từ Event – B sang nền tảng Rodin tự động (hoặc tự động một phần). Luận văn gồm một số nội dung chính nhƣ sau: Chƣơng 1: Tổng quan về Trigger trong cơ sở dữ liệu - nội dung đƣợc trình bày trong chƣơng bao gồm: khái niệm, cách tạo trigger, các thành phần của trigger, phân loại trigger. Chƣơng 2: Ngôn ngữ Event-B - trình bày về cấu trúc của mô hình EventB gồm Máy, Ngữ cảnh, sự kiện của Event-B. Chƣơng 3: Mô hình hóa và kiểm chứng hệ thống trigger bằng Event-B – trình bày về các định nghĩa đƣợc ánh xạ sang các khái niệm của Event-B, các luật chuyển đổi giữa hệ thống trigger sang mô hình Event-B; đƣa ra cách tiếp cận chi tiết, mô hình hóa hệ thống trigger cụ thể trong ví dụ 3.4 và giới thiệu những thông tin và các nghiên cứu liên quan đến công việc cho đến nay. Chƣơng 4: Xây dựng công cụ hỗ trợ mô hình hóa hệ thống trigger bằng Event-B – trình bày về chức năng, giao diện và hƣớng dẫn sử dụng chƣơng trình. Học viên: Nông Thị Oanh - K18HTTT -8- CHƢƠNG 1: TỔNG QUAN VỀ TRIGGER TRONG CƠ SỞ DỮ LIỆU 1.1. Khái niệm Trigger cơ sở dữ liệu là một đoạn mã tự động kích hoạt khi xảy ra một sự kiện đƣợc định nghĩa trong cơ sở dữ liệu. Sự kiện có liên quan đến một thao tác dữ liệu cụ thể của cơ sở dữ liệu nhƣ chèn, xóa hoặc cập nhật một hàng của bảng. Trigger thƣờng đƣợc sử dụng trong một số trƣờng hợp: kiểm tra tiến trình, thực hiện tự động một hành động, thực hiện các luật nghiệp vụ phức tạp. Cấu trúc của trigger giống nhƣ cấu trúc của ECA, vì thế nó có mẫu sau: rule name:: Event(e) IF condition DO action. Điều đó có nghĩa là khi có sự kiện xảy ra và thỏa mãn điều kiện cho trƣớc thì hệ thống cơ sở dữ liệu thực hiện hành động. Ngƣời sử dụng hệ thống cơ sở dữ liệu quan hệ nhƣ Oracle, MySQL, SyBase quen với triggers biểu diễn dƣới dạng SQL:1999 (dạng chuẩn trƣớc là SQL-3). Trigger cơ sở dữ liệu đƣợc phân thành hai loại chính: trigger DML và trigger DDL. Trigger DML đƣợc thi hành khi dữ liệu đƣợc thao tác, còn trigger DDL đƣợc kích hoạt trong sự kiện DDL nhƣ tạo bảng hoặc các sự kiện nhƣ đăng nhập, xác nhận, hủy… Một trigger thƣờng đƣợc tạo trên một bảng nào đó nhƣng nó cũng có thể truy cập vào dữ liệu của bảng khác. Triggers đƣợc sử dụng thƣờng xuyên và rộng rãi trong hệ thống cơ sở dữ liệu của nhiều ứng dụng để thực hiện các thao tác tự động và đảm bảo tính ràng buộc toàn vẹn. Trigger đƣợc lƣu trữ trong cơ sở dữ liệu gồm các khối câu lệnh SQL và PL hoặc câu lệnh Java để chạy và có thể gọi thủ tục lƣu trữ. Tuy nhiên, thủ tục và trigger có cách gọi khác nhau. Trong khi thủ tục đƣợc thi hành trực tiếp bởi ngƣời dùng, ứng dụng thì một hay nhiều trigger đƣợc kích hoạt ngầm bởi Oracle khi có câu lệnh trigger INSERT, DELETE hoặc UPDATE đƣợc thực hiện mà không gây ra vấn đề cho ngƣời dùng đang kết nối hoặc ứng dụng đang chạy. Hình 1.1 minh họa một ứng dụng cơ sở dữ liệu với một số câu lệnh SQL kích hoạt các trigger lƣu trữ trong cơ sở dữ liệu [8]. Học viên: Nông Thị Oanh - K18HTTT -9- Database Applications Table t UPDATE t SET…; Update Trigger BEGIN ….. INSERT INTO t…; Insert Trigger BEGIN ….. DELETE FROM t…; Delete Trigger BEGIN ….. Hình 1.1: Ứng dụng cơ sở dữ liệu có sử dụng các trigger. Các sự kiện kích hoạt trigger bao gồm:  Các câu lệnh DML thay đổi dữ liệu trong bảng (insert, delete hoặc update)  Các câu lệnh DDL.  Các sự kiện hệ thống nhƣ bắt đầu, kết thúc hoặc thông báo lỗi.  Các sự kiện ngƣời dùng nhƣ logon, logoff 1.2. Tạo trigger Ta có thể tạo trigger thông qua lệnh script.  Cú pháp lệnh tạo trigger mức câu lệnh: CREATE [OR REPLACE] TRIGGER trigger_name timing event1 [OR event2 OR event3] ON table_name BEGIN PL/SQL Block; END;  Cú pháp lệnh tạo trigger mức dòng dữ liệu: Học viên: Nông Thị Oanh - K18HTTT -10- CREATE [OR REPLACE] TRIGGER trigger_name timing event1 [OR event2 OR event3] ON table_name [REFERENCING OLD AS old | NEW AS new] FOR EACH ROW [WHEN condition] BEGIN PL/SQL Block; END; Với: Trigger_name timing Tên trigger Thời gian kích hoạt trigger event Loại câu lệnh kích hoạt trigger referencing FOR EACH ROW WHEN Table_name PL/SQL Block Tên biến thay thế cho giá trị trước và sau thay đổi của dòng dữ liệu đang xử lý Trigger thuộc loại tác động trên dòng dữ liệu Chỉ ra một số điều kiện ràng buộc thực hiện trigger Tên bảng dữ liệu có gắn trigger trên đó Nội dung khối lệnh SQL và PL/SQL trong trigger Ví dụ: CREATE OR REPLACE TRIGER secure_emp BEFORE INSERT ON emp BEGIN IF TO_CHAR(sysdate,‟DY‟) IN („SAT‟,‟SUN‟) OR TO_CHAR(sysdate,‟HH24‟) NOT BETWEEN „08‟ AND ‟18‟ THEN RAISE_APPLICATION_ERROR (-20500, ‟Thời gian làm việc không phù hợp‟); END IF; END; CREATE OR REPLACE TRIGER audit_emp_values AFTER DELETE OR INSERT OR DELETE ON emp FOR EACH ROW BEGIN Học viên: Nông Thị Oanh - K18HTTT -11- INSERT INTO audit_emp_values (user_name, timestamp, id, old_last_name, new_last_name, old_title, new_tile, old_salary, new_salary) VALUES (USER, SYSDATE, :old.empno, :old.ename, :new.ename, :old.job, :new.job, :old.sal, :new.sal); END; [8] 1.3. Các thành phần của trigger Một trigger có ba thành phần chính:  Sự kiện hoặc câu lệnh trigger  Điều kiện trigger  Hành động trigger [8] AFTER UPDATE OF past_on_hand ON inventory Câu lệnh trigger WHEN (new. past_on_hand - Xem thêm -