Đặt vấn đề Đặc tả và kiểm chứng hình thức là một pha quan trọng nhằm nâng cao độ tin cậy và chất lƣợng của phần mềm. Có thể chia đặc tả phần mềm ra làm hai loại: đặc tả phi hình thức là đặc tả dựa trên ngôn ngữ tự nhiên và đặc tả hình thức là đặc tả dựa trên kiến trúc toán học. Đặc tả phi hình thức không đƣợc chặt chẽ bằng đặc tả hình thức nhƣng đƣợc nhiều ngƣời biết và có thể dùng để trao đổi với nhau để làm chính xác hóa các điểm chƣa rõ, chƣa thống nhất giữa các bên phát triển hệ thống. Đặc tả hình thức là đặc tả mà ở đó các từ ngữ, cú pháp, ngữ nghĩa đƣợc định nghĩa hình thức dựa vào toán học.
Đặc tả hình thức có thể coi là một phần của hoạt động đặc tả phần mềm. Trong đặc tả hình thức các đặc tả yêu cầu đƣợc phân tích chi tiết, các mô tả trừu tƣợng của các chức năng chƣơng trình có thể đƣợc tạo ra để làm rõ yêu cầu. Đặc tả phần mềm hình thức là một đặc tả đƣợc trình bày trên một ngôn ngữ bao gồm: từ vựng, cú pháp và ngữ nghĩa đƣợc định nghĩa. Định nghĩa ngữ nghĩa đảm bảo ngôn ngữ đặc tả không phải là ngôn ngữ tự nhiên mà dựa trên toán học.
Các chức năng nhận các đầu vào trả lại các kết quả. Các chức năng có thể định ra các điều kiện tiền tố và hậu tố. Điều kiện tiền tố là điều kiện cần thỏa mãn để có dữ liệu vào, điều kiện hậu tố là điều kiện cần thỏa mãn sau khi có kết quả. Có hai hƣớng tiếp cận đặc tả hình thức để phát triển các hệ thống tƣơng đối phức tạp: - Tiếp cận đại số, hệ thống đƣợc mô tả dƣới dạng các toán tử và các quan hệ - Tiếp cận mô hình, mô hình hệ thống đƣợc cấu trúc sử dụng các thực thể toán học nhƣ là các tập hợp và các thứ tự Kiểm thử một sản phẩm phần mềm là xây dựng một cách có chủ đích những tập dữ liệu và dãy thao tác nhằm đánh giá một số hoặc toàn bộ các tiêu chuẩn của sản phẩm phần mềm đó.
Thử nghiệm có hai mục đích: chỉ ra hệ thống phù hợp với đặc tả và phơi ra đƣợc các khuyết tật của hệ thống. Trong khi việc kiểm thử phần mềm (software testing) [4] chỉ có thể chỉ ra các lỗi phát hiện đƣợc nhƣng không thể chỉ ra đƣợc phần mềm hoàn toàn không có lỗi, các phƣơng pháp kiểm TIEU LUAN MOI download : skknchat@gmail.com 2 chứng có thể đảm bảo hệ thống không có lỗi sau khi đã đƣợc kiểm chứng đúng đắn. Theo hƣớng tiếp cận mô hình, chúng ta có phƣơng pháp kiểm chứng mô hình (Model checking) [3], với đầu vào là một otomat hữu hạn trạng thái và thuộc tính cần kiểm chứng, sẽ cho kết quả đầu ra là true hoặc false. Hiện nay có nhiều phƣơng pháp hỗ trợ đặc tả và kiểm chứng phần mềm theo hƣớng tiếp cận trên nhƣ SPIN [5], SMV [6], NuSMV [7].
Khác với kiểm chứng mô hình, chứng minh tự động (Theorem Proving) có thể kiểm chứng các hệ thống với mô hình là vô hạn trạng thái; CafeOBJ [2] là một ngôn ngữ hỗ trợ đặc tả và kiểm chứng theo tƣ tƣởng của chứng minh tự động. Mục đích của khóa luận là tìm hiểu về phƣơng pháp đặc tả và kiểm chứng hình thức phần mềm trong CafeOBJ. Từ mô tả của hệ thống cần kiểm chứng, chúng ta cần đặc tả hệ thống một cách hình thức bằng ngôn ngữ CafeOBJ. Các thuộc tính cần kiểm chứng của hệ thống cũng đƣợc đặc tả một cách tƣơng tự.
Sử dụng ngữ nghĩa cú pháp trong ngôn ngữ CafeOBJ để thể hiện các đặc tả hệ thống cũng nhƣ các đặc tả thuộc tính của hệ thống cần kiểm chứng dƣới dạng hình thức từ các phát biểu của ngôn ngữ tự nhiên.2 Nêu bài toán Bài toán thực hiện trong khóa luận là bài toán đặc tả và kiểm chứng hệ thống đa tác tử (MAS) sử dụng ngôn ngữ CafeOBJ. Tài liệu [1] đã giải quyết đƣợc trƣờng hợp xung đột tài nguyên, tại một thời điểm chỉ có một tiến trình (agent) đƣợc sử dụng tài nguyên dùng chung. Khóa luận của tôi sẽ tập trung vào chứng minh các thuộc tính khác của hệ thống đa tác tử bằng ngôn ngữ CafeOBJ; tƣ tƣởng chứng minh là dùng phƣơng pháp qui nạp, phân rã bài toán ra các trƣờng hợp và thêm các bổ đề vào. Tƣ tƣởng trên đã kiểm chứng đƣợc hệ thống đa tác tử (MAS) với không gian trạng thái là vô hạn.3 Kết quả Luận văn đã đạt đƣợc các kết quả sau: - Tìm hiểu và nắm rõ phƣơng pháp đặc tả phần mềm sử dụng ngôn ngữ đại số CafeOBJ.
- Nắm vững phƣơng pháp chứng minh tự động sử dụng tƣ tƣởng qui TIEU LUAN MOI download : skknchat@gmail.com 3 nạp toán học để kiểm chứng các thuộc tính bất biến (invariant property). Với phƣơng pháp này, để chứng minh một thuộc tính bất biến, chúng ta cần chứng minh nó đúng tại trạng thái khởi tạo của hệ thống. Giả sử thuộc tính đúng tại một trạng thái bất kỳ s, chúng ta phải chứng minh nó đúng với mọi trạng thái tiếp theo của s. - Áp dụng những kiến thức đã tìm hiểu để kiểm chứng 04 thuộc tính của hệ thống đa tác tử.
Trong hệ thống này, các tác tử chia sẻ một tài nguyên dùng chung. Số lƣợng tác tử trong hệ thống là vô hạn vì vậy không gian trang thái là vô hạn. Với hệ thống này, chúng ta không thể áp dụng các phƣơng pháp kiểm chứng mô hình vì lý do trên. Kết quả kiểm chứng cho thấy hệ thống đa tác tử thỏa mãn các thuộc tính cần kiểm tra tại mọi trạng thái của hệ thống.4 Cấu trúc luận văn Các phần còn lại của luận văn có cấu trúc nhƣ sau: - Chƣơng 2 trình bày tổng quan về ngôn ngữ CafeOBJ, kỹ thuật đặc tả và kiểm chứng phần mềm bằng phƣơng pháp hình thức đƣợc sử dụng trong CafeOBJ.
- Một hệ thống đa tác tử và 5 thuộc tính đƣợc đặc tả trong chƣơng 3. - Chƣơng 4 mô tả về phƣơng pháp kiểm chứng hệ thống đa tác tử bằng ngôn ngữ CafeOBJ, với tƣ tƣởng quy nạp, có thể kiểm chứng với không gian trạng thái là vô hạn. - Tóm tắt kết quả đã đạt đƣợc, kết luận, những hạn chế và hƣớng nghiên cứu phát triển trong tƣơng lai sẽ đƣợc trình bày trong chƣơng 5. TIEU LUAN MOI download : skknchat@gmail.com 4 CHƢƠNG 2 TỔNG QUAN VỀ CafeOBJ 2.1 Giới thiệu CafeOBJ là một ngôn ngữ đặc tả đại số đƣợc phát triển ở Nhật Bản dƣới sự chỉ đạo của GS Kokichi Futatsugi trong phòng thí nghiệm Language Design tại Viện khoa học và công nghệ tiên tiến Nhật Bản (JAIST).
Chúng hỗ trợ phƣơng pháp kiểm chứng dựa trên kỹ thuật đặc tả đại số và phƣơng pháp quy nạp nhằm kiểm chứng các chƣơng trình với miền trạng thái vô hạn. CafeOBJ là một ngôn ngữ thực thi dựa trên nhiều cơ sở lôgic, chủ yếu dựa trên các đại số ban đầu và đại số đƣợc suy luận. Các lôgic cơ bản của CafeOBJ bao gồm : - Lôgic đƣợc sắp xếp theo thứ tự (Order-sorted logic): một kiểu có thể là kiểu con của kiểu khác. Ví dụ: số tự nhiên là thuộc số hữu tỉ, nhƣng chúng đảm bảo tính chất hợp lệ là 3 phải bằng 6/2.
- Lôgic biến đổi (Rewriting logic): Ngoài ra để bằng nhau, các biểu thức phải hợp lệ tính đối xứng, chúng ta có thể sử dụng quan hệ bắc cầu. Đặc trƣng của quan hệ bắc cầu là rất thuận lợi để thể hiện đồng thời hoặc tính không xác định. - Các kiểu ẩn (Hidden sorts): Chúng ta có 2 loại trƣơng đƣơng. Một là tƣơng đƣơng cực tiểu (minimal equivalence) chính là đồng nhất hóa 2 vế và chúng tƣơng đƣơng khi và chỉ khi chúng giống nhau thông qua các phƣơng trình đã cho.
Kiểu tƣơng đƣơng khác dùng cho kiểu ẩn, là biến đổi 2 vế là tƣơng đƣơng khi và chỉ khi chúng ứng xử đồng nhất dựa trên bộ quan sát đã cho. Đặc tả trong CafeOBJ bao gồm các mô đun. Mỗi mô đun trong CafeOBJ đƣợc định nghĩa với cú pháp nhƣ hình 2.1, trong đó < mod_name > là tên của mô đun và mod_elements là thành phần của mô đun. mod module-name { module-elements } TIEU LUAN MOI download : skknchat@gmail.
Cú pháp của mô đun.2 đặc tả 2 mô đun là mô đun SIMPLE-NAT và mô đun NAT+, đƣợc lƣu là simple-nat.mod; mô đun SIMPLE-NAT định nghĩa hai phép toán 0 và s (next). Mô đun NAT+ kế thừa mô đun SIMPLE-NAT, định nghĩa thêm phép toán + và tính chất của phép toán 0 và s (next) bởi từ khóa eq. mod! SIMPLE-NAT { [ Nat ] op 0 : -> Nat { constr } op s : Nat -> Nat { constr } } mod! NAT+ { pr(SIMPLE-NAT) op _+_ : Nat Nat -> Nat eq 0 + M:Nat = M. Đặc tả mô đun simple-nat.
Có 3 kiểu khai báo mô đun trong CafeOBJ là mod! (Tight modules) , mod* (Loose modules ), mod. Để load mô đun simple-nat.mod ta dùng cú pháp in filename CafeOBJ> in simple-nat processing input : simple-nat.mod -- defining module! SIMPLE-NAT. -- defining module! NAT+. Đọc file simple-nat.mod trong CafeOBJ.
Với từ khóa eof trong CafeOBJ, chƣơng trình sẽ chỉ đọc file đến dòng trƣớc từ eof, ở hình 2.4 chƣơng trình sẽ chỉ đọc mod SIMPLE-NAT mà lờ đi mod NAT+ mod! SIMPLE-NAT { [ Nat ] op 0 : -> Nat { constr } op s : Nat -> Nat { constr } TIEU LUAN } MOI download : skknchat@gmail. Mô tả eof trong CafeOBJ. Định nghĩa kiểu (sort) trong CafeOBJ có cú pháp nhƣ sau: [ sort-name. sort-name ] Định nghĩa kiểu con (subsort) trong kiểu (sort) nhƣ sau: [ subsort-name < supersort-name ] Hình 2.5 sẽ mô tả kiểu số nguyên không âm là kiểu con của kiểu số nguyên, định nghĩa phép toán nhân hai số nguyên, phép chia một số nguyên cho một số nguyên không âm.
[ NzInt < Int ] op _*_ : Int Int -> Int op _/_ : Int NzInt -> Int Hình 2. Định nghĩa subsort trong sort. Các thành phần của mô đun đƣợc cấu trúc trong ba phần chính. Phần thứ nhất, imports chỉ rõ các mô đun phải đƣợc khai báo trong mô đun hiện thời, hay là sự thừa kế các mô đun đã triển khai đƣợc khai báo trong mô đun hiện thời.
Có ba dạng của việc thừa kế các mô đun: protecting (thừa kế các mô đun nhƣng không thể thay đổi chúng), extending (thừa kế các mô đun có thể mở rộng chúng, nhƣng những mô tả ban đầu còn lại không đƣợc thay đổi) và using (thừa kế các mô đun có thể mở rộng hoặc thay đổi sự mô tả ban đầu).