Khóa luận Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Phạm Ngọc Thắng
ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG
CafeOBJ
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
HÀ NỘI - 2010
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Phạm Ngọc Thắng
ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG
CafeOBJ
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
Cán bộ hướng dẫn: TS. Nguyễn Việt Hà
Cán bộ đồng hướng dẫn: ThS. Đặng Việt Dũng
HÀ NỘI - 2010
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ
Phạm Ngọc Thắng
Lời cảm ơn
Em xin bày tỏ lòng cảm ơn sâu sắc tới TS. Nguyễn Việt Hà và ThS. Đặng Việt
Dũng về sự hướng dẫn, chỉ bảo tận tình, cùng với những lời khuyên quý giá của thầy
trong quá trình em học tập cũng như thực hiện khóa luận.
Em xin gửi lời cảm ơn tới các thầy cô giảng dạy tại Đại học Công nghệ - Đại học
Quốc Gia Hà Nội đã trang bị cho em những kiến thức quý báu trong thời gian em học
tại trường. Đó cũng là tiền đề cơ sở để em có thể thực hiện được tốt khóa luận của
mình.
Em xin gửi lời cảm ơn tới các thầy các cô trong bộ môn Công nghệ phần mềm đã
tạo điều kiện cho em được làm việc ở trên bộ môn với đầy đủ trang thiết bị cho em học
tập và làm việc.
Cảm ơn bạn bè, người thân về sự động viên, giúp đỡ về mặt tinh thần cũng như
về mặt vật chất trong thời gian em thực hiện khóa luận này.
Hà nội, tháng 6 năm 2010
Sinh viên thực hiện
Phạm Ngọc Thắng
i
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ
Phạm Ngọc Thắng
Tóm tắt
Công nghệ thông tin hiện nay là một trong những ngành phát triển mạnh mẽ nói
chung, cùng với công nghệ phần mềm nói riêng. Nhằm tạo ra những sản phẩm phần
mềm đảm bảo chất lượng và tính chính xác cao. Nên việc đặc tả và kiểm chứng phần
mềm hết sức quan trọng trong nhiều lĩnh vực sử dụng phần mềm, đặc biệt là các ngành
công nghệ cao đòi hỏi sự chính xác cao của phần mềm. Trong khuôn khổ của một bài
luận văn tốt nghiệp em đi sâu vào phương pháp đặc tả và kiểm chứng phần mềm sử
dụng ngôn ngữ CafeOBJ và đặc biệt đã áp dụng phương pháp này cho một hệ thống lò
vi sóng. Cùng với việc học tập và nghiên cứu trong khi làm khóa luận tốt nghiệp để
được tiếp cận với thực tế em đã thu được một số kết quả nhất định. Thông qua đó,
cùng với kiến thức cơ sở khi ngồi trên ghế nhà trường, em đã tìm hiểu thêm về những
tiến bộ trong việc phát triển phần mềm trên thế giới nói chung và Việt Nam nói riêng.
ii
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ
Phạm Ngọc Thắng
Mục lục
Chương 1. Giới thiệu ........................................................................................................1
1.1 Đặt vấn đề...............................................................................................................1
1.2 Nội dung nghiên cứu của khóa luận.........................................................................1
1.3 Cấu trúc khóa luận...................................................................................................2
Chương 2. Phương pháp hình thức....................................................................................3
2.1 Phân loại .................................................................................................................3
2.2 Sử dụng...................................................................................................................4
2.2.1 Đặc tả hình thức................................................................................................4
2.2.2 Phát triển ..........................................................................................................5
2.2.3 Kiểm chứng ......................................................................................................5
2.2.3.1 Chứng minh của con người.........................................................................5
2.2.3.1 Chứng minh tự động...................................................................................6
Chương 3. Ngôn ngữ CafeOBJ .........................................................................................7
3.1 Giới thiệu................................................................................................................7
3.2 Đặc tả và kiểm chứng trong CafeOBJ......................................................................9
3.2.1 Ví dụ.................................................................................................................9
3.2.2 Đặc tả số tự nhiên ...........................................................................................10
3.2.3 Đặc tả thuộc tính.............................................................................................10
3.2.4 Kiểm chứng thuộc tính....................................................................................10
Chương 4. Khái quát về OTS và bài toán QLOCK..........................................................13
4.1 Giới thiệu về OTS .................................................................................................13
4.2 OTS (Observation transition system).....................................................................14
4.3 Mô tả bài toán QLOCK .........................................................................................17
iii
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ
Phạm Ngọc Thắng
4.4 Đặc tả QLOCK với OTS .......................................................................................17
4.5 Đặc tả thuộc tính và kiểm chứng đặc tả .................................................................21
Chương 5. Đặc tả và kiểm chứng hệ thống lò vi sóng .....................................................24
5.1 Hệ thống lò vi sóng ...............................................................................................24
5.1.1 Mô tả hệ thống................................................................................................24
5.1.2 Mô tả các thuộc tính........................................................................................26
5.2 Mô hình hóa hệ thống trong OTS/CafeObj ............................................................26
5.2.1 Mô hình hóa và mô tả hệ thống trong OTS......................................................26
5.2.2 Đặc tả hình thức hệ thống trong CafeObj ........................................................28
5.2.3 Không gian trạng thái của hệ thống đặc tả hình thức.......................................29
5.2.4 Các thuộc tính được mô tả ..............................................................................29
5.3 Kiểm chứng bằng phương pháp quy nạp................................................................33
5.3.1 Các bước quy nạp ...........................................................................................33
5.3.2 Kiểm chứng bằng phương pháp quy nạp trong CafeOBJ.................................33
5.4. Kiểm chứng bằng phương pháp tìm kiếm trạng thái .............................................33
Chương 6. Kết luận.........................................................................................................36
iv
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ
Phạm Ngọc Thắng
Danh mục hình vẽ
Hình 3.1: Mô đun EXAMPLE trong CafeOBJ. .................................................................8
Hình 3.2: Đặc tả của module PNAT cho ví dụ. .................................................................9
Hình 3.3: Đặc tả thuộc tính cho điều kiện (*)..................................................................10
Hình 3.4: Kiểm chứng quy nạp với module ISTEP. ........................................................11
Hình 3.5: Kiểm chứng quy nạp cho đặc tả.......................................................................11
Hình 4.1: Thuật toán của bài toán QLOCK. ....................................................................17
Hình 4.2: Kiểu biến tổng quát cho hàng đợi QUEUE......................................................18
Hình 4.3: Hàng đợi QUEUE cho bài toán QLOCK.........................................................19
Hình 4.4: Đặc tả cho hệ thống QLOCK. .........................................................................20
Hình 4.5: Hành động try trong hệ thống QLOCK............................................................20
Hình 4.6: Mô đun INV và ISTEP dùng để kiểm chứng. ..................................................21
Hình 4.7: Kiểm chứng với trường hợp (1).......................................................................22
Hình 4.8: Kiểm chứng với trường hợp (2).......................................................................22
Hình 4.9: Kiểm chứng với bổ đề.....................................................................................23
Hình 5.1: Cấu trúc Kripke của Lò vi sóng [1]. ................................................................25
Hình 5.2: Mô hình của lò vi sóng....................................................................................27
Hình 5.3: Đặc tả của lò vi sóng trong CafeOBJ...............................................................28
Hình 5.4: Mô đun LABEL trong CafeOBJ......................................................................29
Hình 5.5: Hình thức hóa không gian trạng thái của hệ thống...........................................29
Hình 5.6: Hình thức hóa các thuộc tính...........................................................................30
Hình 5.7: Đặc tả các thuộc tính trong CafeOBJ...............................................................31
Hình 5.8: Mô đun ISTEP trong CafeOBJ........................................................................32
v
Chương 1: Giới thiệu
Phạm Ngọc Thắng
Chương 1
Giới thiệu
1.1 Đặ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 sử dụng phương pháp hình thức. Đối với các hệ thống
yêu cầu độ tin cậy cao như hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển
tên lửa, … Các phương pháp đặc tả và kiểm chứng hình thức sẽ được áp dụng cho
những hệ thống này trước khi triển khai chúng. Trong khi việc kiểm thử phần mềm
(software testing) 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 chứng có thể đảm bảo hệ
thống không có lỗi sau khi đã được kiểm chứng đúng đắn.
Hiện nay, đã có nhiều phương pháp và công cụ hỗ trợ cho việc đặc tả và kiểm
chứng phần mềm như OBJ [14], Maude [14], CafeOBJ [13], SPIN [15], SMV [17],
NuSMV [16], …. Mỗi phương pháp có những ưu và nhược điểm riêng và bị hạn chế
trong một số hệ thống nhất định.
Mục đích của khóa luận là tìm hiểu về phương pháp hình thức (formal method)
cũng như 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.
1.2 Nội dung nghiên cứu của khóa luậ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 lò
vi sóng sử dụng ngôn ngữ CafeOBJ. Đây là một trong hệ thống điển hình sẽ được trình
bày về quá trình mô hình hóa hệ thống giúp cho công việc viết đặc tả và kiểm chứng
các thuộc tính của chúng được đơn giản hơn. Nhằm kiểm chứng hệ thống một trong
những phương pháp chúng tôi quan tâm là viết đặc tả và kiểm chứng bằng CafeOBJ
1
Chương 1: Giới thiệu
Phạm Ngọc Thắng
theo tư tưởng quy nạp toán học, với phương pháp này chúng ta có thể đặc tả và kiểm
chứng các hệ thống vô hạn trạng thái một cách chính xác (trong khi với kiểm chứng
mô hình (model checking) chỉ kiểm chứng hữu hạn trạng thái của hệ thống). Ngoài ra
CafeOBJ còn hộ trợ sự kiểm chứng bằng phương pháp tìm kiếm (searching) không
gian trạng thái dành cho hệ thống hữu hạn trạng thái. Đặc tả cho kiểm chứng cùng với
đặc tả hệ thống và đặc tả thuộc tính sẽ được sử dụng để kiểm chứng hệ thống. Kết quả
của quá trình kiểm chứng sẽ cho chúng ta biết được đặc tả thỏa mãn thuộc tính cần
kiểm chứng hay không.
1.3 Cấu trúc khóa luận
Các phần còn lại của khóa luận có cấu trúc như sau:
Chương 2 trình bày lý thuyết về phương pháp hình thức, bao gồm các khái niệm
cơ bản, các kỹ thuật cơ bản được sử dụng trong đặc tả và kiểm chứng phần mềm.
Chương 3 trình bày 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.
Chương 4 trình bày phương pháp chuyển dịch hệ thống trực quan (Observation
transition system), một trong những phương pháp quan trọng nhằm đơn giản hóa việc
đặc tả và kiểm chứng phần mềm, kèm theo ví dụ về hệ thống QLOCK sử dung
OTS/CafeOBJ.
Chương 5 trình bày về “hệ thống Lò Vi Sóng” được đặc tả và kiểm chứng sử
dụng OTS/CafeOBJ, với hai phương pháp kiểm chứng khác nhau gồm quy nạp và tìm
kiếm (searching) các trạng thái.
Chương 6 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.
2
Chương 2: Phương pháp hình thức
Phạm Ngọc Thắng
Chương 2
Phương pháp hình thức
Trong ngành khoa học máy tính, phương pháp hình thức là các kỹ thuật toán học
cho việc đặc tả, phát triển và kiểm chứng các hệ thống phần mềm và phần cứng. Cách
tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng
hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay
an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống
sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của
quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được
sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.
2.1 Phân loại
Các phương pháp hình thức có thể được sử dụng tại nhiều mức:
Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được
phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này
có thể là lựa chọn hiệu quả nhất về mặt chi phí.
Mức 1: Sử dụng phát triển và kiểm chứng hình thức để tạo ra một chương trình
theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính
chất hoặc quá trình tinh chỉnh từ đặc tả hình thức tới một chương trình. Đây có thể là
lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí
vè an toàn và an ninh.
Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các
chứng minh hình thức hoàn toàn và được kiểm chứng bằn máy móc. Việc này có thể
đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tổn cho các lỗi sai
là cực kỳ cao.
Cùng với ngữ nghĩa hình thức của ngôn ngữ lập trình, các phương pháp hình thức
có thể được phân loại tương đối như sau:
Ngữ nghĩa ký hiệu (Denotational semantics), trong đó ý nghĩa của một hệ thống
được biểu diễn bằng lý thuyết toán học về miền xác định. Lợi điểm của những phương
pháp này phụ thuộc vào bản chất được hiểu rõ của các miền xác định để từ đó đem lại
3
Chương 2: Phương pháp hình thức
Phạm Ngọc Thắng
ý nghĩa cho hệ thống; các phê phán chỉ ra rằng không phải hệ thống nào cũng có thể
được nhìn một cách tự nhiên hoặc trực quan dưới dạng một hàm số.
Ngữ nghĩa hoạt động (Operational semantics), trong đó, ý nghĩa của một hệ
thống được biểu diễn bằng một chuổi các hành động của một mô hình tính toán (giả
thiết là) đơn giản hơn. Lợi điểm của phương pháp này là tính đơn giản của các mô
hình tạo nên sự trong sáng của biểu diễn.
Ngữ nghĩa tiên đề (Axiomatic semantics), trong đó ý nghĩa của hệ thống được
biểu diễn theo các tiền điều kiện (precondition) và hậu điều kiện (postcondition), đây
lần lượt là các điều kiện phải được thỏa mãn tại các thời điểm trước và sau khi hệ
thống thực hiện một nhiệm vụ. Những người ủng hộ phương pháp này nói đến mối
quan hệ của nó với lôgic kinh điển; những người phê phán nói rằng những ngữ nghĩa
thuộc dạng này không thực sự mô tả xem hệ thống làm cái gì (chỉ là cái gì đúng trước
đó và sau đó).
2.2 Sử dụng
2.2.1 Đặc tả hình thức
Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát
triển, tại bất kỳ mức độ chi tiết nào mà ta muốn. Mô tả hình thức này có thể được sử
dụng để hướng dẫn các hoạt động phát triển tiếp theo; ngoài ra, nó có thể được sử
dụng để kiểm chứng xem các yêu cầu cho hệ thống đang được phát triển đã được đặc
tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong
báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô
tả cú pháp ngôn ngữ lập trình (sau này được đặt tên là Backus normal form hay
Backus-Naur form (BNF) (Dạng chuẩn tắc Backus)).
4
Chương 2: Phương pháp hình thức
Phạm Ngọc Thắng
2.2.2 Phát triển
Khi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng
làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện
thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:
Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ
thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy
được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp
cho việc dịch thẳng mã chạy được.
Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện
của đặc tả có thể trở thành các khẳng định trong mã chạy được.
2.2.3 Kiểm chứng
Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ
sở cho việc chứng minh các tính chất của đặc tả.
2.2.3.1 Chứng minh của con người
Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không
phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về
hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức chứng minh toán
học: viết tay hoặc đánh máy nội dung bằng ngôn ngữ tự nhiên, với mức độ phi hình
thức như các chứng minh toán học thông thường mà con người vẫn thực hiện. Một
chứng minh tốt là một chứng minh mà những người khác có thể đọc được và hiểu
được. Các phê phán đối với cách tiếp cận này nói rằng tính đa nghĩa cố hữu trong ngôn
ngữ tự nhiên cho phép các lỗi sai trong các chứng minh đó có thể không bị phát hiện;
nhiều khi, những lỗi tinh vi có thể xuất hiện trong các chi tiết mức thấp mà thường
không được để ý đến bởi những chứng minh thuộc kiểu này. Ngoài ra, việc tạo ra các
chứng minh tốt đòi hỏi trình độ toán học cao.
5
Chương 2: Phương pháp hình thức
2.2.3.1 Chứng minh tự động
Phạm Ngọc Thắng
Ngược lại, ngày càng có nhiều quan tâm đến các chứng minh về tính đúng đắn
của hệ thống bằng các phương tiện tự động. Các kỹ thuột tự động được phân thành hai
loại chính:
Chứng minh định lý tự động, trong đó, khi cho trước một mô tả về hệ thống,
một tập các tiên đề lôgic và một tập các quy tắc suy luận, một hệ thống sẽ cố gắng tự
xây dựng một chứng minh hình thức từ đầu.
Kiểm tra mô hình, trong đó, một hệ thống kiểm định các tính chất nhất định
bằng cách duyệt trong bộ tất cả các trạng thái mà trong thời gian chạy, hệ thống có thể
vào trạng thái đó.
Cả hai kỹ thuật trên đều hoạt động mà không cần đến sự hỗ trợ của con người.
Các bộ chứng minh định lý tự động thường yêu cầu định hướng xem các tính chất nào
là đáng quan tâm; các bộ kiểm tra mô hình có thể nhanh chóng sa lầy vào việc kiểm tra
hàng triệu trạng thái không đáng quan tâm nếu không được cho trước một mô hình đủ
trừu tượng.
Những người ủng hộ các hệ thống này cho rằng các kết quả của chúng có độ xác
tính toán học cao hơn các chứng minh của con người, do tất cả các chi tiết buồn tẻ đã
được kiểm định một cách có thuật toán. Việc huấn luyện cần thiết để có thể sự dụng
được các hệ thống này cũng ít hơn đòi hỏi cần thiết cho việc tạo ra các chứng minh
toán học tốt bằng tay. Nhờ đó, các kỹ thuật này có thể dùng được cho nhiều người hơn.
Những người phê phán cho rằng các hệ thống kiểu này giống như máy sấm
truyền: chúng đưa ra các tuyên bố về sự thật nhưng lại không đưa ra giải thích nào về
sự thực đó. Còn có cả vấn đề “kiểm định hệ kiểm định”; nếu chính chương trình tham
gia công tác kiểm định không được chứng minh là đúng, thì có thể có lý do để nghi
ngờ tính đúng đắn của các kết quả được tạo ra.
Bên cạnh các phê phán nội bộ nói trên, còn có các phê phán dành cho các
phương pháp hình thức. Với tầm phát triển hiện nay, các chứng minh về tính đúng đắn,
bằng tay hoặc bằng máy tính, đòi hỏi nhiều thời gian (và do đó cả tiền bạc) để được
tạo ra, với lợi ích hạn chế ngoài việc đảm bảo tính đúng đắn. Điều đó làm cho các
phương pháp hình thức thường chỉ được dùng trong các lĩnh vực thu được lợi ích từ
việc có được các chứng minh đó, hoặc sẽ gặp nguy hiểm nếu có lỗi không được phát
hiện.
6
Chương 3: Ngôn ngữ CafeOBJ
Phạm Ngọc Thắng
Chương 3.
Ngôn ngữ CafeOBJ
3.1 Giới thiệu
CafeOBJ [5] [13] 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 module < mod_id > mod_element*, trong đó < mod_id > là tên
của mô đun và mod_element là một thành phần của mô đun. Một thành phần của mô
đun có thể được khai báo import, khai báo một kiểu (sort), khai báo toán tử
(operation), khai báo biến, khai báo một phương trình (equation), hoặc khái báo sự
dịch chuyển (transition). 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
7
Chương 3: Ngôn ngữ CafeOBJ
Phạm Ngọc Thắng
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). Phần thứ 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.
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) .
}
}
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.
8
Chương 3: Ngôn ngữ CafeOBJ
Phạm Ngọc Thắng
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ỳ (*).
mod PNAT {
[Nat]
-- mô tả kiểu biến là số tự nhiên là Nat
-- hằng số 0
op 0 : -> Nat
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
-- phép so sánh 2 số tự nhiên
-- các biến dùng để đặc tả
op _=_ : Nat Nat -> Bool {comm}
vars X Y : Nat
-- 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) .
}
Hình 3.2: Đặc tả của module PNAT cho ví dụ.
9
Chương 3: Ngôn ngữ CafeOBJ
Phạm Ngọc Thắng
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 (*)).
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)) .
}
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
10
Chương 3: Ngôn ngữ CafeOBJ
Phạm Ngọc Thắng
đú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.
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) .
}
Hình 3.4: Kiểm chứng quy nạp với module ISTEP.
--> 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
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ệ
11
Chương 3: Ngôn ngữ CafeOBJ
Phạm Ngọc Thắng
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 (*).
12
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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.
13
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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 = <O, I, T> 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
14
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
…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:
15
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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) .
16
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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).
Loop:
l1: put(Queue, i)
l2: repeat until top(Queue) = i
Critical section
cs: get(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):
17
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
Để 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).
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 .
}
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.
18
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
mod! QUEUE(D :: EQTRIV) {
pr(OPTION(X <= D)
[Queue]
-- Khai báo kiểu Queue
-- Hằng số rỗng
op empty : -> Queue
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
op top : Queu -> Option
-- hàm get
-- 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 .
}
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.
19
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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.
*[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
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.
-- Đ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) .
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ự
20
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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:
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) .
}
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:
21
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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
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.
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
Hình 4.8: Kiểm chứng với trường hợp (2).
22
Chương 4: Khái quát về OTS và bài toán QLOCK
Phạm Ngọc Thắng
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:
-- Kiểm chứng lại với bổ đề
red inv2(s, j) implies istep1(i, j) .
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.
23
Tải về để xem bản đầy đủ
50 trang
14/05/2025
140
Bạn đang xem 30 trang mẫu của tài liệu "Khóa luận Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ", để tải tài liệu gốc về máy hãy click vào nút Download ở trên.
File đính kèm:
- khoa_luan_dac_ta_va_kiem_chung_phan_mem_su_dung_cafeobj.pdf
