Chương 1. GIỚI THIỆU Kiểm chứng mô hình (model checking) [5, 6, 9] và các kỹ thuật kiểm thử (testing) đang được xem là các giải pháp chủ yếu nhằm đảm bảo chất lượng cho các sản phẩm phần mềm nói chung và các hệ thống đa tác tử nói riêng. Các kỹ thuật kiểm thử chỉ có khả năng phát hiện ra lỗi hoặc khiếm khuyết của hệ thống chứ không thể chỉ ra được hệ thống không còn lỗi. Do đó, nếu chỉ áp dụng các kỹ thuật kiểm thử không thôi thì chưa đủ để đảm bảo chất lượng của hệ thống, đặc biệt là đối với những hệ thống yêu cầu độ tin cậy cao.
Để giải quyết vấn đề này, một trong những phương pháp đang được áp dụng phổ biến là phương pháp kiểm chứng mô hình. Hiện nay có nhiều phương pháp hỗ trợ việc đặc tả và kiểm chứng phần mềm theo hướng tiếp cận mô hình như SMV [7], NuSMV [8], v. Tuy nhiên, phương pháp kiểm chứng mô hình chỉ áp dụng được với các hệ thống có số lượng tác tử là hữu hạn và phải xây dựng được máy hữu hạn trạng thái đặc tả chính xác hành vi của hệ thống. Đây là một trong những điểm yếu của phương pháp này, bởi vì trên thực tế, đối với các hệ đa tác tử, số lượng các tác tử là thường xuyên thay đổi trong các giai đoạn phát triển hệ thống, thậm chí là trong quá trình thực thi hệ thống.
Mặt khác, vấn đề bùng nổ không gian trạng thái là hoàn toàn có thể xảy ra khi áp dụng phương pháp kiểm chứng mô hình cho hệ thống lớn mà ở đó số lượng các tác tử chưa biết trước. Trong trường hợp này, phương pháp chứng minh định lý (theorem proving) là rất phù hợp để chứng minh tính đúng đắn của các hệ đa tác tử. Vấn đề cần giải quyết trong luận văn này là chứng minh tính đúng đắn cho bài toán xung đột tài nguyên cho các hệ đa tác tử sử dụng chung đa tài nguyên. Tài liệu [2] đã chứng minh được tính đúng đắn của một số thuộc tính bất biến của hệ thống đa tác tử với chỉ một tài nguyên dùng chung.
Do đó, khi áp dụng vào hệ thống với đa tài nguyên dùng chung thì về tư tưởng chứng minh là tương tự nhưng về mặt phương pháp đặc tả thì không còn đúng nữa. Luận văn này tập trung nghiên cứu một phương pháp đặc tả và kiểm chứng các hệ đa tác tử sử dụng chung đa tài nguyên và sau đó để cụ thể hóa, luận văn này đã áp dụng vào việc đặc tả và chứng minh tính đúng đắn cho hệ thống đại lý vé máy bay bằng việc sử dụng bộ chứng minh định lý CafeOBJ [3, 4]. Phần còn lại của luận văn này được cấu trúc như sau. Chương 2 trình bày tổng quan về ngôn ngữ CafeOBJ, đây là công cụ để hỗ trợ việc đặc tả và kiểm chứng phần mềm theo tư tưởng của chứng minh định lý (theorem proving).
Chương 3 trình bày việc đặc tả và kiểm chứng các hệ đa tác tử sử dụng chung đa LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 2 tài nguyên. Chương này giới thiệu về hệ thống đa tác tử sử dụng chung đa tài nguyên, phương pháp đặc tả và kiểm chứng các hệ đa tác tử sử dụng chung đa tài nguyên. Chương 4 trình bày việc đặc tả và chứng minh tính đúng đắn cho hệ thống đại lý vé máy bay. Trong chương này trình bày một ví dụ minh họa cho việc đặc tả và kiểm chứng các hệ đa tác tử sử dụng chung đa tài nguyên.
Một hệ thống quản lý việc đặt vé máy bay của các đại lý vé máy bay là một ví dụ điển hình cho một hệ thống đa tác tử sử dụng chung đa tài nguyên. Mô tả bài toán đặt vé máy bay bằng ngôn ngữ tự nhiên và sau đó là mô tả bài toán này trong hệ chuyển trạng thái quan sát được – OTS (Observational Transition System). Từ đó, đặc tả và kiểm chứng tính đúng đắn cho hệ thống đại lý vé máy bay bằng bộ chứng minh định lý CafeOBJ. Chương 5 là kết luận và định hướng phát triển của đề tài.
Phần cuối cùng là tài liệu tham khảo và phụ lục. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 3 Chương 2. TỔNG QUAN VỀ CafeOBJ 2. Giới thiệu CafeOBJ [3, 4] là một ngôn ngữ đặc tả đại số, có khả năng thực thi dựa trên nhiều cơ sở lôgic khác nhau, phần lớn dựa vào các đại số ban đầu và các đại số được suy diễn.
Ngôn ngữ này hỗ trợ phương pháp kiểm chứng dựa trên các kỹ thuật đặc tả đại số và phương pháp quy nạp toán học nhằm mục đích kiểm chứng tính đúng đắn của các chương trình với miền trạng thái là vô hạn. Ngôn ngữ CafeOBJ bao gồm ba lôgic cơ bản: Order-sorted logic (lôgic được sắp xếp theo thứ tự): một kiểu có thể là một kiểu con của kiểu khác. Thí dụ, tập hợp các số tự nhiên là tập con của tập hợp các số hữu tỷ, điều này khẳng định tính hợp lệ rằng 3 phải bằng 6/2. Chúng cũng thực hiện việc kế thừa các phép toán, nghĩa là, một phép toán trên tập hợp các hữu tỷ cũng tự động được sử dụng trên tập hợp các số tự nhiên.
Hơn nữa, mối quan hệ kiểu con ở đây còn cho phép chúng ta có một cách đơn giản hơn để xác định các phép toán cục bộ và việc xử lý các ngoại lệ. Rewriting logic (lôgic biến đổi): thêm vào đó, để bằng nhau các biểu thức phải hợp lệ về tính đối xứng, chúng ta có thể sử dụng quan hệ bắc cầu, không nhất thiết phải là trực tiếp. Điểm mạnh của việc sử dụng quan hệ bắc cầu là rất thuận tiện trong việc thể hiện tính đồng thời hoặc tính bất định. Loại tương đương còn lại là được dùng cho kiểu ẩn, hai vế tương đương với nhau khi và chỉ khi chúng phản ứng như nhau với cùng một bộ quan sát.
Một tính năng rất hữu ích khác của CafeOBJ là có khả năng truyền tham số (parameters). Có nhiều kiểu dữ liệu trừu tượng như kiểu dữ liệu danh sách (lists), kiểu dữ liệu tập hợp (sets), kiểu dữ liệu hàng đợi (queues), kiểu dữ liệu ngăn xếp (stacks)., chúng ta có thể định nghĩa mỗi kiểu dữ liệu này bằng một loại mô-đun trong CafeOBJ có khả năng truyền tham số (parameterised modules), mô-đun dạng này có các thành phần cơ bản được truyền qua tham số từ bên ngoài vào. Việc đặc tả trong CafeOBJ là thông qua các mô-đun. Khi khai báo một mô-đun ta có thể bắt đầu với từ khóa module hoặc mod.
Trong CafeOBJ có ba LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 4 kiểu khai báo mô-đun: mod!, mod* và mod. Hiện tại, trong quá trình thực thi ngôn ngữ CafeOBJ không phân biệt ba kiểu khai báo trên, tuy nhiên việc khai báo rõ kiểu của mô-đun là rất cần thiết, nó giúp cho việc hiểu về đặc tả của mô- đun đó một cách đầy đủ, chính xác, đặc biệt là đối với các hệ thống phức tạp. Một mô-đun không có tham số trong CafeOBJ được khai báo với cú pháp được trình bày như trong hình 2. module module_name { module_element * } Hình 2.1: Định nghĩa mô-đun trong CafeOBJ.
Chi tiết của định nghĩa mô-đun trong hình 2.1 như sau: Module_name là tên của mô-đun cần định nghĩa, module_element là các thành phần của mô-đun, thành phần của một mô-đun có thể là các khai báo của việc kế thừa từ các mô-đun khác (import declaration), hoặc việc khai báo các biến (sort declaration), hoặc việc khai báo các phép toán (operation declaration), hoặc việc khai báo các biến (variable declaration), hoặc việc khai báo các phương trình (equation declaration), hoặc việc khai báo các dịch chuyển (transition declaration). Chúng ta cùng xem xét hai ví dụ trong hình 2.2: Đặc tả mô-đun SIMPLE- NAT và hình 2.3 : đặc tả mô-đun NAT+. 1: mod! SIMPLE-NAT { 2: [ Nat ] 3: op 0 : -> Nat { constr } 4: op s : Nat -> Nat { constr } 5: } Hình 2.2: Đặc tả mô-đun SIMPLE-NAT trong CafeOBJ. Chi tiết của khai báo trong hình 2.2 như sau: Để khai báo và định nghĩa cho một mô-đun, đầu tiên ta khai báo kiểu của mô-đun sau đó đến tên của mô-đun (dòng 1).
Định nghĩa kiểu dữ liệu Nat (dòng 2), định nghĩa hằng số 0 thuộc kiểu dữ liệu Nat ta bắt đầu bằng từ khóa op (dòng 3), định nghĩa phép toán s (phép tăng một số tự nhiên lên 1 đơn vị) ta bắt đầu bằng từ khóa op (dòng 4). LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 5 1: mod! NAT+ { 2: pr(SIMPLE-NAT) 3: op _+_ : Nat Nat -> Nat 4: eq 0 + M:Nat = M .3: Đặc tả mô-đun NAT+ trong CafeOBJ. Chi tiết của khai báo trong hình 2.3 như sau: Mô-đun NAT+ kế thừa mô-đun SIMPLE-NAT (dòng 2), khi kế thừa từ một mô-đun khác, trong CafeOBJ hỗ trợ ba kiểu kế thừa: protecting, extending và using, có thể viết ngắn gọn hơn là: pr, ex và us. Dòng 3 là việc khai báo phép toán cộng, ta bắt đầu với từ khóa op, phép toán này có hai đối số kiểu Nat, kết quả của phép toán này cũng có kiểu Nat.
Dòng 4 là việc định nghĩa một phương trình với phép cộng số 0 với một số bất kỳ thuộc kiểu Nat, ta bắt đầu bằng từ khóa eq, kết quả trả về là chính nó, đặc tả này đã gộp cả việc khai báo biến M thuộc kiểu Nat, chú ý rằng, sau mỗi phương trình ta phải cách ra một dấu cách và kèm theo đó là một dấu chấm “. Dòng 5 là định nghĩa phương trình với vế trái là phép cộng của phép toán s tăng biến N lên một đơn vị với biến M, vế phải là phép toán s tăng kết quả của phép cộng N và M lên một đơn vị. Như vậy ta đã đặc tả xong hai mô-đun SIMPLE-NAT và NAT+. Bây giờ ta lưu file đặc tả này với tên example1.
Để đọc đặc tả các mô-đun ta đã lưu trong file example1.mod, ta chạy chương trình CafeOBJ lên, sau đó chỉ đến đường dẫn lưu file vừa rồi, tiếp đến ta gõ từ khóa in, cách ra một dấu cách và gõ example1. Chương trình CafeOBJ đọc đặc tả thành công thì sẽ có thông báo như sau: processing input : example1.mod -- defining module! SIMPLE-NAT. -- defining module! NAT+.4: Hội thoại giữa CafeOBJ với người dùng. Để việc đặc tả được rõ ràng hơn, CafeOBJ hỗ trợ việc tổ chức các thành phần của một mô-đun vào ba khối chính (blocks) là : khối imports – nơi khai báo các mô-đun mà mô-đun hiện tại tham chiếu đến, khối signature - nơi định nghĩa các kiểu dữ liệu và các phép toán, khối axioms – nơi khai báo các biến LUAN VAN CHAT LUONG download : add luanvanchat@agmail.5 mô tả chi tiết việc tổ chức các khối của mô-đun NAT+.
mod!