Luận án tiến sĩ toán học đặc tả kiểm chứng hình thức và ứng dụng trong cơ sở dữ

MỤC LỤC LỜI CAM ĐOAN. 3 DANH MỤC CÁC TỪ VIET TÁT. 6 DANH SÁCH BẢNG. 7 DANH SÁCH HINH.

9 1 CO SỞ DU LIEU THỜI GIAN THỰC 16 l1 Coséditliéu .2 Điều khiển tương tranh trong CSDL. Các đặc điểm dữ liệu va giao tác của CSDL thời gian thực 19 1.4 Điều khiển tương tranh thời gian thực .1 Giao thức RWPCP. 25 142 Giao thức BAP. Giao thức PCP-DA.

32 2 LOGIC TÍNH TOÁN KHOANG 33 2. 33 Sis) TT HHDHHẨT: wa ci ie ieee 6 Ad KHER Eee vu 33 2.3 - - -- Hệ thống chứng minh .2 Logic tính toán khoảng.: ¿⁄ ¡(s2 v1 án vn kh 38 222 Ngữ nghĩa.3 - Hệ thống chứng minh. 40 924 Định lý của DE ccc ‹¿ ¡vỉ c2 sẽ kề c 4I 23 Kếtluận ee Q2. 42 MÔ HÌNH HÌNH THỨC CỦA HỆ THỐNG CƠ SỞ DỮ LIỆU THỜI GIAN THỤC TRONG LOGIC TÍNH TOÁN KHOẢNG 44 3.

Mô hình cđơsở.2 Mô hình tiến hành .1 Mô hình đơn bộ xử lý.2 Mô hình đa bộ xử lý. Các điều kiện đúng cho thực hiện song song của hệ thống PIATRA .« em HTSE BAO 52 3.2 Điều kiện nhất quán thời gian. Một số điều kiện đủ cho việc duy tri tính nhất Quan THÔI gÌHH psec cv ý ieee eRe ww c c 58 34 Kétluan. 63 ĐẶC TẢ, KIỂM CHỨNG HÌNH THỨC GIAO THỨC DIEU KHIỂN TƯƠNG TRANH VÀ UNG DỤNG TRONG CƠ SỞ DU LIEU THỜI GIAN THỰC 64 S41 THỊNH [HỮU HH hie.

sees eect eae eee wee ewe 65 4.2 Hinh thức hoa R/WPCP .3 Kiểm chứng hình thức giao thức R/WPCP. 7I 4131 Nhà tein ti occ cee swe ieee lớn 2ì na ee 7I 4.2 Nghẽn nhiều nhất một lan của R/WPCP .3 R/WPCP là không bế tắc.4 Chứng minh định lý về điều kiện lập lịch của R/WPCP trong CSDL thời gian thuc.4 Nghẽn cua R/WPCP trong môi trường da bộ xử lý .5 Ung dụng hệ thống cơ sở dữ liệu thời gian thực trong hệ thống điều khiển giao thông hàng không.1 Mô hình hệ thống.2 M6 hình dữ liệu và các giao tác. 82 455 NWS QUAN DI BÙN - + ‹ cet wes ww wees 84 4.4 Lịch giao tác và điều khiển tương tranh. «vs k (vn 225029 5n S6 K6 ee 87 KET QUA NGHIÊN CỨU VA BANLUAN.

000000 cece cence ees 90 HƯỚNG PHÁT TRIEN. 92 CÁC CÔNG TRÌNH ĐÃ CÔNG BỐ. 94 TÀI LIEU THAM KHẢO. 103 DANH MỤC CÁC TỪ VIET TAT Số Viết tắt Diễn giải tiếng Anh Diễn giải tiếng Việt 1 ALE | Alert Detection Transac-| Giao tác phát hiện lỗi tion | 2 BAP | Basic Aborting Protocol - Giao thức huỷ bỏ cơ sở ˆ 3 CSDL | Database Co sở dữ liệu | 4) DC | Duration Calculus [Logic tính toán khoảng _ 5 DDB || Display Database | Cơ sở dữ liệu hiện thị 6 — DM.

Data Manager Bộ quan trị dữ liệu 7 DOS Data Operator System Hệ thống thao tác dữ liệu is | DT| Display Transaction | Giao tac hién thi 9 IL Interval Logic Logic khoảng _ 10 | PCP-DA | Priority Ceiling Protocol Giao thức mức ưu tiên | with Dynamic Adjust- cao nhất với điều chỉnh ment of Serialization Or- | động của thứ tu khả tuần. der | tự NPL | Predicate Logic [Logic vi tr | 12 RM_ Rate Monotonic. Thuật toán lập lịch xác | định mức ưu tiên theo chu kỳ R/WPCP | Read/Write Priority Ceil- iEGiao thức đọc/ghi- mức -1ng Protocol ưu tiên cao nhất | : 1 14 | ST Sensor Transaction | Giao tác cam nhận 15 | TDB Target Database Co sở dữ liệu đích 14 | TM | Transaction Manager | Bộ quản tri giao tác fee | _ Two Phase Locking Khoa hai pha DANH SÁCH BANG 1.1 Các yêu cầu đặc trưng của CSDL thời gian thực DANH SÁCH HÌNH Lol Mô hình CSDL thời gian thực. 19 12 Các ham giá trị của các kiểu giao tác thời gian thực .3 Nhất quán thời gian của dữ liệu.4 Thực hiện của các giao tác dưới R/WPCP.

26 LS Thực hiện của các giao tác dưới BAP.6 Thực hiện của các giao tác dưới PCP-DA .4 Đồ thị thể hiện các biến trạng thái. 47 ae D0 YLHiiiB TH IGG gee eee eee ee ee 57 33 Thực hiện cập nhật của giao tac cảm nhận .4 Duy ti TẤT QUẦN : ¡ ¿ vẽ cee wes ewes HES ee HH 61 4.1 Lich cua R/WPCP trong môi trường đa bộ xrly.2 Mô hình hệ thống CSDL thời gian thực trong điều khiển giao thông hang KHÔNH ¿ : ¿ keke eee RH SLED ER EME RE SS 82 4.3 Thực hiện của các giao tác.4 Lịch của R/WPCP trong hệ thống điều khiển giao thông hàng KHÔI cewek ws KỈ BS eo VY No HH HN 2 86 MỞ ĐẦU Hệ thống cơ sở dữ liệu thời gian thực đã được sử dụng rộng trong các ứng dụng như hàng không vũ trụ, hệ thống điều khiển giao thông hàng không, người máy, năng lượng hạt nhân, hệ thống tích hợp máy, hệ thống chương trình chứng khoán, và hệ thống quản trị mạng. Do đó nghiên cứu cơ sở dữ liệu (CSDL) thời gian thực đã được nhiều người tập trung nghiên cứu và triển khai ứng dụng [13, 14, 31, 34, 44]. Hệ thống cơ sở dữ liệu thời gian thực bao gồm hai lĩnh vực quan trọng trong khoa học máy tính, đó là: hệ thống thời gian thực và hệ thống CSDL.

Một mặt các giao tác trong CSDL thời gian thực thường kết hợp với các ràng buộc thời gian đó là điểm tới hạn. Mặt khác, như là một CSDL, CSDL thời gian thực phải duy trì dữ liệu của nó cho các thông tin hữu ích, cung cấp các thao tác của dữ liệu va xử lý các giao tác [34]. Hiện nay, hệ thống CSDL thời gian thực là một trong những lĩnh vực đang được quan tâm nghiên cứu và phát triển. Sự phát triển này hứa hẹn một triển vọng ứng dụng to lớn trong các hoạt động kinh tế, khoa học kỹ thuật, an ninh và quốc phòng.

Tuy nhiên để khai thác CSDL thời gian thực va phát triển các ứng dụng, trong thực tế thì vẫn còn nhiều vấn đề cần phải tiếp tục nghiên cứu. Ở nước ta, CSDL thời gian thực vẫn còn là một lĩnh vực mới mẻ cả trong nghiên cứu và triển khai ứng dụng. Hơn nữa, nước ta đang trong thời kỳ phát triển của nền kinh tế nhiều thành phần và đa dạng, nên vai trò của các hệ thống thông tin, đặc biệt là các hệ CSDL thời gian thực lại càng chiếm một vị trí quan trọng. Do vậy đầu tư cho nghiên cứu và triển khai ứng dụng hệ thống CSDL thời gian thực là một việc làm cần thiết.

Mô hình dữ liệu và CSDL truyền thống không đáp ứng đây đủ cho các ứng dụng thời gian thực. Bởi vì, nó không được thiết kế để cung cấp cho yêu cầu ứng dụng giao dịch thời gian thực. Do đó, trong hệ thống CSDL thời gian thực chúng ta phải xử lý một số yêu cầu về thời gian, khác với điều kiện thông thường. Để phát triển hệ thống thời gian thực, đặc biệt là hệ CSDL thời gian thực, trong đó các thuật toán lập lịch và điều khiển tương tranh là một vấn đề chính trong nghiên cứu hệ thống CSDL thời gian thực.

Trong một thập kỷ qua, một số giao thức điều khiển tương tranh thời gian thực đã được đề xuất [32. 33, 34, 42] để giải quyết xung đột dữ liệu giữa các giao tác. Các giao thức này phải đảm bảo không chỉ duy trì tính nhất quán của dữ liệu trong môi trường nhiều người sử dụng như trong cơ sở dữ liệu truyền thống mà còn duy trì tính nhất quán thời gian của dữ liệu và tất cả các giao tác phải hoàn thành thực hiện trước điểm hạn của chúng. Do đó, điều khiển tương tranh trong CSDL thời gian thực phức tạp hơn điều khiển tương tranh trong CSDL truyền thống.

Cùng với sự phát triển của máy tính, hệ thống thời gian thực (hệ CSDL thời gian thực) đã có những sự thay đổi rất lớn. Sự phát triển này làm tăng sự phức tạp của hệ thống máy tính, tạo ra sự cần thiết phải cải tiến các kỹ thuật đặc tả và kiểm chứng hình thức. Các phương pháp hình thức liên quan tới nhiều kỹ thuật và mô hình toán học và có thể được áp dụng cho thiết kế hệ thống thời gian thực, ví dụ [23, 26, 28, 37, 46]. Trong đó, việc sử dụng các logic hình thức trong đặc tả, thiết kế, kiểm chứng và xây dựng hệ thống thời gian thực ngày càng được quan tâm.

Mục đích chính của việc sử dụng phương pháp hình thức là chìa khoá giải quyết việc xây dựng điều kiện đúng, để đặc tả chính xác bài toán đặt ra và có thể kiểm chứng được bằng toán học nhờ sự trợ giúp của các công cụ. Một trong những phương pháp hình thức đang tồn tai, được áp dung trong việc đặc tả hình thức cho hệ thống thời gian thực là logic thời gian thực [37]. Các phương pháp đặc tả hình thức có thể được thiết kế để phân tích và kiểm chứng chất lượng thuộc tính thời gian nhằm giảm thiểu số lỗi và tăng khả năng thực thi của hệ thống. Tuy nhiên, với các yêu cầu thời gian thực, chất lượng đặc tả và phân tích thì không đây đủ, ví dụ như phương pháp sử dụng logic thời gian chỉ đặc tả được thứ tự thời gian, chứ không đặc tả được các ràng buộc thời gian và tính chất của dữ liệu.

Hiện nay các nhà nghiên cứu đã và đang cố gắng nghiên cứu mở rộng các phương pháp đặc tả hình thức đang tồn tại cho phép thể hiện thuộc tính thời gian như: Real Time Logic [8], Time CSP [40], Metric Temporal Logic [30], Timed Transition 10 System [22], Timed Automata [9],. Trong số đó, Logic tính toán khoảng (Duration Calculus) (DC) [15] là một hệ thống hình thức cho đặc tả và thiết kế hệ thống thời gian thực đặc biệt an toàn. DC bat đầu được phát triển trong các dự án ProCoS (ESPRIT BRA 3104 và 7071) năm 1990 và được đề xuất bởi Zhou Chaochen, CA. Sau đó DC được tập trung nghiên cứu và phát triển mở rộng bởi các nhà nghiên cứu trong dự án Design Technique for Real- Time Systems của Viện công nghệ phần mềm Quốc tế (UNU/IIST) từ năm 1993.

DC là một logic đơn giản, phù hợp để biểu diễn và xử lý khoảng thời gian, một khái niệm chính trong lập lịch, và DC đã sử dụng hiệu quả trong nhiều công trình nghiên cứu về các hệ thống thời gian thực, ví dụ [16, 20, 29, 38, 39, 47]. Việc áp dụng các phương pháp hình thức trong các lĩnh vực nghiên cứu CSDL nói chung và CSDL thời gian thực nói riêng là một lính vực nghiên cứu mới, và còn nhiều vấn đề cần được phát triển.