Luận văn Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ

hai, signature, khai báo các kiểu (sorts), các kiểu con (subsorts), và các toán tử (operators) được sử dụng trông mô đun. Và cuối cùng, axioms bao gồm sự khai báo của các biến, các phương trình (equations), các sự dịch chuyển (transitions), và các biểu thức thể hiện hành vi của mô đun. Hình 3.1 Mô đun EXAMPLE trong CafeOBJ. Để cung cấp sự mô tả một mô đun trong CafeOBJ, chúng ta tìm hiểu ví dụ trong Hình 2.1, với sự định nghĩa mô đun EXAMPLE như là mô tả cho số tự nhiên. Mô đun EXAMPLE thừa kế các kiểu (sorts) và các toán tử (operators) đã được định nghĩa trong hai mô đun INT và NAT. Phần signature khai báo các kiểu Pnat, Nat và Int. Ký hiệu “<” nghĩa là kiểu Nat là kiểu con của kiểu Int (chính là kiểu số tự nhiên là kiểu con của kiểu số nguyên hay là kiểu số nguyên bao gồm cả kiểu số tự nhiên). Hằng số 0, toán tử s được khai báo bởi op. Hành vi của toán tử “+” là được thực hiện bởi hai biểu thức và được khai báo bởi eq. module EXAMPLE{ imports { protecting (NAT) protecting (INT) } signature { [PNat, Nat < Int] op 0 : -> PNat op s : PNat -> PNat op (_+_) : PNat PNat -> PNat } axioms { vars N M : Pnat eq 0 + N = 0 . eq s(M) + N = s(M + N) . } } Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng 9 3.2 Đặc tả và kiểm chứng trong CafeOBJ 3.2.1 Ví dụ Để tìm hiểu về đặc tả và kiểm chứng trong CafeOBJ, chúng ta tìm hiểu một ví dụ đơn giản về sự đặc tả hệ thống số tự nhiên, đặc tả thuộc tính cần chứng minh và kiểm chứng thuộc tính đó. Trong ví dụ này chúng ta chỉ mô tả một số đặc tả cơ bản với phép toán cộng (“+”), phép so sánh (“=”), phép toán (“s”) tăng số tự nhiên lên một đơn vị, và đặc tả thuộc tính cần kiểm chứng chính là tính chất kết hợp của phép cộng tức là: (X + Y) + Z = X + (Y + Z), với X, Y, Z là số tự nhiên bất kỳ (*). Hình 3.2: Đặc tả của module PNAT cho ví dụ. mod PNAT { [Nat] -- mô tả kiểu biến là số tự nhiên là Nat op 0 : -> Nat -- hằng số 0 op s : Nat -> Nat -- phép toán tăng của số tự nhiên op _+_ : Nat Nat -> Nat -- phép toán cộng trong số tự nhiên op _=_ : Nat Nat -> Bool {comm} -- phép so sánh 2 số tự nhiên vars X Y : Nat -- các biến dùng để đặc tả -- biểu diễn quan hệ của phép toán “+” eq 0 + Y = Y . eq s(X) + Y = s(X + Y) . -- biểu diễn quan hệ của phép toán “=” eq (X = X) = true . eq (0 = s(Y)) = false . eq (s(X) = s(Y)) = (X = Y) . } Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng 10 3.2.2 Đặc tả số tự nhiên Như đã trình bày ở phần trên (mục 3.2.1), từ mô tả về số tự nhiên với ba phép toán cơ bản, và các thuộc tính của nó. Chúng ta tiến hành đặc tả bài toán bằng mô đun PNAT trong CafeOBJ như trong Hình 3.2. Đặc tả này định nghĩa các toán tử cần thiết và các quan hệ giữa chúng cho ví dụ. Trong đặc tả này, khai báo số tự nhiên kiểu [Nat], hằng số 0, các phép toán tăng “s”, phép toán cộng “+”, phép so sánh “=”, được khai báo sau từ khóa op, cùng với các phương trình biểu diễn quan hệ giữa chúng được khai báo sau từ khóa eq. 3.2.3 Đặc tả thuộc tính Với đặc tả hệ thống PNAT như trên (Hình 3.2), chúng ta cần đặc tả thuộc tính cần kiểm chứng (điều kiện (*)) như trong hình 3.3. Trong đó x, y, z là các hằng số tự nhiên bất kỳ, hàm bất biến inv nhằm kiểm tra tính đúng đắn của thuộc tính (thỏa mãn điều kiện (*)). Hình 3.3: Đặc tả thuộc tính cho điều kiện (*). 3.2.4 Kiểm chứng thuộc tính Như đã biết trong phần này chúng ta cần phải kiểm chứng thuộc tính hay chứng minh điều kiện (*) thỏa mãn với mọi số tự nhiên bất kỳ. Nghĩa là chúng ta cần phải kiểm chứng đặc tả hệ thống PNAT (Hình 3.2) thỏa mãn với đặc tả thuộc tính INV (Hình 3.3) hay sau khi thực hiện chương trình hàm inv(x, y, z) trả về giá trị “true” với mọi x, y, z thuộc số tự nhiên. Với tư tưởng kiểm chứng quy nạp nhằm kiểm chứng tín mod INV { pr(PNAT) ops x y z : -> Nat . op inv : Nat Nat Nat -> Bool vars X Y Z : Nat -- điều cần chứng minh eq inv(X,Y,Z) = ((X + Y) + Z = X + (Y + Z)) . } Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng 11 đúng đắn của đặc tả thuộc tính thỏa mãn với mọi số tự nhiên. Chúng ta tạo thêm mô đun ISTEP (Hình 3.4) với hàm istep nhằm kiểm chứng cho trường hợp tổng quát. Hình 3.4: Kiểm chứng quy nạp với module ISTEP. Hình 3.5: Kiểm chứng quy nạp cho đặc tả. Với tư tưởng kiểm chứng bằng phương pháp quy nạp đó, trong CafeOBJ cũng hỗ trợ rất mạnh mẽ sẽ được đề cập ở phần sau. Được xem như là một tư tưởng nổi bật của việc kiểm chứng phần mềm và kiểm thử phần mềm. Nhờ phương pháp quy nạp này mà việc kiểm chứng các thuộc tính của hệ thống với không gian trạng thái vô hạn được thực hiện một cách rõ ràng. Nhằm đảm bảo phần mềm không có lỗi. Và trong Hình 3.5 chúng ta thấy được sự kiểm chứng qua hai trường hợp đó là trường hợp cơ sở và trường hợp tổng quát. Sau Khi thực hiện chương trình như Hình 3.5 trong CafeOBJ, hệ mod ISTEP{ pr(INV) vars X Y Z : Nat op istep : Nat Nat Nat -> Bool eq istep(X, Y, Z) = inv(X, Y, Z) implies inv(s(X), Y, Z) . } --> Trường hợp cơ sở với x = 0 open INV -- Kiểm tra red inv(0,y,z) . close --> Trường hợp tổng quát là chúng ta muốn chứng minh rằng: -- giả sử inv(x,y,z) = true thì inv(s(x),y,z) = true -- nghĩa là giả sử đặc tả đúng với x bây giờ chúng ta chỉ cần -- chứng minh nó đúng với s(x) là được ). open ISTEP -- Kiểm tra red istep(x,y,z) . close Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng 12 thống CafeOBJ đều trả về kết quả “true” trong cả hai trường hợp đó. Nghĩa là hệ thống đã được kiểm chứng thỏa mãn với điều kiện (*). Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 13 Chương4 Khái quát về OTS và bài toán QLOCK 4.1 Giới thiệu về OTS Chúng ta sử dụng OTS/CafeOBJ để mô hình hóa hệ thống với kỹ thuật đại số, việc đặc tả và kiểm chứng của các hệ thống một cách rõ nét hơn. Trong phần này, chung ta sẽ mô tả cách để viết đặc tả hình thức của một số hệ thống với sự thể hiện của OTS/CafeOBJ. Ưu điểm của phương thức này: - Trình bày một mô hình hình thức để mổ tả hệ thống, trong đó chú trọng đến các quan sát (observers) cũng như các hành động trong OTS, - Phương thức OTS/CafeOBJ cung cấp một mô hình ngữ nghĩa và framework chung cho một số hệ thống phức tạp, - Đối với việc kiểm chứng hình thức một số hệ thống bới bộ chứng minh cũng được cung cấp bởi phương thức OTS/CafeOBJ. Trong chương 3 trình bày về đặc tả và kiểm chứng trong CafeOBJ với hệ thống đơn giản, trong khi thực tế có nhiều hệ thống phức tạp với sự chuyển đổi trạng thái của hệ thống khi có một hành vi nào đó tác động vào hệ thống đó. Chúng ta khó để biểu diễn hệ thống theo cách thông thường trong CafeOBJ. Vì vậy với hệ thống biến đổi trạng thái trực quan (OTS) là một mô hình toán học sẽ được định nghĩa trong phần sau sẽ giúp chúng ta có thể trực quan hóa và dễ biểu diễn các đặc tả và kiểm chứng hệ thống mộ cách chính xác và đơn giản hơn. Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 14 4.2 OTS (Observation transition system) Chúng ta giả định rằng tồn tại một không gian trạng thái gọi là Y. Khi chúng ta mô tả một hệ thống, hệ thống về cơ bản được mô hình hóa bằng cách quan sát các số lượng chỉ liên quan đến hệ thống và quan tâm tới chúng từ bên ngoài của mỗi trạng thái trong Y. Một OTS S = bao gồm: - O: Tập hợp các quan sát. Mỗi quan sát o ∈ O là một hàm o : Y → D ánh xạ tới từng trạng thái υ ∈ Y vào một số kiểu giá trị D (D có thể khác nhau cho mỗi quan sát). Giá trị trả về bởi một quan sát (trong một trạng thái) được gọi là giá trị của các quan sát (trong trạng thái). Với một OTS S và hai trạng thái υ1, υ2 ∈ Y, sự bình đẳng giữa hai trạng thái, ký hiệu là υ1=S υ2, đối với S được định nghĩa như sau: υ1=S υ2 iff ∀o ∈ O.o(υ1) = o(υ2), Với ‘=’ trong o(υ1) = o(υ2) phải được xác định rõ phạm vi của mỗi o ∈ O. - I: Các điều kiện ban đầu: Điều kiện này xác định giá trị ban đầu của mỗi quan sát, nó xác định trạng thái ban đầu của OTS. - T: Bộ quy tắc chuyển đổi có điều kiện. Mỗi quy tắc chuyển đổi τ ∈ T là một quan hệ giữa các trạng thái với điều kiện, đối với mỗi trạng thái υ ∈ Y, tồn tại một trạng thái, υ’ ∈ Y, gọi là một trạng thái tiếp sau của υ, sao cho τ(υ, υ'), cho mỗi trạng thái υ1, υ2, υ1’, υ2’ ∈ Y sao cho υ1=S υ2, τ(υ1, υ1') và τ(υ2, υ2'), υ1’=S υ2'. τ có thể được coi là một hàm tương đương với Y đối với =S. Vì vậy, τ(υ) được gọi là trạng thái tiếp sau của υ đối với τ. Các điều kiện cτ cho một quy tắc chuyển đổi τ ∈ T được gọi là điều kiện có hiệu quả. Với một trạng thái, giá trị chân lý của nó có thể được xác định bởi chỉ các giá trị của các quan sát trong trạng thái. Các vị từ của loại này được gọi là các vị từ trạng thái. Cho một trạng thái υ ∈ Y, cτ là đúng (true) trong υ, cụ thể là τ là hiệu quả trong υ, khi và chỉ khi υ # S τ(υ). Nhiều quan sát tương tự hoặc các quy tắc chuyển đổi có thể được lập chỉ mục. Nói chung, các quan sát và các quy tắc chuyển đổi được biểu diễn băng oi1 ….im và τj1 Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 15 …jm, tương ứng, với điều kiện m, n >= 0 và chúng ta giả định rằng tồn tại các kiểu dữ liệu Dk sao cho k ∈ Dk (k = i1,..., im, j1,..., jn). Ví dụ, một mảng số nguyên a sở hữu bởi một tiến trình p có thể biểu hiện bằng một quan sát ap, và sự tăng của các phần tử thứ i của mảng có thể biểu diễn bằng một quy tắc chuyển đổi incap,i. Với một OTS, Trong khóa luận này chúng ta quan tâm đến thuộc tính an toàn (safety property) được định nghĩa như sau: một vị ngữ p: Y → {true, false} là một thuộc tính an toàn đối với S khi và chỉ khi p là một trạng thái vị từ và p(υ) đúng cho mỗi υ ∈ Υ. Nếu chúng ta chứng minh rằng một OTS có thuộc tính an toàn p, theo phương pháp quy nạp được sử dụng chủ yếu sau đây: - Trường hợp cơ sở: Đối với bất kỳ trạng thái υ ∈ Υ trong đó mỗi quan sát o ∈ O thỏa mãn I, chúng ta thấy rằng p(υ) đúng. - Bước quy nạp: Với bất kỳ trạng thái đạt được υ ∈ Υ sao cho p(υ) đúng, chúng ta cho rằng, đối với bất kỳ quy tắc chuyển đổi τ ∈ T, p(τ(υ)) cũng đúng. Một OTS S được mô tả trong CafeOBJ. Không gian trạng thái Y được biểu thị là một kiểu ẩn (hidden sort) Sys, bằng cách khai báo *[Sys]*. Quan sát oi1, …, im ∈ O được biểu thị là toán tử quan sát trong CafeOBJ. Chúng ta giả định rằng các kiểu dữ liệu Dk(k = i1,..., im) và D được mô tả trong đại số ban đầu và có tồn tại các kiểu ẩn Sk(k = i1,..., im) và S tương ứng với các kiểu dữ liệu. Các toán tử quan sát CafeOBJ biểu thị oi1, …, im được khai báo như sau: bop o : Sys Si1 .... Sim -> S Các điều kiện ban đầu I, giá trị của từng quan sát trong bất kỳ trạng thái ban đầu, được mô tả bằng cách khai báo một hằng số (một toán tử không có bất kỳ đối số nào) biểu diễn bất kỳ trạng thái ban đầu và xác định giá trị của mỗi quan sát trong trạng thái với các phương trình. Trước tiên, các hằng init biểu diễn bất kỳ trạng thái ban đầu được khai báo như sau: op init: -> Sys Giả sử rằng giá trị ban đầu của oi1, …, im là f(i1, …, im), điều này có thể được mô tả trong CafeOBJ như sau: Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 16 eq o(init, Xi1, …, Xim) = f(Xi1, …, Xim) . Với Xk (k = i1,..., im) là một biến trong CafeOBJ với Sk, và f(Xi1, …, Xim) có nghĩa là một hạng tử (bao gồm Xi1,..., Xim) tương ứng với f(i1, …, im). Một nguyên tắc chuyển đổi τj1, ...,jn ∈ T được biểu diễn bởi một toán tử hành động trong CafeOBJ. Chúng ta giả định rằng các kiểu dữ liệu Dk (k = j1, ...,jn) được mô tả trong đại số ban đầu và có tồn tại các kiểu ẩn Sk (k = j1,...,jn) tương ứng với các kiểu dữ liệu. Các toán tử hành động trong CafeOBJ biểu diễn τj1, …., jn được khai báo như sau: bop a : Sys Sj1 ... Sjn -> Sys Nếu τj1,...,jn được thực hiện trong một trạng thái mà nó có hiệu quả, giá trị của oi1, …, im có thể thay đổi, nó có thể được mô tả trong CaifeOBJ nói chung như sau: ceq o(a (S, Xj1, ..., Xjn), Xi1, ..., Xim) = e-a(S, Xj1, ..., Xjn, Xi1, ..., Xim) if c-a (S, Xj1, ..., Xjn) . Với e-a(S, Xj1, ..., Xjn, Xi1, ..., Xim) có nghĩa là một hạng tử (bao gồm S, Xj1,..., Xjn, Xi1,..., Xim) tương ứng với giá trị của oi1, …, im, trong trạng thái kế tiếp sau, và c-a (S, Xj1, ..., Xjn) có nghĩa là một hạng tử (bao gồm S, Xj1,..., Xjn) tương ứng với cτj1,..., jn. Nếu τj1,...,jn được thực hiện trong một trạng thái mà trong đó nó không hiệu quả, thì giá trị của bất kỳ quan sát là không thay đổi. Tuy nhiên, tất cả chúng ta cần khai báo phương trình sau: ceq a(S, Xj1, ..., Xjn) = S if not c-a (S, Xj1, ..., Xjn) . Nếu giá trị của oi1, …, im không bị ảnh hưởng bằng cách thực hiện τj1,...,jn ở trạng thái bất kỳ (bất kể giá trị chân lý của cτj1,...,jn), phương trình sau đây được khai báo: eq o (a (S, Xj1 ... Xjn), Xi1 ... Xim) = o (S, Xi1, ..., Xim) . Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 17 4.3 Mô tả bài toán QLOCK Ta thấy rằng nhiều tiến trình (agents or processes) tranh quyền sử dụng một tài nguyên, nhưng tại một thời điểm chỉ có duy nhất một tiến trình có thể sử dụng tài nguyên. Vì thế mà tất cả các tiến trình phải tuân theo giao thức độc quyền truy xuất (mutual exclusion protocol) trong việc sử dụng tài nguyên. Trong đó QLOCK là một hệ thống sử dụng giao thức độc quyền truy xuất với một hàng đợi (Queue) dùng chung cho tất cả các tiến trình (processes) thỏa mãn các yêu cầu sau: Độc quyền truy xuất: Nếu tiến trình Pi đang trong miền găng (critical section) thì không tiến trình nào được sử dụng miền găng. Tiến trình: Nếu không có tiến trình nào ở trong miền găng và có một số tiến trình muốn vào miền gắng thì một tiến trình nào đó phải được vào miền găng. Trạng thái ban đầu: Mọi tiến trình là ở miền dư, và hàng đợi là rỗng. 4.4 Đặc tả QLOCK với OTS Có thể vắn tắt bài toán QLOCK dưới dạng thuật toán (Hình 4.1) trong đó: - Queue là hàng đợi chứa các định danh (i) của các tiến trình và được khởi tạo rỗng. - Mọi tiến trình được khởi tạo với nhãn ban đầu là l1. - put, top, get là các phương thức của hàng đợi (Queue). Hình 4.1: Thuật toán của bài toán QLOCK. Chúng ta sẽ tạo hàng đợi QUEUE với kiểu khai báo tổng quát (generic): Loop: l1: put(Queue, i) l2: repeat until top(Queue) = i Critical section cs: get(Queue) Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 18 Để khai báo hàng đợi tổng quát và định nghĩa cho phương thức “top” trong QUEUE trước hết chúng ta tạo 2 mô đun (Hình 4.2) trong đó: Mô đun EQTRIV thể hiện các phần tư khai báo tổng quát và mô đun OPTION nhằm tiền định nghĩa cho phương thức “top” trong QUEUE. Khi một hàng đợi rỗng thì phương thức “top” sẽ trả về hằng số none ngược lại sẽ trả về some(E) (Trong đó E chính là phần tử ở đỉnh hàng đợi). Hình 4.2: Kiểu biến tổng quát cho hàng đợi QUEUE. Trong bài toán QLOCK chúng ta phải sử dụng một hàng đợi để thực hiện phương thức độc quyền truy xuất cho cả hệ thống. Việc tạo ra một hàng đợi với các thuộc tính và phương thức cơ bản của một hàng đợi như chúng ta đã biết, gồm các phương thức put đưa một thành phần vào hàng đợi, phương thức get xóa một thành phần ra khỏi hàng đợi và top lấy ra một thành phần trên đỉnh của hàng đợi. Các thuộc tính và những phương thức cơ bản đó được định nghĩa trong CafeOBJ như Hình 4.3. Mô đun QUEUE chính là đặc tả cho hàng đợi trong hệ thống QLOCK. mod* EQTRIV{ [Elt] op _=_ : Elt Elt -> Bool {comm} } mod! OPTION(X :: EQTRIV){ [Option] op none : -> Option op some : Elt.X -> Option op val : Option -> Elt.X op _=_ : Option Opton -> Bool {comm} var O : Option vars E E’ : Elt.X eq val(some(E)) = E . eq (O = O) = true . eq (none = some(E)) = false . } Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 19 Hình 4.3: Hàng đợi QUEUE cho bài toán QLOCK. QLOCK sẽ được đặc tả như một OTS với các thành phần: - Hai hàm queue và pc o queue(s) trả về hàng đợi các định danh của tiến trình ở trang thái s o pc(s,i) trả về nhãn (l1, l2 hay cs) của tiến trình i ở trạng thái s. - Khởi tạo với trạng thái ban đầu (init) o queue(init) trả về empty o pc(init, i) trả về nhãn l1 với mọi tiến trình i. - Với 3 hành động want, try, exit o want(s,i) đưa về trạng thái tiếp theo sau khi thực hiện tiến trình i với nhãn l1 ở trạng thái s. o try(s,i) đưa về trạng thái tiếp theo sau khi thực hiện lặp lại tiến trình i với nhẵn l2 ở trạng thái s. Nếu i có nhẵn l2 và top(queue(s) là i, thì nhẵn của i ở trạng thái tiếp theo sẽ là cs. mod! QUEUE(D :: EQTRIV) { pr(OPTION(X <= D) [Queue] -- Khai báo kiểu Queue op empty : -> Queue -- Hằng số rỗng op _,_ : Elt.D Queue -> Queue -- Nối một phần tử vào Queue op put : Queue Elt.D -> Queue -- hàm put op get: Queue -> Queue -- hàm get op top : Queu -> Option -- hàm top var Q : Queue vars X Y : Elt.D eq put (empty, X) = X , empty . eq put((Y,Q),X) = Y , put(Q,X) . eq get(empty) = empty . eq get((X,Q)) = Q . eq top(empty) = none . eq top((X,Q)) = some(X) . eq empty?(empty) = true . --empty? là kiểu ngoại lệ của empty[1] eq empty?((X,Q)) = false . } Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 20 o exit(s,i) đưa về trạng thái tiếp theo sau khi thực hiện tiến trình i với nhãn cs ở trạng thái s. - Chúng ta sẽ có đặc tả (signature) hệ thống như hình 4.4. Hình 4.4: Đặc tả (signature) cho hệ thống QLOCK. - Phương trình được định nghĩa cho hành động try như hình 4.5. Hình 4.5: Hành động try trong hệ thống QLOCK. - Các phương trình định nghĩa cho các hành động khác hoàn toàn tương tự -- Điều kiện xẩy ra try op c-try : Sys Pid -> Bool {strat: (0 1 2)} eq c-try(S,I) = (pc(S,I) = l2 and top(queue(S)) = some(I) ) . -- Thực hiện chuyển tiếp trạng thái ceq pc(try(S,I),J) = (if I = J then cs else pc(S,J) fi) if c-try(S,I) . *[Sys]* -- trạng thái ban đầu op init : -> Sys -- các hàm bop pc : Sys Pid -> Label bop queue : Sys -> Queue -- các hành động bop want : Sys Pid -> Sys bop try : Sys Pid -> Sys bop exit : Sys Pid -> Sys Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 21 4.5 Đặc tả thuộc tính và kiểm chứng đặc tả Chúng ta sẽ tạo ra 2 mô đun INV và ISTEP (Hình 4.6) sử dụng để kiểm chứng tính chất độc quyền truy xuất của đặc tả được nêu như trên: Hình 4.6: Mô đun INV và ISTEP dùng để kiểm chứng. Với mỗi tiến trình bất kỳ k chúng ta sẽ chứng minh tính độc quyền truy xuất có thỏa mãn với 3 hành động want, try và exit, Trong khóa luận này chỉ trình bày kiểm chứng về try còn want và exit hoàn toàn tương tự. - Với tiến trình k bất kỳ sẽ có 4 trường hợp xảy ra so với i và j (i và j là hai tiến trình được khai báo ở trên): o Trường hợp k = i, k = j (1) o Trường hợp k # i, k# j (2) o Trường hợp k = i, k # j (3) o Trường hợp k # i, k # j (4) - Với trường hợp (1) chúng ta sẽ kiểm chứng như hình 4.7: mod INV{ pr(QLOCK) ops i j : -> Pid op inv1 : Sys Pid Pid -> Bool var S : Sys vars I J : Pid -- sử dụng để chứng minh cho trường hợp cụ thể eq inv1 (S,I,J) = (pc(S,I) = cs and pc(S,J) = cs implies I = J) . } mod ISTEP{ ops s s’ : -> Sys op istep1 : Pid Pid -> Bool vars I J : Pid -- sử dụng để chứng minh cho trường hợp tổng quát eq istep1(I,J) = inv1(s,I,J) implies inv1(s’,I,J) . } Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 22 Hình 4.7: Kiểm chứng với trường hợp (1). Sau khi thực hiện như trên (Hình 4.7) kết quả trả về là true, vậy trường hợp này thỏa mãn. - Với trường hợp (2) chúng ta sẽ kiểm chứng như hình 4.8. Hình 4.8: Kiểm chứng với trường hợp (2). open ISTEP op k : -> Pid . -- Điều kiện của try eq pc(s,k) = l2 . eq top(queue(s)) = some(k) . -- trường hợp I = k và j # k eq i = k . eq (j = k) = false . -- trạng thái chuyển tiếp eq s’ = try(s,k) . -- kiểm chứng tính đúng đắn red istep1(i, j) . close open ISTEP op k : -> Pid . -- Điều kiện của try eq pc(s,k) = l2 . eq top(queue(s)) = some(k) . -- trường hợp I = k và j = k eq i = k . eq j = k . -- trạng thái chuyển tiếp eq s’ = try(s,k) . -- kiểm chứng tính đúng đắn red istep1(i, j) . close Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng 23 o Sau khi thực hiện (Hình 3.8) sẽ trả về (pc(s,j) = cs) xor true. Chúng ta thấy có hai trường hợp xảy ra:  pc(s,j) = cs là true.  pc(s,j) = cs là false. o Nếu như pc(s,j) = cs là true thì sẽ không thỏa mãn với bài toán, chúng ta thấy một bổ đề đúng đắn:  eq inv2(S,I) = (pc(S,I) = cs implies top(queue(S)) = some(I)) .  Với bổ đề này thêm vào tính chất bất biến của module INV (Hình 3.6). Kiểm chứng lại tính đúng đắn: Hình 4.9: Kiểm chứng với bổ đề. Trả về giá trị true, mặt khác với bổ đề trên thì inv2(s, j) = true từ đó chúng ta suy ra được rằng istep1(i, j) = true vậy thỏa mãn. - Với trường hợp (3) hoàn toàn tương tự trường hợp (2) chúng ta có thỏa mãn. - Với trường hợp (4) hoàn toàn tương tự trường hợp (1) chúng ta có thỏa mãn. Vậy đặc tả đã được kiểm chứng thỏa mãn điều kiện bài toán đã cho. -- Kiểm chứng lại với bổ đề red inv2(s, j) implies istep1(i, j) . Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 24 Chương 5 Đặc tả và kiểm chứng hệ thống lò vi sóng 5.1 Hệ thống lò vi sóng 5.1.1 Mô tả hệ thống Để nấu thức ăn trong lò vi sóng, chúng ta phải mở cửa lò, rồi đặt thức ăn vào trong lò và đóng cửa lại. Không được đặt các vật chứa trong lò vi sóng. Sau đó bật nút start-up. Lò sẽ đun nóng khoảng 30 giây, và sau đó nó sẽ bắt đầu nấu. Khi nấu xong, lò sẽ tắt. Và Lò sẽ tắt bất cứ khi nào mà chúng ta mở cửa trong lúc lò đang hoạt động. Nếu chúng ta khởi động lò vi sóng trong lúc cửa lò đang mở, thì lỗi sẽ xảy ra và khi đó lò sẽ ko được đun nóng. Trong trường hợp này nút khởi động có thể sẽ được sử dụng để khởi động lại hệ thống lò vi sóng. Từ nguyên lý hoạt động của lò vi sóng như trên, chúng ta sẽ có mô đun của hệ thống lò vi sóng được đặc tả như là cấu trúc Kripke trong Hình 5.1. Để cho rõ ràng hơn chúng ta xem hệ thống bao gồm 7 trạng thái hay S= {S1, S2, S3, S4, S5, S6, S7} chính là các trạng thái của hệ thống. Mỗi trạng thái được gán với nhãn như trên với hai mệnh đề nguyên tử. Đó là đúng (true) trong trạng thái và phủ định của mỗi mệnh đề đó là sai (false) trong trạng thái. Các nhãn ở mỗi vòng trong của các trạng thái trên Hình 5.1 chỉ ra các hành động, các hành động này chính là nguyên nhân dẫn đến sự dịch chuyển của hệ thống lò vi sóng. Xem trạng thái S1 là trạng thái khởi tạo, đó là lúc cửa của lò được mở và lò vi sóng không hoạt động. Sau đó người dùng đóng cửa, thì hệ thống từ trạng thái S1 chuyển sang trạng thái S3. Tại thời điểm này, nếu người dùng ấn nút khởi động (start- up), thì lò vi sóng sẽ bắt đầu hoạt động và hệ thống chuyển đến trạng thái S6. Lò sẽ tự động làm nóng trong vòng 30 giây trước khi hệ thống chuyển đến trạng thái S7, và sau đó lò sẽ bắt đầu nấu trước khi hệ thống chuyển đến trạng thái S4. Sau khi lò vi sóng nấu xong, hệ thống sẽ chuyển từ trạng thái S4 về trạng thái S3. Như chúng ta đã thấy được lò vi sóng sẽ không hoạt động trước khi người dùng chưa đóng cửa lò, bởi vì nó sẽ rất nguy hiểm. Tuy nhiên nếu người dùng ấn nút khởi động (start-up) trước khi người dùng đống cửa lò, lỗi hệ thống sẽ xảy ra và lò vi sóng sẽ không làm việc và hệ thống sẽ chuyển đến trạng thái S2. Chỉ có sau khi người dùng đóng cửa và ấn nút khởi Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 25 động lại (reset), hệ thống sẽ chuyển tới trạng thái S3 và ở trạng thái này lò vi sóng sẽ bắt đầu hoạt động chỉ sau khi chúng ta ấn nut khởi động (start-up). Và sau khi chúng ta mở cửa lò, hệ thống sẽ chuyển từ trạng thái S4 về trạng thái S1. Hình 5.1: Cấu trúc Kripke của Lò vi sóng [1]. ~Start ~Close ~Heat ~Error Start ~Close ~Heat Error ~Start Close ~Heat ~Error ~Start Close Heat ~Error Start Close ~Heat Error Start Close ~Heat ~Error Start Close Heat ~Error S1 S2 S3 S4 S5 S6 S7 start open close open cooking done open close reset cook warm start Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 26 5.1.2 Mô tả các thuộc tính Chúng ta cần phải kiểm chứng rằng mô hình được mô tả của hệ thống lò vi sóng thỏa mãn với các thuộc tính sau: Thuộc tính 1: Tất cả các trạng thái của hệ thống lò vi sóng, nếu cửa lò đóng, nút khởi tạo (start-up) chưa được ấn và thức ăn sẽ không được đun nóng (chúng ta gọi trạng thái này như trạng thái bắt đầu) sau đó lò vi sóng sẽ nấu sau khi chúng ta ấn nút khởi tạo (start-up). Và sau khi nấu xong hệ thống sẽ quay trở lại về trạng thái bắt đầu. Thuộc tính 2: Với tất cả các trạng thái của hệ thống, nếu cửa lò được đóng, nút khởi động (start-up) được bật, thức ăn không được đun nóng và không có lỗi xảy ra thì lò vi sóng sẽ bắt đầu nấu ngày lập tức hay thức ăn sẽ được làm nóng. Thuộc tính 3: Với tất cả các trạng thái của hệ thống, nếu cửa lò được đóng, nút khởi động (start-up) được ấn nhưng có lỗi xảy ra thì hệ thống sẽ không hoạt động. Thuộc tính 4: Với tất cả các trạng thái của hệ thống, nếu cửa lò được đóng, nút khởi động (start-up) được bật, thức ăn chưa chưa được làm nóng nhưng có lỗi xảy ra thì lò vi sóng sẽ nấu sau khi bật nút khởi động lại (reset) và nút khởi động (start-up). Và sau khi nấu, hệ thống sẽ quay trở về trạng thái sau khi nút khởi động lại được bật (reset). Thuộc tính 5: Với tất cả các trạng thái của hệ thống, nếu cửa lò không được đóng sau đó hệ thống sẽ không làm việc và lỗi sẽ xảy ra nếu chúng ta bật nút khởi động (start-up). 5.2 Mô hình hóa hệ thống trong OTS/CafeObj 5.2.1 Mô hình hóa và mô tả hệ thống trong OTS Với việc mô hình hóa hệ thống lò vi sóng trong hệ thống chuyển dịch tổng quan (OTS). Sau đây chúng ta sẽ mô tả chi tiêt hơn các kiểu khai báo trong CafeOBJ: Sys: Kiểu (sort) thể hiện không gian trạng thái của hệ thống. Label: Kiểu thể hiện nhãn cho mỗi trạng thái; ví dụ như: st, cl, he, err… Bool: Kiểu lập luận true hoặc false được xây dựng trong mô đun BOOL trong ngôn ngữ CafeOBJ. Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 27 Hình 5.2: Mô hình của lò vi sóng. lb: toán tử trực quan (observer) nhằm kiểm tra trạng thái tương ứng với các nhãn của nó trọng hệ thống. warm: Một hành động của việc làm ấm lên bên trong lò vi sóng tự động sau khi người dùng bật nút khởi động (start-up). cook: Là một hành động của việc nấu thức ăn tự động sau khi làm ấm lò vi sóng. done: Là một hành động được hoàn thành quá trình nấu. open: Là một hành động của việc mở cửa lò vi sóng. close: Là một hành động của việc đống của lò vi sóng. start: Là một hành động của việc bắt đầu khởi động là ví sóng sau khi người dùng bật nút khởi động. reset: Là một hành động của việc khởi động lại lò vi sóng khi xảy ra lỗi. done warm = reset start close lb Sys open cooking close start S1 S2 S3 S4 S5 S6 S7 open close done open reset cook warm start User Label open Bool init cook Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 28 5.2.2 Đặc tả hình thức hệ thống trong CafeObj Từ mô hình lò vi sóng (Hình 5.2) chúng ta có thể đặc tả hệ thống trong CafeOBJ bằng mô đun MO với các thành phần được mô tả trong Hình 5.3. Trong đó, *[Sys]* là khai báo kiểu Sys chính là không gian trạng thái của hệ thống, bop lb là khai báo phương thức trực quan kiểm tra các hằng nhãn có thuộc trạng thái tương ứng hay không. Trong đó các hằng nhãn bao gồm st (start), cl (close), ht (heat), err (error) và các ký hiệu “~” trước nhãn ở trong trạng thái trong Hình 5.1 thể hiện nhãn đó không thuộc trạng thái. Hình 5.3: Đặc tả của lò vi sóng trong CafeOBJ. Trước khi đặc tả hê thống trong CafeOBJ bằng mô đun MO, ta tạo mô đun LABEL nhằm đặc tả cho các nhãn trong mỗi thái. Các nhãn này được xem như các hằng và chúng sẽ được kiểm tra các quan hệ giữa các nhãn bằng phương thức “_=_” được mô tra trong Hình 5.4. *[Sys]* -- không gian trạng thái của hệ thống [Label] -- Khai báo nhãn Label -- Khai báo toán tử trực quan bop lb : Sys Label -> Bool {memo} --Các hành động bop warm : Sys -> Sys bop cook : Sys -> Sys bop done : Sys -> Sys bop open : Sys -> Sys bop close : Sys -> Sys bop start : Sys -> Sys bop reset : Sys -> Sys Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 29 Hình 5.4: Mô đun LABEL trong CafeOBJ. Từ đó chúng ta sẽ đặc tả hệ thống trong CafeOBJ bằng mô đun MO với kế thừa một số thuộc tính và phương thức của mô đun LABEL và các hành động trong hệ thống sẽ được mô tả trong chương trình. 5.2.3 Không gian trạng thái của hệ thống đặc tả hình thức Với hệ thống Lò vi sống được mô tả bằng cấu trúc Kripke trong Hình 5.1, chúng ta sẽ thấy được sự dịch chuyển của hệ thống từ trạng thái này sang trạng thái khác bởi sự tác động của một trong các hành động {warm, cook, done, open, close, reset, start, }. Tập hợp tất cả các trạng thái đó chính là không gian trạng thái của hệ thống Lò vi sóng. Chúng được hình thức hóa với RMO là không gian trạng thái của hệ thống MO được đặc tả hình thức trong CafeObj. RMO được định nghĩa quy nạp như sau: Hình 5.5: Hình thức hóa không gian trạng thái của hệ thống. mod! LABEL { [LabelConst < Label] -- Khai báo các hằng thuộc Kiểu LabelConst ops st cl he err : -> LabelConst -- sư dụng phương thức _=_ nhằm -- định nghĩa các quan hệ giữa các nhãn st, cl, he, và err pr(EQL) vars Lc1 Lc2 : LabelConst eq (Lc1 = Lc2) = (Lc1 == Lc2) . } RMO = { init }  { warm(s) | s  RMO }  { cook(s) | s  RMO }  { done(s) | s  RMO }  { open(s) | s  RMO }  { close(s) | s  RMO }  { reset(s) | s  RMO } Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 30 5.2.4 Các thuộc tính được mô tả Từ các thuộc tính được mô tả bằng ngôn ngữ tự nhiên trong phần 5.1.2. Chúng ta sẽ đặc tả hình thức chúng trong ngôn ngữ CafeObj bằng mô đun INV, với sự thừa kế các thuộc tính và các phương thức của mô đun MO và các đặc tả thuộc tính được biểu diễn bởi các hàm trong CafeOBJ. Trong đó, inv1 là đặc tả của thuộc tính 1 trong hệ thống, inv2 là đặc tả của thuộc tính 2 trong hệ thống, inv3 là đặc tả của thuộc tính 3 trong hệ thống, inv4 là đặc tả của thuộc tính 4 trong hệ thống và inv5 là đặc tả của thuộc tính 5 trong hệ thống, với đầu vào là một trạng thái bất kỳ trong không gian trạng thái. Các hàm này sẽ kiểm tra tính đúng đắn của đặc tả hệ thống trong chương trình có thỏa mãn các thuộc tính đã được mô tả hay không. Việc triển khai này trong CafeOBJ sẽ được mô tả chi tiết trong Hình 5.7. Hình thức hóa của việc chứng minh cho các thuộc tính được đặc tả sẽ được mô tả bằng công thức toán học như sau: Hình 5.6: Hình thức hóa các thuộc tính. INV1 |= sRMO. inv1(s) INV2 |= sRMO. inv2(s) INV3 |= sRMO. inv3(s) INV4 |= sRMO. inv4(s) INV5 |= sRMO. inv5(s) Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 31 Hình 5.7: Đặc tả các thuộc tính trong CafeOBJ. Để chứng minh cho các thuộc tính bất biến bằng phương pháp quy nạp trên không gian trạng thái RMO, chúng ta khai báo theo mô đun được gọi là ISTEP trong CafeOBJ như sau: mod INV { pr(MO) op s : -> Sys -- trạng thái bất kỳ trong không gian trạng thái -- Tên các thuộc tính biểu diễn trong CafeOBJ pred inv1 : Sys -- tương dương với khai báo : inv1 : Sys -> bool pred inv2 : Sys -- tương dương với khai báo : inv2 : Sys -> bool pred inv3 : Sys -- tương dương với khai báo : inv3 : Sys -> bool pred inv4 : Sys -- tương dương với khai báo : inv4 : Sys -> bool pred inv5 : Sys -- tương dương với khai báo : inv5 : Sys -> bool -- biến trong CafeOBJ vars S : Sys -- định nghĩa các thuộc tính -- inv1 -- cho thuộc tính 1 eq inv1(S) = (((lb(S,st) == false) and (lb(S,cl) == true) and (lb(S,he) == false)) implies (c-done(cook(warm(start(S)))) and S = done(cook(warm(start(S)))))) . -- inv2 -- cho thuộc tính 2 eq inv2(S) = (((lb(S,st) == true) and (lb(S,cl) == true) and (lb(S,he) == false) and (lb(S,err) == false)) implies (c-done(cook(warm(S))))) . -- inv3 -- cho thuộc tính 3 eq inv3(S) = (((lb(S,st) == true) and (lb(S,cl) == true) and (lb(S,err) == true)) implies ((not c-start1(S)) and (S = start(S)))) . -- inv4 -- cho thuộc tính 4 eq inv4(S) = (((lb(S,st) == true) and (lb(S,cl) == true) and (lb(S,he) == false) and (lb(S,err) == true)) implies (c-done(cook(warm(start(reset(S))))) and reset(S) = done(cook(warm(start(reset(S))))))) . -- inv5 -- cho thuộc tính 5 eq inv5(S) = ((lb(S,cl) == false) implies ((not c-start1(S)) and (lb(start(S),err) == true))) . } -- kết thúc module INV Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 32 Hình 5.8: Mô đun ISTEP trong CafeOBJ. mod ISTEP { pr(INV) -- một trạng thái tiếp theo sau trạng thái s op s' : -> Sys -- khai báo các công thức cơ bản để chứng minh pred istep1 : -- for inv1 pred istep2 : -- for inv2 pred istep3 : -- for inv3 pred istep4 : -- for inv4 pred istep5 : -- for inv5 -- các công thức cơ bản để chứng minh trường hợp quy nạp eq istep1 = inv1(s) implies inv1(s') . eq istep2 = inv2(s) implies inv2(s') . eq istep3 = inv3(s) implies inv3(s') . eq istep4 = inv4(s) implies inv4(s') . eq istep5 = inv5(s) implies inv5(s') . } -- kết thúc module ISTEP Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 33 5.3 Kiểm chứng bằng phương pháp quy nạp 5.3.1 Các bước quy nạp Các bước chứng minh bằng phương pháp quy nạp sử dụng để kiểm chứng các thuộc tính bất biến cho hệ thống lò vi sóng với các thuộc tính invI (I = 1, 2, 3, 4,5) như sau: 5.3.2 Kiểm chứng bằng phương pháp quy nạp trong CafeOBJ Chúng ta triển khai các bước quy nạp cho việc kiểm chứng các đặc tả được mô tả theo các bước kiểm chứng trong CafeOBJ. Khi chạy tất cả chúng trong CafeOBJ, tất cả sẽ trả về giá trị đúng (true). Điều đó có nghĩa là tât cả các thuộc tính thỏa mãn hệ thống. Từ đó chúng ta đã hoàn thành việc kiểm chứng các thuộc tính bất biến của hệ thống dựa trên các đặc tả hình thức trong CafeOBJ được mô tả chi tiết trong phần phụ lục A. 5.4. Kiểm chứng bằng phương pháp tìm kiếm trạng thái Kiểm chứng trong CafeOBJ bằng việc tìm kiếm (searching) [2], cho mỗi thuộc tính được mô tả, kỹ thuật này cố gắng để áp dụng sự dịch chuyển trạng thái có thể trong quy tắc dịch chuyển trạng thái trong hệ thống để tới trạng thái tiếp theo. Từ trạng thái khởi tạo init, nếu tât cả trạng thái đạt được thỏa mãn thuộc tính thì xem như thuộc tính đã được chứng minh. Tuy nhiên, có một vài tuần hoàn trong không gian trạng thái. Các tuần hoàn này làm cho việc kiểm chứng bằng phương pháp tìm kiếm sẽ dẫn đến -- Phần cơ sở  Kiểm tra các thuộc tính invI thỏa mãn với trạng thái khởi tạo init -- Phần quy nạp s là mộ trạng thái hệ thống, Chúng ta cho rằng thuộc tính invI thỏa mãn ở trạng thái s, chúng ta phải kiểm tra rằng thuộc tính đó có thỏa mãn với trạng thái tiếp theo của trạng thái s với các hành động của hệ thống sau:  open, close, start, reset, warm, cook, and done Nếu tất cả việc kiểm tra trên trả về giá trị đúng (true) thì việc kiểm chứng các thuộc tính bất biến của hệ thống hoàn thành. Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 34 vô hạn. Để giải quyết vấn đề này, chúng ta định nghĩa một phương thức sử dụng cho để kiểm tra hai trạng thái của hệ thống đó là “_=ob=_”. Phương thức này sử dụng để xác định một trạng thái tìm kiếm mới đã có sẵn cho việc tìm kiếm. Bằng cách này chúng ta sẽ bỏ qua các vòng tuần hoàn trong không gian trạng thái trong khi việc tìm kiếm nằm trong tiến trình. Quy tắc dịch chuyển trạng thái của hệ thống và phương thức trên được đặc tả trong CafeOBJ với mô đun MOTrans như sau: -- Đặc tả của module MOTrans mod! MOTrans { pr(MO) [ Config ] op : Sys -> Config . var S : Sys . -- sự chuyển đổi có thể trong quy tắc chuyển đổi ctrans [warm] : => if c-warm(S) . ctrans [cook] : => if c-cook(S) . ctrans [done] : => if c-done(S) . ctrans [open] : => if c-open(S) . ctrans [close] : => if c-close(S) . ctrans [start1] : => if c-start1(S) . ctrans [start2] : => if c-start2(S) . ctrans [reset] : => if c-reset(S) . -- vị từ sự dụng để xác định một trạngt thái mới đã được tìm kiếm pred _=ob=_ : Config Config {memo} . vars S1 S2 : Sys . eq ( =ob= ) = (S1 = S2) . } -- Kết thúc mô đun Hình 5.9: Mô đun MOTrans trong CafeOBJ Chương 5: Đặc tả và kiểm chứng hệ thống lò vi sóng Phạm Ngọc Thắng 35 Để kiểm chứng các thuộc tính được mô tả bằng phương pháp tìm kiếm trong CafeOBJ, mỗi thuộc tính được đặc tả riêng trong từng mô đun. Như vậy chúng ta có 5 mô đun tương ứng với 5 thuộc tính được mô tả trong hình 5.7. Với mỗi thuộc tính, từ trạng thái đầu init, nếu tất cả các trạng thái đạt được thỏa mãn thuộc tính thì xem như thuộc tính đã được chứng minh. Chúng ta sẽ chứng minh rằng không có một trạng thái nào trong không gian trạng thái là không thỏa mãn với từng thuộc tính. Khi chạy tất cả chúng trong CafeOBJ, tất cả kết quả trả về bởi CafeOBJ sẽ là “false”. Nghĩa là tất cả các thuộc tính thỏa mãn trong hệ thống. Chúng ta triển khai tiến trình kiểm chứng bằng phương pháp tìm kiếm để chứng minh cho 5 thuộc tính đã được mô tả trong phần phụ lục B. Phục lục Phạm Ngọc Thắng 36 Chương 6 Kết luận Chúng ta đã đặc tả và kiểm chứng hệ thống Lò vi sóng với năm thuộc tính đã được nêu. Cả hai kỹ thuật kiểm chứng là quy nạp và tìm kiếm (searching) trong CafeOBJ đã được áp dụng để chứng minh các thuộc tính của hệ thống thỏa mãn trong hệ thống được mô tả. Bởi vì mô hình hóa hệ thống trong bài toán này là một trạng thái hữu hạn, do vậy việc xử lý kiểm chứng bằng cách tìm kiếm là hiểu quả hơn việc kiểm chứng bằng phương pháp quy nạp. Tuy nhiên, kỹ thuật quy nạp sẽ hiệu quả hơn kỹ thuật tìm kiếm khi mô hình hệ thống là vô hạn. Việc viết các bộ chứng minh cho việc kiểm chứng bằng phương pháp quy nạp được mô trả trong phần 5.3 là rất đơn giản. Sau khi chạy các bộ chứng minh cho tất cả các thuộc tính trong mô đun CafeOBJ, tất cả chúng đều trả về giá trị “true” mà không cần bất kỳ một bổ đề (lemma) nào. Đây không có nghĩa là việc kiểm chứng hệ thống đó bằng phương pháp quy nạp trong CafeOBJ là đơn giản. Chúng ta rất may trong bài toán này bởi mô hình hệ thống là hữu hạn trạng thái. Cho một mô hình hệ thống vô hạn trạng thái, sẽ có rất nhiều trường hợp cho ra kết quả với giá trị không phải là “true”. Những trường hợp này sẽ trả về giá trị “true” với một vài bổ đề (lemmas). Việc tìm kiếm các bổ đề và chứng minh chúng là rất khó và cũng là việc thú vị. Trong trình huống này, sự ảnh hưởng của việc kiểm chứng bằng quy nạp sẽ được sử dụng. Và nó không được giải quyết bởi kỹ thuật kiểm chứng mô hình (model checking) . Viết bộ chứng minh cho việc kiểm chứng bởi phương pháp tìm kiếm các trạng thái được mô tả trong phần 5.4 là rất hiệu quả cho mô hình trạng thái hữu hạn. Trong khi đó việc sử dụng phương pháp tìm kiếm trong việc kiểm chứng cho mô hình trạng thái vô hạn, sẽ không tìm kiếm hết các trạng thái thỏa mãn với thuộc tính của hệ thống được nêu. Phục lục Phạm Ngọc Thắng 37 Phục lục A: kiểm chứng bằng quy nạp -- Đối với inv1 --> I cơ sở open INV red inv1(init) . --> init close --> II quy nạp --> 1 open(s) open ISTEP -- trạng thái tiếp theo eq s' = open(s) . -- kiểm chứng red istep1 . close --> 2 close(s) open ISTEP -- trạng thái tiếp theo eq s' = close(s) . -- kiểm chứng red istep1 . close --> 3 start(s) open ISTEP -- trạng thái tiếp theo eq s' = start(s) . -- kiểm tra red istep1 . close --> 4 reset(s) open ISTEP -- trạng thái tiếp theo eq s' = reset(s) . -- kiểm tra red istep1 . close --> 5 warm(s) open ISTEP -- trạng thái tiếp theo eq s' = warm(s) . red istep1 . -- kiểm tra close --> 6 cook(s) open ISTEP -- trạng thái tiếp theo eq s' = cook(s) . -- kiểm tra red istep1 . close --> 7 done(s) open ISTEP -- trạng thái tiếp theo eq s' = done(s) . -- kiểm tra red istep1 . close -- Khi chúng ta chạy trong CafeOBJ, tất cả đều trả về “true” Phục lục Phạm Ngọc Thắng 38 -- Đối với inv3 --> I bước cơ sở --> init open INV red inv3(init) . close --> II bước quy nạp --> 1 open(s) open ISTEP -- trạng thái tiếp theo eq s' = open(s) . -- kiểm tra red istep3 . close --> 2 close(s) open ISTEP -- trạng thái tiếp theo eq s' = close(s) . -- kiểm tra red istep3 . close --> 3 start(s) open ISTEP -- trạng thái tiếp theo eq s' = start(s) . -- kiểm tra red istep3 . close --> 4 reset(s) open ISTEP -- trạng thái tiếp theo eq s' = reset(s) . -- kiểm tra red istep3 . close --> 5 warm(s) open ISTEP -- trạng thái tiếp theo eq s' = warm(s) . -- kiểm tra red istep3 . close --> 6 cook(s) open ISTEP -- trạng thái tiếp theo eq s' = cook(s) . -- kiểm tra red istep3 . close --> 7 done(s) open ISTEP -- trạng thái tiếp theo eq s' = done(s) . -- kiểm tra red istep3 . close -- Khi chúng ta chạy trong CafeOBJ, tất cả đều trả về “true” -- Đối với inv2 --> I bước cở sở --> init open INV red inv2(init) . close --> II bước quy nạp --> 1 open(s) open ISTEP -- trạng thái tiếp theo eq s' = open(s) . -- kiểm tra red istep2 . close --> 2 close(s) open ISTEP -- trạng thái tiếp theo eq s' = close(s) . -- kiểm tra red istep2 . close --> 3 start(s) open ISTEP -- trạng thái tiếp theo eq s' = start(s) . -- kiểm tra red istep2 . close --> 4 reset(s) open ISTEP -- trạng thái tiếp theo eq s' = reset(s) . -- kiểm tra red istep2 . close --> 5 warm(s) open ISTEP -- trạng thái tiếp theo eq s' = warm(s) . -- kiểm tra red istep2 . close --> 6 cook(s) open ISTEP -- trạng thái tiếp theo eq s' = cook(s) . -- kiểm tra red istep2 . close --> 7 done(s) open ISTEP -- trạng thái tiếp theo eq s' = done(s) . -- kiểm tra red istep2 . close -- Khi chúng ta chạy trong CafeOBJ, tất cả đều trả về “true” Phục lục Phạm Ngọc Thắng 39 -- Đối với inv5 --> I bước cơ sở --> init open INV red inv5(init) . close --> II bước quy nạp --> 1 open(s) open ISTEP -- trạng thái tiếp theo eq s' = open(s) . -- kiểm tra red istep5 . close --> 2 close(s) open ISTEP -- trạng thái tiếp theo eq s' = close(s) . -- kiểm tra red istep5 . close --> 3 start(s) open ISTEP -- trạng thái tiếp theo eq s' = start(s) . -- kiểm tra red istep5 . close --> 4 reset(s) open ISTEP -- trạng thái tiếp theo eq s' = reset(s) . -- kiểm tra red istep5 . close --> 5 warm(s) open ISTEP -- trạng thái tiếp theo eq s' = warm(s) . -- kiểm tra red istep5 . close --> 6 cook(s) open ISTEP -- trạng thái tiếp theo eq s' = cook(s) . -- kiểm tra red istep5 . close --> 7 done(s) open ISTEP -- trạng thái tiếp theo eq s' = done(s) . -- kiểm tra red istep5 . close -- Khi chúng ta chạy trong CafeOBJ, tất cả đều trả về “true” -- Đối với inv4 --> I bước cơ sở --> init open INV red inv4(init) . close --> II bước quy nạp --> 1 open(s) open ISTEP -- trạng thái tiếp theo eq s' = open(s) . -- kiểm tra red istep4 . close --> 2 close(s) open ISTEP -- trạng thái tiêp theo eq s' = close(s) . -- kiểm tra red istep4 . close --> 3 start(s) open ISTEP -- trạng thái tiếp theo eq s' = start(s) . -- kiểm tra red istep4 . close --> 4 reset(s) open ISTEP -- trạng thái tiếp theo eq s' = reset(s) . -- kiểm tra red istep4 . close --> 5 warm(s) open ISTEP -- trạng thái tiếp theo eq s' = warm(s) . -- kiểm tra red istep4 . close --> 6 cook(s) open ISTEP -- trạng thái tiếp theo eq s' = cook(s) . -- kiểm tra red istep4 . close --> 7 done(s) open ISTEP -- trạng thái tiếp theo eq s' = done(s) . -- kiểm tra red istep4 . close -- Khi chúng ta chạy trong CafeOBJ, tất cả đều trả về “true” Phục lục Phạm Ngọc Thắng 40 Phục lục B: Kiểm chứng bằng searching open (MOTrans + INV1) -- Kiểm tra tính đúng đắn của thuộc tính inv1 red =(*,*)=>* suchThat (not inv1(S)) withStateEq (C1:Config =ob= C2:Config) . close CafeOBJ> open (MOTrans + INV1) -- opening module MOTrans + INV1.. done. %MOTrans + INV1> -- this is a proof that there is no counter examples for the property inv1 %MOTrans + INV1> red =(*,*)=>* suchThat (not inv1(S)) withStateEq (C1:Config =ob= C2:Config) . -- reduce in %MOTrans + INV1 : (() = ( * , * ) =>* () suchThat (not inv1(S)) withStateEq (C1 =ob= C2)):Bool ** No more possible transitions. (false):Bool (0.016 sec for parse, 2760 rewrites(0.187 sec), 4636 matches, 1855 memo hits) Phục lục Phạm Ngọc Thắng 41 open (MOTrans + INV2) -- Kiểm tra tính đúng đắn của thuộc tính inv2 red =(*,*)=>* suchThat (not inv2(S)) withStateEq (C1:Config =ob= C2:Config) . close CafeOBJ> open (MOTrans + INV2) -- opening module MOTrans + INV2.. done. %MOTrans + INV2> -- this is a proof that there is no counter examples for the property inv2 %MOTrans + INV2> red =(*,*)=>* suchThat (not inv2(S)) withStateEq (C1:Config =ob= C2:Config) . -- reduce in %MOTrans + INV2 : (() = ( * , * ) =>* () suchThat (not inv2(S)) withStateEq (C1 =ob= C2)):Bool ** No more possible transitions. (false):Bool (0.000 sec for parse, 2111 rewrites(0.125 sec), 3507 matches, 1544 memo hits) open (MOTrans + INV3) -- Kiểm tra tính đúng đắn của thuộc tính inv3 red =(*,*)=>* suchThat (not inv3(S)) withStateEq (C1:Config =ob= C2:Config) . close CafeOBJ> open (MOTrans + INV3) -- opening module MOTrans + INV3.. done. %MOTrans + INV3> -- this is a proof that there is no counter examples for the property inv3 %MOTrans + INV3> red =(*,*)=>* suchThat (not inv3(S)) withStateEq (C1:Config =ob= C2:Config) . -- reduce in %MOTrans + INV3 : (() = ( * , * ) =>* () suchThat (not inv3(S)) withStateEq (C1 =ob= C2)):Bool ** No more possible transitions. (false):Bool (0.000 sec for parse, 2084 rewrites(0.140 sec), 3504 matches, 1560 memo hits) Phục lục Phạm Ngọc Thắng 42 open (MOTrans + INV5) -- Kiểm tra tính đúng đắn của thuộc tính inv5 red =(*,*)=>* suchThat (not inv5(S)) withStateEq (C1:Config =ob= C2:Config) . close -- CafeOBJ’s output CafeOBJ> open (MOTrans + INV5) -- opening module MOTrans + INV5.. done. %MOTrans + INV5> -- this is a proof that there is no counter examples for the property inv5 %MOTrans + INV5> red =(*,*)=>* suchThat (not inv5(S)) withStateEq (C1:Config =ob= C2:Config) . -- reduce in %MOTrans + INV5 : (() = ( * , * ) =>* () suchThat (not inv5(S)) withStateEq (C1 =ob= C2)):Bool ** No more possible transitions. (false):Bool (0.000 sec for parse, 1972 rewrites(0.109 sec), 3350 matches, 1452 memo hits) open (MOTrans + INV4) -- Kiểm tra tính đúng đắn của thuộc tính inv4 red =(*,*)=>* suchThat (not inv4(S)) withStateEq (C1:Config =ob= C2:Config) . close CafeOBJ> open (MOTrans + INV4) -- opening module MOTrans + INV4.. done. %MOTrans + INV4> -- this is a proof that there is no counter examples for the property inv4 %MOTrans + INV4> red =(*,*)=>* suchThat (not inv4(S)) withStateEq (C1:Config =ob= C2:Config) . -- reduce in %MOTrans + INV4 : (() = ( * , * ) =>* () suchThat (not inv4(S)) withStateEq (C1 =ob= C2)):Bool ** No more possible transitions. (false):Bool (0.000 sec for parse, 3349 rewrites(0.140 sec), 5833 matches, 2064 memo hits) Tài liệu tham khảo Phạm Ngọc Thắng 43 Tài liệu tham khảo [1] Edmund M. Clarke, Jr. Orna Grumberg, Doron A. Peled, Model Checking. MIT Press, (1999). [2] Kokichi FUTATSUGI , Formal Method’s Lectures, [3] Kokichi FUTATSUGI, Specification and Verification of Highly Reliable Systems’s Lectures, [4] Kokichi FUTATSUGI, Verifying Specifications with Proof Scores in CafeOBJ, The 21st IEEE International Conference on Automated Software Engineering (ASE'06), 2006. [5] A.T. Nakagawa – T. Sawada – K. Futatsugi. “CafeOBJ User’s Manual”, 1999. [6] K. Ogata and K. Futatsugi. “Rewriting-Based Verification of Authentication. Protocols” , 2003. [7] K. L. McMillan. “The SMV system*”. [8] Kazuhiro Ogata and Kokichi Futatsugi. Proof scores in the OTS/CafeOBJ method. In Proc. Of The 6th IFIP WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2003). Springer, 2003. [9] K. Ogata and K. Futatsugi. Modeling and verification of distributed real-time systems based on CafeOBJ, in: ASE ’01 (2001). [10] K. Ogata and K. Futatsugi. Formal analysis of Suzuki Kasami distributed mutual exclusion algorithm. In: FMOODS 02 (2002). [11] K. Futatsugi and K. Ogata. Rewriting can verify distributed real-time system, in: Int’l Symposium on Rewriting, Proof, and Computation, 2001. [12] Diaconescu, R. and K. Futatsugi, Behavioural coherence in object-oriented algebraic specification, J.UCS 6 (2006). [13] CafeOBJ official homepage, [14] [15] [16] [17]