Đặc tả kiểm chứng hình thức và ứng dụng trong cơ sở dữ liệu thời gian thực luận

MỤC LỤC LỜI CAM ĐOAN. 3 DANH MỤC CÁC TỪ VIẾT TẮT. 6 DANH SÁCH BẢNG. 7 DANH SÁCH HÌNH.

9 1 CO SO DU LIEU THOI GIAN THỰC 16 tl Cos ditliéw sa: : so: cuc sao vua c 0n 6 Số 26 16 1.2 Điều khiển tương tranh trong CSDL. Các đặc điểm dữ liệu và 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.2 Giao thức BAP. Giao thức PCP-DA. 32 2 LOGIC TINH TOAN KHOANG 33 2.3 Hệ thống chứng mỉnh .- - - - 37 22 Logic tính toán khoảng.-::sz: sẽ cu 9 số có nh 38 2.3 Hệ thống chứng mỉnh.

- 40 22:4 Đỉnh lý của DC :‹: : 2ö: : sẽ c: 6 v5 s? 4I 93 Nếtluận.: c2: ï 0n 96065 He 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.1 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 0gia0'tÁC. + =<-^ wes o Hid BMGT GS SE Ral § 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 trì tính nhất quán thời gian.ẶẶẶ Ốc 63 DAC TA, KIEM CHUNG HINH THUC GIAO THỨC ĐIỀU KHIỂN TƯƠNG TRANH VÀ ỨNG DỤNG TRONG CO SO DU LIEU THOI GIAN THUC 64 4.1 Hình thức hoá2PL.2 Hình thức hoá RWPCP.

Kiểm chứng hình thức giao thức R/WPCP.1 Khả tuân tự .2 Nghẽn nhiều nhất một lần 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 thoi gian thuc.4 Nghén cua R/WPCP trong môi trường đa bộ xử lý 4.5 Ung dụng hệ thống cơ sở dữ liệu thời gian thực trong hệ thong diéu khién giao thong hang khong.1 Mô hình hệ thống.2 Mô hình dữ liệu và các giao tác.3 Nhất quán thời gian .4 Lịch giao tác và điều khiển tương tranh.-:s-«-: :sø22 v52 822 29062 š KẾT QUẢ NGHIÊN CỨU VÀ BÀN LUẬN. HƯỚNG PHÁT TRIỂN. CÁC CÔNG TRÌNH ĐÃ CÔNG BỐ. TÀI LIỆU THAM KHẢO.

DANH MỤC CÁC TỪ VIẾT TẮT. Diễn giải tiếng Anh | __Dién giai 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 P=— —— + _ 7 5 DDB | Display Database | Cơ sở dữ liệu hiện thị 6 | DM Data ‘Manager Bộ quản trị dữ liệu |7 | DOS. | Data Operator System Hệ thống thao tác dữ liệu § DT Display Transaction. Giao tác hiện thi 9 IL | Interval Logic | Logic khoảng _ 10 'PCP- DA | "Priority Ceiling Protocol ¡| Giao thức mức ưu m tiên.

with Dynamic Adjust- ' cao nhất với điều chỉnh. ment of Serialization Or- | dong của thứ tự khả tuần | der | tu LH I PL Predicate Logic Logic vi tir | 12 | RM Ratc Monotonic Thuật toán lập lịch xác .định mức ưu tiên theo ¡ chu kỳ '13 R/WPCP Read/Write Priority Ceil- r Giao thức đọc/ghi mức | ing Protocol _uu tién cao nhất | — _ ————— — J | 14 | ST, Sensor Transaction | Giao tác cảm n nhận | 115 TDB Target Database Co SỞ dữ liệu đích C15, - TDB TagetDi ee —= | 14 TM | Transaction Manager | Bộ quản trị giao tác c16 2PL | Two Phase Locking Khoá hai pha DANH SÁCH BẢNG 1.1 Các yêu cầu đặc trưng của CSDL thời gian thực DANH SÁCH HÌNH 1.4 Mô hình CSDL thời gian thực. 19 Các hàm giá trị của các kiểu giao tác thời gian thực. 20 Nhất quán thời gian của dữ liệu.

21 Thực hiện của các giao tác dưới R/WPCP. 26 Thực hiện của các giao tác dưới BAP. 28 Thực hiện của các giao tác dưới PCP-DA. 31 Đồ thị thể hiện các biến trạng thái.

47 Nhất quán thời gian. 57 Thực hiện cập nhật của giao tác cảm nhận. 59 Duy trì nhất quấn: :: : ss : : s5 : : s6 z: sẽ ý: äẽ c 52 ‹ 61 Lịch của R/WPCP trong môi trường đa bộ xử lý. 80 Mô hình hệ thống CSDL thời gian thực trong điều khiển giao thông: hàng không ; : : s¿ : ¿ søzz z5 22 (2022 222 5222 ý 82 Thực hiện của các giao tác.

83 Lịch của R/WPCP trong hệ thống điều khiển giao thông hàng KHÔNE Số 000. eesesl oe ee 86 MỞ ĐẦU Hệ thống cơ sở đữ 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 và 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 và 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 tại, được áp dụng 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 bát đầ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 Šystems 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.