ĐẠ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
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
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
-2- Học viên: Nông Thị Oanh - K18HTTT
Chƣơng 3: MÔ HÌNH HÓA VÀ KIỂM CHỨNG HỆ THỐNG TRIGGER
BẰNG EVENT – B 27
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
-4- Học viên: Nông Thị Oanh - K18HTTT
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
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
-6- Học viên: Nông Thị Oanh - K18HTTT 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
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
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].
-9- Học viên: Nông Thị Oanh - K18HTTT
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.
Học viên: Nông Thị Oanh - K18HTTT
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:
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
Trigger_name
Tên trigger
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
WHEN (new. past_on_hand<new.record_point)
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.
Hình 1.2: Các thành phần của trigger
1.3.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,
Câu lệnh trigger
Điều kiện trigger
Hành
động
trigger
-12-
Nếu phần điều kiện có giá trị true, những hành động của trigger đƣợc thực hiện.
1.3.3. Hành động trigger
Hành động trigger là thủ tục (đoạn PL/SQL, chƣơng trình Java, hàm C)
chứa các mã và câu lệnh SQL để chạy khi các sự kiện sau xuất hiện:
-13- Học viên: Nông Thị Oanh - K18HTTT
Câu lệnh trigger đƣợc sử dụng.
Giá trị điều kiện trigger là True.
Giống nhƣ thủ tục lƣu trữ, hành động trigger gồm:
Chứa các câu lệnh SQL, PL/SQL hoặc Java.
Định nghĩa các cấu trúc ngôn ngữ PL/SQL nhƣ các biến, các hằng,
con trỏ, các trƣờng hợp ngoại lệ khác.
Định nghĩa cấu trúc ngôn ngữ Java.
Gọi các thủ tục lƣu trữ.
Nếu các trigger là các trigger dòng, câu lệnh trong hành động trigger có
thể truy cập đến giá trị của dòng đang đƣợc xử lý bởi trigger.
Một hành động có thể kiểm tra kết quả của truy vấn trong một phần điều
kiện của trigger, tham chiếu tới các giá trị cũ và mới của những bộ giá trị thay
đổi sau khi thực hiện trigger, thực hiện các truy vấn mới và làm những thay đổi
đối với cơ sở dữ liệu. Thực tế, một action có thể thực hiện một chuỗi các câu
lệnh định nghĩa dữ liệu (ví dụ, tạo bảng mới, thay đổi quyền của ngƣời dùng) và
các lệnh hƣớng - giao dịch (ví dụ, commit), hoặc gọi các thủ tục khác.
Một ví dụ chỉ ra trong hình 1.3, cú pháp viết trên Oracle 7 để định nghĩa
các triggers, (Cú pháp của SQL:1999 cho những trigger này tƣơng tự nhƣ trong
Oracle; chúng ta sẽ xem một ví dụ sử dụng cú pháp ngắn gọn của SQL:1999).
Một trigger sử dụng init_count để khởi động một biến đếm trƣớc khi thực hiện
câu lệnh INSERT để thêm một bộ giá trị vào quan hệ Students. Trigger dùng
Mặt khác, trigger init_count đƣợc thực hiện một lần với mỗi câu lệnh INSERT,
không quan tâm đến số lƣợng các bản ghi đƣợc thêm vào, bởi vì chúng không có
mệnh đề FOR EACH ROW. Trigger nhƣ thế này đƣợc gọi là statement-level
trigger.
Trong hình 1.3, từ khoá new tham chiếu tới một bộ giá trị mới đƣợc thêm
vào. Nếu bộ giá trị đang tồn tại đƣợc sửa, từ khoá old và new có thể đƣợc sử
dụng để tham chiếu tới các giá trị trƣớc và sau khi có sự thay đổi. Bản
SQL:1999 phác thảo cũng cho phép hành động của trigger tham chiếu đến một
tập các bản ghi đã thay đổi, không chỉ là thay đổi của một bản ghi. Ví dụ, thật
hữu ích nếu có thể tham chiếu tới một tập các bản ghi mới thêm vào quan hệ
Students, những bản ghi đƣợc thêm chỉ bằng một câu lệnh INSERT; chúng ta có
thể đếm đƣợc số bản ghi mới có age<18 thông qua việc sử dụng truy vấn trên
tập này.
Định nghĩa trong hình 1.3 sử dụng cú pháp của SQL:1999, để minh hoạ
sự tƣơng đồng và sự khác nhau về cú pháp đƣợc sử dụng trong DBMS. Từ khoá
NEW TABLE có thể đƣợc chúng ta sử dụng để cung cấp một tên mới cho tập
-15- Học viên: Nông Thị Oanh - K18HTTT
các bộ giá trị mới đƣợc thêm. Mệnh đề FOR EACH STATEMENT chỉ ra trigger
này là statement-level trigger và có thể bỏ qua vì nó là mệnh đề mặc định. Định
nghĩa này không có mệnh đề WHEN; nếu có mệnh đề này, nó sẽ có mệnh đề
FOR EACH STATEMENT theo sau-mệnh đề viết trƣớc khi xác định các hành
động.
Mỗi trigger đƣợc thực hiện một lần với mỗi câu lệnh SQL thêm các bộ
giá trị vào bảng Students, và việc thêm từng bộ giá trị duy nhất vào bảng đƣợc
thống kê lại. Hai trƣờng đầu tiên của bộ giá trị chứa các hằng số (chỉ ra bảng
đƣợc thay đổi là Students và loại thay đổi là Insert), và trƣờng thứ ba là số lƣợng
Trigger mức dòng lệnh: Trigger đƣợc kích nhiều lần ứng với mỗi dòng
dữ liệu chịu ảnh hƣởng bởi thao tác thực hiện lệnh.
1.5. Quản lý trigger
1.5.1. Phân biệt trigger cơ sở dữ liệu
Trigger và thủ tục:
Trigger
Thủ tục
Lệnh tạo: CREATE TRIGGER
Lệnh tạo: CREATE PROCEDURE
Lƣu giữ trong Từ điển dữ liệu dƣới
dạng mã nguồn và dạng p-code
Lƣu giữ trong Từ điển dữ liệu dƣới
dạng mã nguồn và dạng p-code
Đƣợc gọi ngầm định
Thực hiện theo lời gọi tƣờng minh
Không cho phép dùng: COMMIT,
ROLLBACK, SAVEPOINT
Cho phép dùng: COMMIT,
ROLLBACK, SAVEPOINT
Trigger cơ sở dữ liệu và trigger giao diện:
Trigger cơ sở dữ liệu
Trigger giao diện
Đƣợc thực hiện khi có tác động lên
database do ứng dụng hoặc do chính
các công cụ của Oracle
Đƣợc thực hiện chỉ bởi các tác động
ngay trên ứng dụng
Đƣợc kích hoạt bởi các lệnh SQL
Đƣợc kích bởi các sự kiện trên ứng
ALTER TRIGGER trigger_name COMPILE;
Ví dụ:
Biên dịch lại trigger check_sal sau khi sửa đổi nội dung
ALTER TRIGGER check_sal COMPILE;
1.5.3. Hủy bỏ trigger
Sử dụng câu lệnh SQL để huỷ bỏ trigger.
Cú pháp:
DROP TRIGGER trigger_name;
-18- Học viên: Nông Thị Oanh - K18HTTT
Ví dụ: DROP TRIGGER check_sal;
1.6. Khác nhau giữa các ràng buộc và triggers
Mục đích của trigger là đảm bảo sự nhất quán của cơ sở dữ liệu, và với
mục đích này, chúng ta nên xem xét đến việc sử dụng các ràng buộc tham chiếu
(ví dụ, ràng buộc khoá ngoại). Ràng buộc không tự động kích hoạt nhƣ trigger
nên các ràng buộc dễ để hiểu và cũng cung cấp cho hệ quản trị cơ sở dữ liệu
nhiều cơ hội để tối ƣu hoá việc thực hiện. Ràng buộc cũng tránh cho dữ liệu trở
nên thiếu nhất quán với bất kỳ loại câu lệnh nào, ngƣợc lại trigger chỉ kích hoạt
ứng với một loại câu lệnh xác định (ví dụ, câu lệnh Insert hoặc Delete). Một lần
nữa, ta thấy giới hạn này làm cho ràng buộc dễ hiểu hơn.
Mặt khác, trigger cho phép chúng ta thực hiện các ràng buộc cơ sở dữ liệu
bằng nhiều cách phức tạp, nhƣ những ví dụ minh sau đây:
Giả sử rằng chúng ta có một bảng Orders có các trƣờng itemid, quantity,
customerid, và unitprice. Khi một khách hàng đặt một hoá đơn, giá trị ba
trƣờng đầu tiên đƣợc điền vào bằng ngƣời dùng (ví dụ là ngƣời bán hàng).
Giá trị trƣờng thứ tƣ có thể đƣợc lấy từ một bảng có tên là Items, nhƣng
nó cần thiết phải có mặt trong bảng Orders để có đƣợc một bản ghi hoàn
Event-B không phải là ngôn ngữ lập trình. Event-B là một phƣơng pháp
hình thức để mô hình hoá và phân tích ở mức hệ thống. Nó đƣợc sử dụng nhƣ là
một ký hiệu và phƣơng pháp phát triển hình thức của hệ thống rời rạc. Event - B
đƣợc coi là sự kế thừa của ký hiệu phƣơng pháp hình thức nhƣ là phƣơng pháp
B (đƣợc biết đến nhƣ là B cổ điển), Z và Action Systems, bởi vì nó đơn giản
hóa ký hiệu máy B, dễ dàng để học và phù hợp hơn cho sự phát triển hệ thống
phân tán phản ứng và song song. Điểm chủ chốt của Event-B là sử dụng lý
thuyết về tập hợp nhƣ là các ký hiệu mô hình hoá, sử dụng cơ chế làm mịn để
biểu diễn hệ thống ở các mức trừu tƣợng khác nhau và sử dụng các chứng minh
toán học để kiểm chứng hệ thống. Một ƣu điểm khác của Event-B là hỗ trợ công
cụ cho mô hình hóa hệ thống. Event -B đƣợc sử dụng cùng với nền tảng Rodin.
2.1. Máy và Ngữ cảnh
Các mô hình Event-B đƣợc mô tả bởi hai cấu trúc cơ bản là Máy
(Machine) và Ngữ cảnh (Context ). Trong đó, Máy dùng để mô tả phần động của
mô hình bao gồm biến, bất biến, định lý và các sự kiện tƣơng tác với môi
trƣờng. Ngữ cảnh mô tả phần tĩnh của mô hình, chứa các tập hợp (set), hằng,
tiên đề và định lý.
Máy và Ngữ cảnh có mối quan hệ khác nhau: Máy có thể đƣợc “làm mịn”
bởi máy khác và Ngữ cảnh đƣợc “mở rộng” bởi ngữ cảnh khác (không có chu
trình nào đƣợc phép trong cả hai quan hệ này). Hơn nữa, một Máy có thể “tham
chiếu” đến một hoặc nhiều Ngữ cảnh. Máy có thể “tham chiếu” ngầm định đến
tất cả các Ngữ cảnh mở rộng bởi Ngữ cảnh đã đƣợc “tham chiếu”. Một máy chỉ
có thể “tham chiếu ” đến Ngữ cảnh tƣờng minh hoặc ngầm định. Ví dụ về quan
-21- Học viên: Nông Thị Oanh - K18HTTT
hệ giữa Máy và Ngữ cảnh:
- Bất biến: biểu diễn thuộc tính của biến. Bất biến đƣợc định nghĩa trong
điều kiện của tập và hằng.
- Sự kiện: Một sự kiện có thể gán giá trị mới cho biến. Bảo vệ sự kiện cụ
thể dƣới điều kiện có thể xảy ra. Khi khởi tạo máy là trƣờng hợp đặc biệt của sự
kiện.
-23- Học viên: Nông Thị Oanh - K18HTTT Hình 2.3. Ví dụ một cấu trúc của máy
2.2. Sự kiện
Mô hình hệ thống với Event-B đƣợc bắt đầu từ các sự kiện trừu tƣợng
quan sát đƣợc có thể xảy ra trong hệ thống, từ đó đặc tả các trạng thái và hành vi
của hệ thống ở mức trừu tƣợng cao hơn. Một sự kiện e tác động lên (một danh
sách) biến trạng thái v, với điều kiện G(v) và hành động A(v), sẽ đƣợc mô tả nhƣ
sau :
Vì thế¸ khi trạng thái v thỏa mãn điều kiện G(v) = true, hành động A(v) sẽ
đƣợc thực hiện. Hình 2.3 biểu diễn cấu trúc tổng quát của một sự kiện. Trong đó:
1. Mệnh đề status có thể là ordinary, convergent (sự kiện phải làm tăng
giá trị các biến của nó ), anticipated (sự kiện không đƣợc làm tăng giá trị các
biến của nó ).
Copyright: Tài liệu đại học ©