ĐẠ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 -