Chương 1 trình bày các khái niệm cơ bản trong CSDL, CSDL thời gian thực, như điều khiển tương tranh, điều kiện đúng và tính khả tuần tự, mô hình CSDL thời gian thực, các đặc điểm dif liệu va giao tác, điều khiển tương tranh thời gian thực, đảo ngược mức ưu tiên, kế thừa mức ưu tiên, và một số giao thức điều khiển tương tranh tiêu biểu như giao thức doc/ ghi mức ưu tiên cao nhất (R/WPCP), giao thức huỷ bỏ cơ sở (BAP), giao thức mức ưu tiên cao nhất với điều chỉnh động của thứ tự khả tuần tự (PCP-DA). Chương 2 trình bày tóm lược về cú pháp, ngữ nghĩa, hệ thống chứng minh của logic khoảng, và logic tính toán khoảng. Chứng minh một số định lý, làm cơ sở cho việc xây dựng và phát triển mô hình hình thức cũng như đặc tả và kiểm chứng hình thức trong CSDL thời gian thực. Chương 3 xây dựng mô hình hình thức của hệ thống CSDL thời gian thực trong logic tính toán khoảng.
Xây dựng các biến trạng thái DC để mô hình hoá hệ thống CSDL thời gian thực được đặc trưng bởi dữ liệu và các giao tác, viết các công thức DC trên các biến trạng thái để mô tả các thuộc tính của hệ thống CSDL thời gian thực. Sau đó đưa ra một đặc tả điều kiện đúng cho thực hiện song song của hệ thống giao tác trong CSDL thời gian thực. Đặc tả và kiểm chứng một số điều kiện để duy trì tính nhất quán thời gian trong hệ thống CSDL thời gian thực. Chương 4 phát triển phương pháp luận để đặc tả và kiểm chứng hình thức giao thức điều khiển tương tranh trong CSDL thời gian thực.
Sử dung mô hình hình thức của CSDL thời gian thực được dé xuất trong chương 3 để đặc tả và kiểm chứng hình thức một lớp các giao thức điều khiển tương tranh như R/WPCP, BAP, PCP-DA. Thông qua việc đặc tả và kiểm chứng hình thức, chúng tôi đã nhận thấy rằng số đảo ngược mức ưu tiên của một số giao thức trong môi trường đa bộ xử lý có thể nhiều hon mot lần. Chúng tôi đã cải tiến một số giao thức cho môi trường đa bộ xử lý. Kết quả nghiên cứu này có thể áp dụng và mở rộng cho nhiều giao thức khác nhau trong CSDL thời gian thực, khi thực hiện trong môi trường đa bộ xử lý.
Sau đó, chúng tôi nghiên cứu ứng dụng hệ thống CSDL thời gian thực trong hệ thống điều khiển giao thông hàng không như mô hình hệ thống, dữ liệu, giao tác, nhất quán thời 14 gian và điều khiển tương tranh. Từ các kết quả nghiên cứu chi tiết về đặc tả và kiểm chứng hình thức các giao thức điều khiển tương tranh, chúng tôi đã ứng dụng các giao thức đó vào trong hệ thống điều khiển giao thông hàng không. Cuối cùng là phần kết luận, tóm tắt các kết quả trong nghiên cứu và trình bày hướng nghiên cứu phát triển trong tương lai của chúng tôi. iS CHUONG 1 CO SO DU LIEU THOI GIAN THUC Chương nay trình bay một số khái niệm chính của hệ thống CSDL, hệ thống CSDL thời gian thực và giao thức điều khiển tương tranh trong CSDL thời gian thực.1 Cơ sở dữ liệu Cơ sở dữ liệu là một hệ thống tích hợp các quan hệ dữ liệu về các tổ chức được lưu trữ trên máy tính.
Thực tế dữ liệu được lưu giữ trong CSDL thể hiện trạng thái của CSDL tại một thời điểm nhất định. Bởi vì nội dung của CSDL thay đổi khi thông tin dữ liệu được cập nhật hoặc bị xoá từ CSDL, chúng ta có thể định nghĩa một CSDL với một tập các đối tượng đữ liệu, mỗi tập dữ liệu là một biến thay đổi theo thời gian và một trạng thái của CSDL tại một thời điểm / là một giá trị của các biến cho các đối tượng dữ liệu tai thời điểm ¡. Mỗi CSDL thường kết hợp với một tập các ràng buộc toàn vẹn mà dữ liệu đúng trong CSDL phải thoả mãn. Các giá trị của dữ liệu được phép lưu trữ trong CSDL chỉ khi chúng không vi phạm các ràng buộc toàn vẹn tương ứng.
Các ràng buộc đữ liệu đó thường được thể hiện như các công thức logic trên các đối tượng dữ liệu.2 Điều khiến tương tranh trong CSDL Một trong các mục đích chính của các hệ thống CSDL là cho phép nhiều người sử dụng để truy cập chia sẻ dữ liệu đồng thời [12]. Truy cập song song là dễ nếu tất cả mọi người sử dụng, chỉ đọc dữ liệu. Khi đó việc đọc dữ liệu của người này sẽ không ảnh hưởng tới những người khác. Tuy nhiên, khi hai hoặc nhiều người sử dụng cùng truy cập CSDL song song và ít nhất một trong số họ muốn ghi dữ liệu, khi đó tác động ghi dữ liệu có thể ảnh hưởng tới việc đọc dữ liệu, đọc trước và sau khi ghi là khác nhau.
Điều nay có thể gây ra vấn đề không nhất quán dữ liệu [12]. Vì nhiều người sử dụng có thể truy cập dữ liệu vào CSDL tai cùng thời điểm, nên cần đảm bảo rằng các thao tác thực hiện song song luôn luôn duy trì tính nhất quán dữ liệu trong CSDL. Truy cập của người sử dụng được thực hiện bởi các giao tác. Một giao tác là một dãy logic của các thao tác được đặc trưng bởi các thuộc tính sau: e Nguyên tử: hoặc là tất cả hoặc không có một thao tác nào của giao tác được thực hiện.
e Nhất quán: một giao tác, khi thực hiện độc lập sẽ chuyển CSDL từ một trạng thái nhất quán tới một trạng thái nhất quán khác, e Độc lập: thực hiện của giao tác nay không ảnh hưởng tới các giao tác khác, e Bén vững: khi một giao tác đã uỷ thác, hệ thống phải đảm bảo tính bền vững của nó không phụ thuộc vào hỏng hóc sau đó. Chú ý rằng bất cứ thao tác nào trong CSDL cũng được xem xét như là một phần của một giao tác. Trong một hệ thống giao tác, khi chúng thực hiện song song có thể ảnh hưởng đến tính nhất quán của dữ liệu trong CSDL vì sự ảnh hưởng giữa các giao tác. Dé các giao tác thực hiện không ảnh hưởng tới các giao tác khác, thực hiện của chúng phải được điều khiển bằng các giao thức điều khiển tương tranh.
Giao thức điều khiển tương tranh được biết đến nhiều nhất trong hệ thống quản trị CSDL là giao thức khoá hai pha Pre 17 đo“ W-L4/222 là 1 2 ORM Adee [12]. Trong giao thức khoá hai pha (2PL), mỗi đối tượng dữ liệu có hai loại khoá: các khoá doc (read locks) và các khoá ghi ( write locks). Một giao tác có thể đọc hoặc ghi trên một đối tượng dữ liệu + khi và chỉ khi nó có một khoá đọc hoặc ghi trên z tương ứng. Hai khoá nói là bị xung đột khi và chỉ khi chúng thao tác trên cùng một đơn vị dữ liệu và một trong chúng là khoá ghi.
Các giao tác chỉ có thể chia sẻ các khoá không bị xung đột. Trong 2PL, mọi giao tác đều thực hiện theo hai pha. Pha đầu được gọi là pha nhận, các khoá trên các đối tượng di liệu cần xử lý bởi các giao tác và không có khoá nào được giải phóng, trong khi pha thứ hai thì giải phóng khoá và không thể nhận một khoá mới. Một giao thức điều khiển tương tranh được xem là đúng khi và chỉ khi bất cứ thực hiện nào của các giao tác được điều khiển bởi nó cũng thoả mãn điều kiện đúng, đó là tính khả tuần tự.
Điều kiện đúng và tính khả tuần tự Hiển nhiên là một thực hiện tuần tự của các giao tác sẽ đưa CSDL từ một trạng thái nhất quán tới một trạng thái nhất quán khác, và do đó nó được xem như là đúng. Do vậy, điều kiện đúng để thực hiện song song của các giao tác trong hệ thống quản trị CSDL là khả tuần tự, nghĩa là thực hiện song song các giao tác đó cho những kết quả như chúng thực hiện tuần tự. Tính khả tuần tự có thể được định nghĩa tương đương như sau. Định nghĩa 1 Mot thực hiện song song của các giao tác gọi là khả tuần tự khi và chỉ khi tồn tại một thứ tự toàn bộ trên tập các giao tác sao cho khi một giao tác T trước một giao tác 1' theo thứ tự này, thì bất cứ thao tác O nào cua † phải thực hiện trước các thao tác O' của 1" trong đó O' xung đột với O khi thực hiện song song [12].
Trong hầu hết các giao thức điều khiển tương tranh, tính khả tuần tự là dựa trên khái niệm của các thao tác xung đột và được gọi là khả tuần tự xung đội. Trong đó, hai thao tác được gọi là xung đột nếu chúng thao tác trên cùng một đơn vị dữ liệu và ít nhất một trong chúng là thao tác ghi.3 Cac đặc điểm dữ liệu và giao tác của CSDL thời gian thực Tất cả các khái niệm đã đề cập ở trên cho hệ thống CSDL cũng được áp dụng cho CSDL thời gian thực. Các đặc trưng mới cho CSDL thời gian thực là các đặc tính thời gian. Một hệ thống CSDL thời gian thực bao gồm hệ thống quản trị CSDL truyền thống và hệ thống thời gian thực [13].
Trong CSDL thời gian thực, các giao tác không chỉ thoả mãn điểm tới hạn, mà chúng còn phải sử dụng dữ liệu hợp lệ trong khi thực hiện. Trong hệ thống CSDL thời gian thực, các đối tượng di liệu được chia thành các đối tượng dữ liệu liên tục va các đối tượng dif liệu rời rac. Mô hình hệ thống CSDL được mô tả trong Hình 1. Tlbv>h|iậếịýt G t i á s e a ncg o r Đối tượng dữ liệu Đối tượng dữ liệu liên tục roi rac |h : ĩ 7 Bo diéu RATER [pethcewcecsrnaswnncacsmmniemensens Hình 1.1: Mô hình CSDL thời gian thực Một giá trị của đối tượng dữ liệu liên tục phản ánh trạng thái của đối tượng này trong thế giới thực.
Mỗi giá trị của đối tượng liên tục có thể không hợp lệ trong khoảng thời gian trôi qua. Các đối tượng dữ liệu rời rạc là tinh và giá trị của nó không phụ thuộc vào thời gian. Các đối tượng dữ liệu liên tục có thể chia thành các đối tượng dữ liệu cơ sở và các đối tượng dữ liệu suy diễn. Giá trị của một đối tượng dữ liệu cơ sở có thể được nhận trực tiếp từ sensor, trong khi giá trị của đối tượng dữ liệu suy diễn được tính toán từ một tập giá trị các đối tượng cơ sở.
Ví dụ: CSDL điều khiển giao thông hàng không chứa các đối tượng dữ 19 liệu cơ sở thể hiện chuyến bay trong một vùng bay xác định.