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. 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com -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 Event- B 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com -8- CHƢƠNG 1: TỔNG QUAN VỀ TRIGGER TRONG CƠ SỞ DỮ LIỆU 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.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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com -9- Database Applications Table t Update Trigger UPDATE t SET…; BEGIN ….
Insert Trigger INSERT INTO t…; BEGIN …. DELETE FROM t…; Delete Trigger BEGIN ….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. 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com -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 Tên trigger timing Thời gian kích hoạt trigger event Loại câu lệnh kích hoạt trigger Tên biến thay thế cho giá trị trước và sau referencing 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ữ FOR EACH ROW liệu Chỉ ra một số điều kiện ràng buộc thực hiện WHEN trigger Table_name Tên bảng dữ liệu có gắn trigger trên đó PL/SQL Block 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com -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. 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] Hành động AFTER UPDATE OF past_on_hand ON inventory Câu lệnh trigger trigger WHEN (new.
past_on_hand<new.record_point) Điều kiện trigger FOR EACH NOW DECLARE /*a dumy variable for counting*/ NUMBER X; BEGIN SELECT COUNT(*) INTO X /*query to find out if part has already been*/ FROM pending_orders /*reodered-if yes,x=1, if no, x-0*/ WHERE past_no=:new,part_no; IF x=0 THEN /*past has not been reodered yet, so reorder*/ INSERT INTO pending_orders VALUE (new1past_no, new,reorder_quantity, sysdate) END IF /*past has already been reodered*/ END.2: Các thành phần của trigger 1. Sự kiện hoặc câu lệnh trigger Sự kiện hoặc câu lệnh trigger là câu lệnh SQL, sự kiện cơ sở dữ liệu hoặc sự kiện ngƣời dùng kích hoạt trigger. Sự kiện trigger có thể là câu lệnh insert, Học viên: Nông Thị Oanh - K18HTTT LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com -12- delete hoặc update trong bảng. Một sự kiện trigger có thể có một hoặc nhiều sự kiện sau: Câu lệnh insert, delete hoặc update trên một bảng cụ thể (trong một số trƣờng hợp là view) Câu lệnh create, alter hoặc drop trên đối tƣợng lƣợc đồ bất kì.