ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
ĐINH QUANG ĐẠT
NGHIÊN CỨU PHƯƠNG PHÁP KIỂM CHỨNG MÔ HÌNH
PHẦN MỀM DỰA TRÊN SAT
Ngành: Công nghệ thông tin
Chuyên ngành: Công nghệ phần mềm
Mã số: 60 48 10
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Nguyễn Trường Thắng
Hà Nội – 2013
Phụ lục 3:
2
Mục lục
Lời cam đoan
1
Mục lục
2
Danh mục các hình vẽ
4
Danh mục các ký hiệu và chữ viết tắt
5
1
7
Kiểm chứng mô hình
1.1 Giới thiệu về kiểm chứng mô hình . . . . . . . . . . . . . . . . . . . .7
1.1.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7
1.1.2 Kiểm định trong phần cứng và phần mềm . . . . . . . . . . . . .8
1.1.3 Kiểm chứng mô hình . . . . . . . . . . . . . . . . . . . . . . .9
1.1.4 Các tiến trình trong kiểm chứng mô hình . . . . . . . . . . . . 11
.
1.1.5 Mặt mạnh và mặt yếu của kiểm chứng mô hình . . . . . . . . . 12
.
1.2 Các kiến thức nền tảng . . . . . . . . . . . . . . . . . . . . . . . . . 13
.
1.2.1 Hệ thống dịch chuyển . . . . . . . . . . . . . . . . . . . . . . 13
.
1.2.2 Logic thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . 16
.
1.2.3 Logic thời gian tuyến tính (LTL) và logic tính toán cây (CTL) . 17
.
2 Vấn đề bùng nổ trạng thái và cách giải quyết sử dụng BDD
22
2.1 Vấn đề của bùng nổ trạng thái trong kiểm chứng mô hình . . . . . . . 22
.
2.2 Cách giải quyết theo hướng tiếp cận cổ điển . . . . . . . . . . . . . . 23
.
2.2.1 Thuật toán điểm cố định . . . . . . . . . . . . . . . . . . . . . 23
.
2.2.2 Kiểm chứng mô hình tương trưng với OBDDs . . . . . . . . . 25
.
3 Kiểm chứng mô hình giới hạn sử dụng bộ giải công cụ SAT
31
3.1 Các thuộc tính an toàn . . . . . . . . . . . . . . . . . . . . . . . . . 32
.
3.2 Giải công cụ SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
.
3
3.3 Xác định giới hạn . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
.
3.4 BMC cho các thuộc tính LTL . . . . . . . . . . . . . . . . . . . . . . 37
.
3.5 Giới thiệu về SMT . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
.
4 Ngôn ngữ SMV, công cụ NuSMV và thực nghiệm
43
4.1 Ngôn ngữ SMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
.
4.1.1 Kiểu dữ liệu trong SMV . . . . . . . . . . . . . . . . . . . . . 43
.
4.1.2 Phép toán trong SMV . . . . . . . . . . . . . . . . . . . . . . 44
.
4.2 Công cụ NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
.
4.3 Thực nghiệm sử dụng công cụ NuSMV . . . . . . . . . . . . . . . . 45
.
Kết luận
60
Tài liệu tham khảo
61
4
Danh sách hình vẽ
1.1 Tàu vũ trụ Ariane-5 vào tháng 4 năm 1996 . . . . . . . . . . . . . . . .8
1.2 Sơ đồ kiểm định hệ thống . . . . . . . . . . . . . . . . . . . . . . . . .9
1.3 Sơ đồ tổng quan hướng tiếp cận kiểm chứng mô hình . . . . . . . . . 11
.
1.4 Một hệ thống dịch chuyển T mà T |= FGp nhưng T ̸|= AFAGp. . . . 21
.
2.1 Minh họa cho việc tính toán EFp . . . . . . . . . . . . . . . . . . . 25
.
2.2 Minh họa OBDD cho công thức (w ∧ x) ∨ (y ∧ z) . . . . . . . . . . . 26
.
2.3 Xây dựng dạng chính tắc OBDD từ một công thức (w ∧ x) ∨ (y ∧ z) . 28
.
3.1 Một đường dẫn dạng lasso. . . . . . . . . . . . . . . . . . . . . . . . 38
.
3.2 Chuyển dịch của J f UgKik . . . . . . . . . . . . . . . . . . . . . . . . 40
.
3.3 Chuyển dịch của l J f UGKik với vòng lặp . . . . . . . . . . . . . . . . . 40
.
4.1 Biểu đồ lớp các yêu cầu của hệ thống thư viện . . . . . . . . . . . . . 46
.
4.2 Kiểm chứng một thuộc tính với BMC . . . . . . . . . . . . . . . . . 59
.
5
DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT
ICT
Information and communications technology
VHDL VHSIC Hardware Description Language
LTL
Linear Temporal Logic
CTL
Computation tree logic
PTL
Propositional Temporal Logic
BDD
Binary Decision Diagram
BMC
Bounded Model Checking
SAT
Boolean Satisfiability Problem
SMT
Satisfiability Modulo Theories
OBDD Ordered binary decision diagrams
DPLL
Davis Putnam Logemann Loveland
6
LỜI MỞ ĐẦU
Ngày nay, với tốc độ phát triển cực kỳ nhanh của lĩnh vực công nghệ thông tin
tại Việt Nam và trên thế giới, nhất là đối với phần mềm đã thâm nhập vào hầu hết
các lĩnh vực của đời sống như mua bán (mua hàng trực tuyến, các ứng dụng về kế
toán, quản lý, . . . ), các lĩnh vực ngân hàng (quản lý tài khoản, giao dịch trực tuyến,
. . . ), các lĩnh vực giải trí (trò chơi, phim ảnh, . . . ). Với sự bùng nổ về số lượng các
phần mềm thì việc đảm bảo về chất lượng đang là những yêu cầu cấp bách trong
hoàn cảnh hiện nay.
Trên thế giới đã có rất nhiều bài báo, đề tài, công trình nghiên cứu về kiểm chứng
mô hình, về các hướng khác nhau của kiểm chứng mô hình nhưng hướng nghiên
cứu tập trung vào giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm
chứng mô hình luôn luôn là đề tài mang lại nhiều tranh luận, cảm hứng cũng như
nghiên cứu nhất. Tác giả muốn nghiên cứu về vấn đề kiểm chứng mô hình liên
quan tới vấn đề bùng nổ không gian trạng thái của kiểm chứng mô hình với một
kỹ thuật mới nhất hiện nay đó là kiểm chứng mô hình giới hạn dựa trên SAT. Đồng
thời dựa trên các kết quả đã được nghiên cứu tìm hiểu, tác giả cũng cài đặt thực
nghiệm sử dụng kỹ thuật đã nghiên cứu, tìm hiểu.
Bố cục của luận văn bao gồm 4 chương :
• Chương 1: Giới thiệu về kiểm chứng mô hình và các kiến thức nền tảng của
kiểm chứng mô hình.
• Chương 2: Trình bày về vấn đề bùng nổ không gian trạng thái trong kiểm
chứng mô hình và cách giải quyết theo hướng tiếp cận cổ điển.
• Chương 3: Trình bày về SAT và cách giải bài toán bùng nổ không gian trạng
thái sử dụng kiểm chứng mô hình giới hạn dựa trên SAT.
• Chương 4: Trình bày về ngôn ngữ SMV, công cụ NuSMV và thực nghiêm sử
dụng NuSMV.
7
Chương 1
Kiểm chứng mô hình
1.1.
Giới thiệu về kiểm chứng mô hình
1.1.1. Giới thiệu
Độ tin cậy của chúng ta về các chức năng của các hệ thống ICT (Công nghệ
thông tin và truyền thông) tăng lên nhanh chóng. Những hệ thống này đang trở nên
phức tạp hơn và ngày càng chiếm một phần không thể thiếu trong cuộc sống hàng
ngày của chúng ta thông qua Internet và các loại hệ thống nhúng như thẻ thông
minh (smart cards), điện thoại di động, máy tính bảng, . . . Từ năm 1995, người ta
đã ước tính được rằng chúng ta sẽ phải làm việc với khoảng 25 thiết bị ICT trong
một ngày. Các dịch vụ như ngân hàng điện tử và mua sắm qua mạng đã trở thành
hiện thực. Dòng tiền hàng ngày thông qua Internet là khoảng 10 triệu đô la Mỹ.
Khoảng 20% chi phí phát triển các phương tiện giao thông hiện đại như xe hơi,
xe lửa tốc độ cao và máy báy được dành cho các hệ thống xử lý thông tin. Các
hệ thống thông tin phổ biến có mặt ở khắp mọi nơi. Các hệ thống thông tin điều
khiển thị trường chứng khoán, quan trọng với hệ thống Internet và quan trong đối
với các hệ thống trong y tế, . . . Độ tin cậy của các hệ thống thông tin có tầm quan
trọng trong xã hội. Với các lỗi xảy ra với các hệ thống có thể gây ra những tổn
thất rất nghiêm trọng. Một vài ví dụ mà chúng ta đã biết đến như các lỗi trong bộ
chia dấu phẩy động của Intel Pentium II trong đầu những năm 90 gây ra thiệt hại
khoảng 450 triệu đô la Mỹ để thay thế các bộ vi xử lý lỗi, và danh tiếng của Intel
cũng đã bị ảnh hưởng. Các lỗi phần mềm trong hệ thống xử lý hành lý đã làm trì
hoãn việc mở cửa sân bay Denver trong 9 tháng, mỗi ngày mất 1.1 triệu USD. Hai
mươi bốn giờ sau sự thất bại của hệ thống đặt vé trực tuyến của một công ty máy
bay lớn trên thế giới sẽ gây ra phá sản vì các đơn đặt hàng bị bỏ lỡ. Đối với một số
8
lỗi trong các hệ thống có thể gây ra thảm họa[3]. Một ví dụ điển hình là lỗi trong
phần mềm điều khiển của tàu vũ trụ Ariane-5 vào tháng 4 năm 1996, sau 36 giây
kể từ khi ra khỏi bệ phóng đã bị rơi chỉ do lỗi chuyển đổi số thực 32 bit sang số
nguyên 16 bit (hình 1.1).
Hình 1.1: Tàu vũ trụ Ariane-5 vào tháng 4 năm 1996
Tầm quan trọng cũng như sự phức tạp của hệ thống ICT tăng lên nhanh chóng.
Các hệ thống ICT không còn độc lập, mà được nhúng vào một hệ thống lớn, tương
tác và kết nối với các thành phần và hệ thống khác. Do đó, chúng trở nên dễ bị lỗi
- số các lỗi phát triển theo cấp số nhân đối với số các tương tác với các thành phần
hệ thống. Đặc biệt, tính tương tranh và tính không đơn định của mô hình tương
tác hệ thống lại khó xử lý với các kỹ thuật chuẩn. Độ phức tạp của hệ thống ICT
ngày càng tăng cùng với những áp lực làm cho thời gian phát triển hệ thống, điều
này đã làm cho việc cung cấp các hệ thống ICT với ít khuyết điểm là vô cùng khó
khăn và phức tạp.
1.1.2. Kiểm định trong phần cứng và phần mềm
Kỹ thuật kiểm định hệ thống đang được áp dụng để thiết kế các hệ thống ICT
có độ tin cậy cao. Nói chung, kiểm định hệ thống được sử dụng để xác minh xem
hệ thống có đạt được những đặc tính nhất định. Các đặc tính được kiểm chứng có
thể rất cơ bản, ví dụ, một hệ thống không nên đến được trạng thái mà ở đó tiến
trình không thể thực hiện (kịch bản của deadlock), và chủ yếu được lấy từ đặc tả
của hệ thống. Đặc tả này quy định những gì hệ thống phải làm và những gì không,
9
và do đó tạo nên cơ sở cho bất kỳ hoạt động kiểm định nào. Một khuyết điểm được
tìm thấy một khi hệ thống không đáp ứng được một trong các thuộc tính của đặc
tả. Hệ thống được xem xét là "đúng" khi hệ thống thỏa mãn tất cả các thuộc tính
lấy từ đặc tả của hệ thống. Vì vây, tính đúng đắn luôn luôn tương đối với đặc tả,
và không có một thuộc tính tuyết đối của hệ thống. Một sơ đồ của kiểm định được
mô tả trong hình 1.2.
Đặc tả hệ thống
(System
specification )
Thiết kế
(Design)
Thuộc tính
(Properties)
Sản phẩm/ bản thử
(Product/ Prototype)
Tìm thấy lỗi
Kiểm chứng
(Verification)
Không tìm
thấy lỗi
Hình 1.2: Sơ đồ kiểm định hệ thống
Từ đặc tả hệ thống được sử dụng để thiết kê và từ thiết kế đưa ra các sản phẩm,
bản thử. Đồng thời từ đặc tả hệ thống cũng đưa ra được các tính chất của hệ thống.
Sau đó, các tính chất và sản phẩm, bản thử sẽ được sử dụng để kiểm chứng. Kết
quả thu được có thể là tìm thấy lỗi hoặc không tìm thấy lỗi.
1.1.3. Kiểm chứng mô hình
Trong thiết kế phần mềm và phần cứng của các hệ thống phức tạp, nhiều thời
gian và công sức dành cho việc kiểm định hơn là việc xây dựng hệ thống. Các kỹ
thuật được tìm kiếm để giảm thiểu những nỗ lực kiểm định trong khi gia tăng độ
bao phủ. Các phương pháp hình thức đưa ra một triển vọng lớn để có thể tích hợp
kiểm chứng trong quá trình thiết kế, cung cấp các kỹ thuật kiểm chứng hiệu quả
hơn và giảm bớt thời gian kiểm chứng.
Kỹ thuật kiểm chứng dựa trên mô hình được dựa trên sự mô tả mô hình của các
hành vi có thể của hệ thông qua những công thức toán học rõ ràng và chính xác.
10
Hóa ra là, trước khi kiểm định bằng bất cứ hình thức nào, việc xây dựng mô hình
chính xác của các hệ thống thường dẫn đến việc phát hiện ra sự không đầy đủ,
không rõ ràng và không nhất quán trong đặc tả hệ thống. Những vấn đề như vậy
thường chỉ được phát hiện ra rất lâu sau giai đoạn thiết kế. Các mô hình cùng với
các thuật toán có thể khai thác tất cả các trạng thái của hệ thống. Điều này cung
cấp cơ bản cho một loạt các kỹ thuật kiểm chứng khác nhau, từ sự khám phá một
cách toàn diện mô hình (kiểm chứng mô hình) tới những thực nghiệm trên một
tập hợp các hạn chế của các kịch bản trong mô hình (mô phỏng), hoặc trong thực
tế (thử nghiệm). Do không ngừng cải tiến thuật toán và cấu trúc dữ liệu cùng với
sự phát triển mạnh mẽ của máy tính với tốc độ xử lý và bộ nhớ tăng lên một cách
đáng kể, kỹ thuật kiểm chứng dựa trên mô hình cách đây một thập kỷ chỉ áp dụng
với những ví dụ đơn giản thì bây giờ đã có thể áp dụng với những thiết kế thực tế.
Kiểm chứng mô hình là một kỹ thuật kiểm chứng xem xét tất cả các trạng thái
có thể của hệ thống theo cách vét cạn. Tương tự như chương trình chơi cờ của máy
tính kiểm tra những nước đi có thể, công cụ kiểm chứng giúp cho việc kiểm chứng
mô hình, xem xét tất cả các kịch bản hệ thống có thể xảy ra theo một cách có hệ
thống. Theo cách này, nó có thể chỉ ra rằng mô hình hệ thống thực sự thỏa mãn
với một đặc tính nhất định. Đó là một thách thức thật sự để kiểm tra không gian
rộng lớn các trạng thái có thể. Những công cụ kiểm chứng tốt nhất hiện tại có thể
xử lý không gian trạng thái khoảng 108 tới 109 trạng thái với không gian trạng thái
được liệt kê tường minh, sử dụng khéo léo thuật toán và cấu trúc dữ liệu phù hợp.
Một không gian các trạng thái lớn (1020 thậm chí lên tới 10476 trạng thái) có thể
được xử lý cho những vấn đề cụ thể. Thậm chí những lỗi tinh vi chưa được phát
hiện bằng mô phỏng, kiểm tra, và giả lập có thể bị lộ ra bằng cách sử dụng kiểm
chứng mô hình.
Mô hình hệ thống thường được sinh một cách tự động từ mô tả của hệ thống, và
mô tả của hệ thống được xác định trong một số ngôn ngữ chương trình giống như
C hoặc Java hoặc ngôn ngữ mô tả hệ thống như Verilog hoặc VHSIC Hardware
Description Language. Chú ý rằng, thuộc tính đặc tả quy định cái gì mà hệ thống
nên làm, và cái gì mà hệ thống không nên làm, trong khi đó, mô tả của hệ thống
xác định hệ thống hoạt động như thế nào? Công cụ kiểm chứng kiểm tra tất cả
các trạng thái có liên quan của hệ thống để kiểm tra xem chúng có thỏa mãn với
đặc tính mà bạn mong muốn hay không. Nếu trạng thái gặp phải là vi phạm đặc
tính đang xem xét, Công cụ kiểm chứng sẽ cung cấp một phản ví dụ cho thấy việc
11
làm thế nào mà mô hình có thể tới được trạng thái không mong muốn. Phản ví dụ
cũng mô tả một đường dẫn thực thi có thể dẫn tới từ những trạng thái khởi tạo của
hệ thống tới những trạng thái vi phạm thuộc tính đang được kiểm chứng. Với sự
giúp đỡ của mô phỏng, người sử dụng có thể xem lại các kịch bản vi phạm để có
được những thông tin gỡ lỗi có ích và tích hợp các mô hình phù hợp (xem hình 1.3).
Yều cầu
(Requirements)
Hệ thống
(System)
Hình thức hóa
(Formalizing )
Mô hình hóa
(Modeling )
Đặc tả thuộc tính
(Property specification )
Kiểm chứng mô hình
(Model checking )
Mô hình hệ thống
(System model )
Thỏa mãn
(satisfied )
Vi phạm, phản ví dụ
(Violated,
counterexample )
Mô phỏng
(Simulation)
Định vị lỗi
(Location error)
Hình 1.3: Sơ đồ tổng quan hướng tiếp cận kiểm chứng mô hình
Một hệ thống được mô hình hóa qua các trạng thái và các dịch chuyển thành
một mô hình hệ thống, các đặc tả yêu cầu được hình thức hóa qua logic thời gian
thành các đặc tả thuộc tính. Đây là hai đầu vào của kiểm chứng mô hình. Kiểm
chứng mô hình có thể đưa ra kết quả là thỏa mãn hoặc là vi phạm và có phản ví dụ
và có thể được mô phỏng nhờ mô hình hệ thống để định vị các lỗi.
1.1.4. Các tiến trình trong kiểm chứng mô hình
Trong việc áp dụng kiểm chứng mô hình để thiết kế các pha khác nhau như
sau: Pha Mô hình hóa giúp cho việc mô hình hóa hệ thống dưới sự xem xét bằng
cách sử dụng ngôn ngữ mô tả mô hình của công cụ kiểm chứng bằng tay. Kiểm tra
12
tính đúng đắn trước tiên và các đánh giá nhanh của mô hình để thực thi một vài
mô phỏng. Mô hình hóa các đặc tính để kiểm tra sử dụng ngôn đặc tả các thuộc
tính; Pha Thực thi chạy công cụ kiểm chứng để kiểm tra tính hợp lệ của thuộc tính
trong mô hình hệ thống. Pha Phân tích kiểm tra xem thuộc tính có an toàn hay
không? sau đó kiểm tra thuộc tính tiếp theo (nếu có thể); Thuộc tính có vi phạm
hay không? nếu có thì phân tích phản ví dụ được sinh ra từ mô phỏng, làm mịn mô
hình, thiết kế, và các thuộc tính và lặp lại toàn bộ thủ tục. Thoát ra khỏi bộ nhớ?
sau đó Cố gắng làm giảm mô hình và thử lại.
1.1.5. Mặt mạnh và mặt yếu của kiểm chứng mô hình
Kiểm chứng mô hình đã có rất nhiều ưu điểm tuy nhiên vẫn không thể tránh
khỏi được những khuyết điểm. Một số ưu điểm và khuyết điểm của kiểm chứng
mô hình có thể được thể hiện như sau. Về ưu điểm kiểm chứng mô hình hướng
tiếp cận chung có thể áp dụng với một phạm vi rộng lớn các ứng dụng như các hệ
thống nhúng, công nghệ phần mềm và thiết kế phần cứng. Kiểm chứng mô hình
hỗ trợ kiểm chứng từng phần, các thuộc tính có thể được kiểm tra riêng lẻ, do đó
cho phép tập trung vào những đặc tính quan trọng trước tiên. Không có đặc tả yêu
cầu nào trọn vẹn là cần thiết. Tìm ra các lỗi khó bị phát hiện, điều này trái ngược
với kiểm tra và mô phỏng nhằm mục đích tìm những khuyết điểm có thể xảy ra
nhất. Kiểm chứng mô hình cung cấp các chuẩn đoán về thông tin trong trường hợp
thuộc tính không có giá trị; điều này có ích trong việc hỗ trợ sửa lỗi. Việc sử dụng
kiểm chứng mô hình yêu cầu không cần mức độ cao về sự tương tác của người
dùng cũng không cần trình độ cao về chuyên môn. Kiểm chứng mô hình có được
sự quan tâm, thu hút tăng lên nhanh chóng bởi ngành công nghiệp; Kiểm chứng
mô hình có thể dễ dàng tích hợp trong vòng đời phát triển hiện có; Kiểm chứng
mô hình dựa trên một nền tảng toán học vững chắc; Các khuyết điểm của kiểm
chứng mô hình được thể hiện qua các điểm như sau, kiểm chứng mô hình chủ yếu
thích hợp với các ứng dụng chuyên về điều khiển và chưa phù hợp với các ứng
dụng chuyên về cơ sở dữ liệu. Các ứng dụng của kiểm chứng mô hình chinh phục
các vấn đề có thể giải được; đối với hệ thống vô hạn trạng thái hoặc luận lý về kiểu
dữ liệu trừu tượng (yêu các logic không giải được và giải được một nửa), kiểm
chứng mô hình nói chung là tính toán không hiệu quả. Kiểm chứng mô hình chủ
yếu kiểm chứng mô hình của hệ thống, và không kiểm chứng hệ thống thực sự (sản
phẩm hoặc bản nguyên mẫu); và kết quả thu được tốt là do mô hình hệ thống. Các
13
kỹ thuật bổ xung, như kiểm tra, cần được tìm những sai lầm hư cấu (đối với phần
cứng) hoặc những lỗi của mã nguồn (đối với phần mềm). Kiểm chứng mô hình chỉ
kiểm tra những trạng thái yêu cầu. Không có đảm bảo nào là kiểm tra được hết các
trạng thái. Các thuộc tính hợp lệ không được kiểm tra không thể được xem xét.
Kiểm chứng mô hình vướng phải vấn đề bùng nổ không gian trạng thái. Số lượng
các trạng thái cần của hệ thống thực có thể vượt quá bộ nhớ của máy tính. Cách sử
dụng của kiểm chứng mô hình đòi hỏi phải có một số chuyên gia trong việc trừu
tượng hóa hệ thống để có được mô hình hệ thống nhỏ hơn với ít thuộc tính trạng
thái hơn. Kiểm chứng mô hình không đảm bảo mang lại kết quả chính xác, với bất
kỳ công cụ nào, công cụ kiểm chứng mô hình có thể chứa các khiếm khuyết về
phần mềm. Kiểm chứng mô hình không cho phép kiểm tra một cách tổng quát.//
Mặc dù vẫn còn tồn tại những khuyết điểm như vậy nhưng kiểm chứng mô hình
vần là một kỹ thuật tiềm năng để phát hiện ra những lỗi trong phần cứng và phần
mềm. Tiếp theo luận văn sẽ đề cập đến các kiến thức nền tảng sẽ được sử dụng
trong kiểm chứng mô hình.
1.2.
Các kiến thức nền tảng
1.2.1. Hệ thống dịch chuyển
Hệ thống dịch chuyển thường được sử dụng trong khoa học máy tính như các
mô hình mô tả hành vi của hệ thống. Hệ thống dịch chuyển về cơ bản là các đồ
thị có hướng với các nút thể hiện các trạng thái, các cạnh mô hình cho các chuyển
dịch.
Định nghĩa 1.2.1. Hệ thống dịch chuyển [3]
Một hệ thống dịch chuyển TS là một bộ (S , Act, −→, I, AP, L) trong đó
• S là tập hợp các trạng thái,
• Act là tập hợp các hành động,
• −→⊆ S × Act × S là một quan hệ dịch chuyển,
• I ⊆ S là tập hợp các trạng thái khởi tạo,
• AP là tập hợp những mệnh đề nguyên tử, và
• L : S −→ 2AP là một nhãn của hàm.
14
T S được gọi là hữu hạn nếu S , Act, và AP là hữu hạn.
α
Viết s −→
− s′ thay cho (s, α, s′ ) ∈−→. Các hành động trực quan của hệ thống
dịch chuyển có thể được mô tả như sau: hệ thống dịch chuyển bắt đầu tại một số
trạng thái khởi tạo s0 ∈ I và tiến triển theo quan hệ dịch chuyển −→. Có nghĩa là,
α
nếu s là trạng thái hiện tại, sau đó một chuyển dịch s −→
− s′ bắt đầu từ s được chọn
không đơn định và thực hiện, nghĩa là hành động α đươc thực thi và hệ thống dịch
chuyển tiến triển từ trạng thái s tới trạng thái s′ . Thủ tục lựa chọn này được lặp đi
lặp lại trong trạng thái s′ và kết thúc ở trạng thái mà không dịch chuyển được nữa.
Nếu I là rỗng , thì hệ thống dịch chuyển không có hành vi nào và cũng không có
trạng thái khởi tạo nào được chọn lựa. Nhãn của hàm L quan hệ với tập L(s) ∈ 2AP
của các mệnh đề nguyên tử tới một vài trạng thái s. Cho Φ là một công thức logic
mệnh đề, s thỏa mãn công thức Φ nếu sự ước lượng cảm ứng bởi L(s) làm cho
công thức Φ true; nghĩa là:
s |= Φ ⇔ L(s) |= Φ.
Định nghĩa 1.2.2. Predecessors và Successors trực tiếp[3]
Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. Với s ∈ S và α ∈
Act, tập hợp của α − successors được định nghĩa như sau:
∪
α
Post(s, α) = {s′ ∈ S |s −→
− s′ }, Post(s) =
Post(s, α).
α∈Act
Tập hợp của α − predecessors được định nghĩa bằng:
∪
α
Pre(s, α) = {s′ ∈ S |s′ −→
− s}, Pre(s) =
Pre(s, α).
α∈Act
Mỗi trạng thái s′ ∈ Post(s, α) được gọi là α − successor trực tiếp của s. Theo
đó mỗi trạng thái s′ ∈ Post(s) được gọi là phần tử kế tiếp trực tiếp của s. Chú ý là
tập hợp các phần tử kế tiếp trực tiếp được mở rộng tới các tập con của S theo cách
hiển nhiên: cho C ⊆ S ,lấy
Post(C, α) =
∪
s∈C
Post(s, α), Post(C) =
∪
Post(s).
s∈C
Với Pre(C, α) và Pre(C) cũng được định nghĩa tương tự. Trạng thái kết thúc của
một hệ thống dịch chuyển T S là các trạng thái không có bất kỳ chuyển dịch đi ra
nào. Một khi hệ thống được mô tả bởi T S đạt được một trạng thái kết thúc, toàn
bộ hệ thống sẽ dừng lại.
15
Định nghĩa 1.2.3. Trạng thái dừng[3]
Trạng thái s trong hệ thống dịch chuyển T S gọi là dừng khi và chỉ khi Post(s) = ∅
Hệ thống dịch chuyển[3, 11? ] không đơn định được đề cập ở đây là cái cốt
yếu cho việc mô hình các hệ thống máy tính. Tuy nhiên, rất tiện lợi để xem xét hệ
thống với hành vi quan sát được là đơn định. Có hai hướng tiếp cận nói chung để
hình thức hóa các hành vi thấy được của hệ thống dịch chuyển: một hướng dựa vào
các hành động, một hướng dựa vào các nhãn của các trạng thái. Trong khi hướng
tiếp cận dựa vào hành vi cho rằng chỉ có các hành động thực thi có thể quan sát
từ bên ngoài, hướng tiếp cận dựa trên trạng thái bác bỏ hành động và dựa vào các
mệnh đề nguyên tử chứa trạng thái hiện thời có thể nhìn thấy. Các hệ thống dịch
chuyển đơn định theo quan điểm dựa vào hành vi có phần lớn có nhiều nhất một
nhãn dịch chuyển đi ra với hành động α cho mỗi trạng thái, trong khi các hệ thống
dịch chuyển đơn định theo quan điểm của các nhãn trạng thái, nghĩa là với bất kỳ
nhãn trạng thái A ∈ 2AP và bất kỳ trạng thái nào có nhiều nhất một dịch chuyển
đi ra dẫn tới một trạng thái với nhãn A. Trong cả hai quan điểm, đều yêu cầu có
nhiều nhất một trạng thái khởi tạo.
Định nghĩa 1.2.4. Hệ thống dịch chuyển đơn định[3]
Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển.
1. T S được gọi là action − deterministic (hành vi đơn định) nếu |I| ≤ 1 và
|Post(s, α)| ≤ 1 với tất cả các trạng thái s và các hành động α.
2. T S được gọi là AP − deterministic nếu |I| ≤ 1 và |Post(s) ∩ {s′ ∈ S |L(s′ ) =
A}| ≤ 1 với tất cả các trạng thái s và A ∈ 2AP .
Cho đến nay, hành vi của hệ thống dịch chuyển đã được mô tả ở mức trực quan,
và được hình thức hóa bằng cách sử dụng khái niệm executions (các sự thực thi).
Một sự thực thi của một hệ thống dịch chuyển mô tả các hành vi có thể của hệ
thống dịch chuyển:
Định nghĩa 1.2.5. Đoạn thực thi[3]
Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. Một đoạn thực thi
hữu hạn ϱ của T S là một chuỗi xem kẽ của các trạng thái và các hành vi kết thúc
với một trạng thái:
αi+1
ϱ = s0 α1 s1 α2 ...αn sn sao cho si −−−→ si+1 với mọi 0 ≤ i < n,
16
với n ≥ 0. n là độ dài của đoạn thực thi ϱ. Một đoạn thực thi vô hạn ρ của T S là
một chỗi vô hạn, xen kẽ của các trạng thái và các hành vi:
αi+1
ρ = s0 α1 s1 α2 ... sao cho si −−−→ si+1 với mọi i ≥ 0.
Các đoạn thực thi ϱ = s0 α1 ...αn sn và ρ = s0 α1 s1 α2 ... được viết tương ứng như
sau:
αn
α1
α1
α2
ϱ = s0 −→ ... −→ sn và ρ = s0 −→ s1 −→ ...
Một đoạn thực thi được gọi là tối đa khi không thể kéo dài thêm được nữa.
Định nghĩa 1.2.6. Đoạn thực thi tối đa và đoạn thực thi khởi đầu[3]
Một đoạn thực thi tối đa gồm cả đoạn thực thi hữu hạn kết thúc tại một trạng thái
kết thúc, hoặc một đoan thực thi vô hạn. Một đoạn thực thi được gọi là khởi đầu
nếu bắt đầu tại một trạng thái khởi tạo, nghĩa là s0 ∈ I
Định nghĩa 1.2.7. Thực thi[3]
Một thực thi của một hệ thống dịch chuyển T S là một đoạn thực thi khởi đầu và
tối đa.
Định nghĩa 1.2.8. Các trạng thái tới được[3]
Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. Một trạng thái s ∈ S
được gọi là tới được trong T S nếu tồn tại một đoạn thực thi khởi đầu và hữu hạn:
α1
α2
αn
s0 −→ s1 −→ ... −→ sn = s.
Reach(T S ) biểu diễn tập hợp tất cả các trạng thái tới được trong T S .
1.2.2. Logic thời gian
Đối với các hệ thống phản ứng, tính đúng đắn phụ thuộc vào sự thực thi của hệ
thống, không chỉ là đầu vào và đầu ra của việc tính toán mà còn là vấn đề công
bằng (fairness). Logic thời gian[4, 5, 8, 14] là một hình thức vượt trội để xử lý các
vấn đề này. Logic thời gian mở rộng logic mệnh đề hoặc logic tân từ bằng cách
cho phép chuyển tới hành vi vô hạn của một hệ thống phản ứng. Chúng cung cấp
các ký hiệu một cách trực quan nhưng có một nền tảng toán học chính xác để diễn
tả tính chất về mối quan hệ giữa các nhãn trạng thái trong thưc thi. Các hình thức
17
cơ bản của thời gian được thể hiện trong phần lớn các logic thời gian bao gồm hai
toán hạng:
♢(hay còn được ký hiệu là F): cuối cùng trong tương lai.
(hay còn được ký hiệu là G): bây giờ và sau này trong tương lai.
Bản chất cơ bản của logic thời gian có thể là một trong hai loại tuyến tính
(linear) hoặc phân nhánh (branching). Trong quan điểm của tuyến tính, ở mỗi thời
điểm có một thời điểm kế tiếp, trong khi đó ở quan điểm của phân nhánh có cấu
trúc như cây, nơi mà thời gian có thể phân thành các hướng khác nhau để lựa chọn.
Năm 1977, Amir Pnueli đề xuất logic thời gian tuyến tính (LTL). Logic này được
mở rộng từ logic mệnh đề với toán hạng thời gian G và F và khái niệm của tính
công bằng (fairness) đảm bảo cho một đường dẫn ngữ nghĩa vô hạn. LTL đã được
mở rộng sau đó gồm có toán hạng U (“until”: cho đến khi) được đưa ra bởi Kamp
vào năm 1968 và toán hạng X (“next time”: thời gian tiếp theo) từ logic thời
gian UB (hệ thống hợp nhất của thời gian phân nhánh). Vào năm 1981, Clarke và
Emerson đã mở rộng UB, qua đó phát minh ra logic thời gian phân nhánh đặt tên
là logic tính toán cây (CTL) và kiểm chứng mô hình CTL. Lichtenstein và Pnueli
đã định nghĩa kiểm chứng mô hình cho LTL vào năm 1985. Hợp nhất giữa LTL và
CTL, được gọi là CTL*, được định nghĩa bởi Emerson và Halpern vào năm 1986,
mặc dù hiện tại vẫn không có công cụ kiểm chứng nào cho ngôn ngữ này. Vì cả
hai kiểm chứng mô hình nói chung và kiểm chứng mô hình trừu tượng nói riêng
ban đầu đều được định nghĩa cho CTL, và do đó, kiểm chứng mô hình LTL thường
xuyên được định nghĩa trong các tài liệu liên quan tới kiểm chứng mô hình CTL.
1.2.3. Logic thời gian tuyến tính (LTL) và logic tính toán cây (CTL)
Cho một hệ thống dịch chuyển T , chúng ta có thể đặt ra những câu hỏi như
sau:
- Có một vài trạng thái “không mong muốn” có thể truy cập ở trong T , chẳng
hạn như trạng thái thể hiện deadlock, hoặc sự vi phạm của mutual exclusion,
...?
- Có những hoạt động của T sao cho, từ một vài điểm trở về sau, một vài trạng
thái “mong muốn” không bao giờ tới được hoặc một vài hành động không
bao giờ được thực thi? Những hoạt động như vậy có thể tương trưng cho các
18
livelock, một ví dụ, một vài tiến trình bị ngăn chặn từ lúc đi vào phần then
chốt của nó, mặc dù các thành phần khác của hệ thống có thể vẫn tiến hành.
- Một vài trạng thái khởi tạo hệ thống của T có thể truy cập được từ mọi trạng
thái? Nói cách khác, hệ thống có thể được thiết lập lại?
Logic thời gian tuyến tính (LTL)
Logic thời gian là một ngôn ngữ thuận tiện cho việc biểu thị hình thức các
thuộc tính như vậy. Trước tiên chúng ta xem xét logic thời gian tuyến tính (LTL)
với các công thức của nó biểu thị các thuộc tính của các hoạnh động trong các hệ
thống dịch chuyển. Giả sử cho một tập hợp đếm được V của các mệnh đề nguyên
tử, các mệnh đề nguyên tử thể hiện các thuộc tính của những trạng thái riêng lẻ. Lý
luận của logic thời gian tuyến tính qua những dấu vết tuyến tính theo thời gian. Ở
mỗi thời điểm, chỉ có một lịch trình trong tương lai thực sự xảy ra. Thông thường,
lịch trình được định nghĩa như bắt đầu ở “hiện tại”, trong các bước thời gian hiện
hành, và tiến triển vô hạn trong tương lai.
Định nghĩa 1.2.9. Công thức của mệnh đề LTL[11]
Những công thức của mệnh đề logic thời gian PTL trong thời gian tuyến tính được
định nghĩa quy nạp như sau:
- Mọi mệnh đề cơ bản v ∈ V là công thức.
- Hợp của hai mệnh đề là một mệnh đề.
- Nếu φ và ψ là các công thức thì Xφ và φUψ cũng là các công thức.
Công thức PTL được diễn giải qua các hành vi. Chúng ta giả sử rằng mệnh đề
cơ bản v ∈ V có thể đánh giá ở các trạng thái s ∈ S và viết s(V) để biểu diễn tập
hợp của các mệnh đề đúng ở trạng thái s. Với hành vi σ = s0 s1 ..., lấy σi biểu diễn
trạng thái si và σ|i hậu tố si si+1 ... của σ.
Định nghĩa 1.2.10. Quan hệ nắm giữ LTL[11]
Quan hệ σ |= φ (σ nắm giữ của φ) được định nghĩa quy nạp như sau:
- σ |= v (với v ∈ V) khi và chỉ khi v ∈ σ0 (V).
- Ngữ nghĩa của phép hợp được định nghĩa như bình thường.
- σ |= Xφ khi và chỉ khi σ1 |= φ.
19
- σ |= φU khi và chỉ khi với một số k ≥ 0, σ|k |= ψ và σ| j |= φ nắm giữ với mọi
0 ≤ j ≤ k.
Những công thức PTL hữu ích khác có thể được đưa ra như những từ viết tắt:
Fφ (“cuối cùng φ”) được định nghĩa như true U φ; nó khẳng định rằng φ nắm giữ
của một vài hậu tố. Công thức kép Gφ ≡ ¬F¬φ (“luôn luôn” φ) yêu cầu φ nắm
giữ tất cả các hậu tố. Công thức φWψ (“φ chờ đợi ψ”,“φ trừ khi ψ”) được định
nghĩa như (φUψ) ∨ Gφ và yêu cầu φ nắm giữ cho đến khi ψ không nắm giữ; không
giống như φUψ, nó không yêu cầu ψ trở thành đúng ở sau cùng.
Những công thức sau đây là những ví dụ điển hình khẳng định tính đúng đắn
về quản lý tài nguyên của hai tiến trình. Chúng ta giả sử rằng reqi và ownsi là hai
mệnh đề cơ bản đúng khi tiến trình được yêu cầu tài nguyên hoặc khi nó sở hữu
tài nguyên.
G¬(owns1 ∧ owns2 ): Không bao giờ trường hợp cả hai tiến trình đều sở hữu
tài nguyên. Nói chung, các tính chất của hình thức Gp, cho các công thức
không phải là thời gian p, biểu thị cho những bất biến của hệ thống (system
invariants).
G(req1 ⇒ Fowns1 ): Bất cứ khi nào tiến trình 1 yêu cầu tài nguyên, cuối cùng
nó sẽ có được. Các công thức của hình thức này thường được gọi sụ phản hồi
các thuộc tính (response properties).
GF(req1 ∧ ¬(owns1 ∨ owns2 )) ⇒ GFowns1 : Nếu nó rất nhiều lần thường xảy
ra trường hợp tiến trình 1 yêu cầu tài nguyên khi tài nguyên rảnh, sau đó tiến
trình 1 rất nhiều lần thường sở hữu tài nguyên. Công thức này biểu thị tình
trạng công bằng (mạnh) cho tiến trình 1.
G(req1 ∧ req2 ⇒ (¬owns2 W(owns2 W(¬owns2 Wowns1 )))): Bất kì khi nào
cả hai tiến trình cạnh trạnh tài nguyên, tiến trình 2 sẽ được cấp tài nguyên
nhiều nhất một lần trước khi cấp cho tiến trình 1. Tính chất này là một ví dụ
cho thuộc tính ưu tiên (precedence property). Cách tốt nhất được hiểu như
sự khẳng định hiện hữu của cả 4, có thể trống hoặc được mở (right-open),
những khoảng thời gian mà thỏa mãn những điều kiện tương ứng.
20
Logic tính toán cây CTL
Các công thức PTL khẳng định các thuộc tính của các hành vi đơn lẻ, nhưng
chúng cũng quan tâm đến giá trị của hệ thống: chúng ta nói rằng công thức φ nắm
giữ của T (viết là T |= φ) nếu φ nắm giữ của tất cả các hoạt động của T . Theo
nghĩa này, các công thức PTL biểu thị các tính chất đúng đắn của hệ thống. Sự
hiện diện của một hoạt động thỏa mãn một thuộc tính nhất định không thể biểu
thị trong PTL. Các thuộc tính có khả năng như vậy thuộc về logic thời gian phân
nhánh như logic CTL. Trong mô hình thời gian nhánh, tại mỗi thời điểm t có thể
có rất nhiều khả năng trong tương lai. Với những khả năng tương lai tương ứng là
một đường đi được tổ chức từ t. Do đó, một đường đi biểu diễn một khả năng xảy
ra trong tương lai. Các toán tử thường biểu thị hoặc là “A” nghĩa là với mọi khả
năng trong tương lai diễn tả luôn luôn, chắc chắn hoặc là “E” nghĩa là có thể tồn
tại khả năng tương lai diễn tả sự có thể, không chắc chắn.
Định nghĩa 1.2.11. Công thức mệnh đề CTL[11]
Các công thức của mệnh đề CTL được định nghĩa quy nạp như sau:
- Mọi mệnh đề nguyên tử v ∈ V đều là công thức.
- Hợp của hai mệnh đề là một mệnh đề.
- Nếu φ và ψ là các công thức thì EXφ, EGφ, và φEUψ là các công thức.
Các công thức CTL được diễn giải ở các trạng thái của hệ thống dịch chuyển.
Một đường dẫn (path) trong T là một ω − sequence σ = s0 s1 . . . của các trạng thái
có quan hệ δ, nó là một đường dẫn s − path nếu s = s0 .
Định nghĩa 1.2.12. Quan hệ nắm giữ CTL[11]
Quan hệ T , s |= φ được định nghĩa theo quy nạp như sau:
- T , s |= v (với v ∈ V) khi và chỉ khi v ∈ s(V).
- Ngữ nghĩa của phép hợp được định nghĩa như bình thường.
- T , s |= EXφ khi và chỉ khi tồn tại một s-path s0 s1 . . . sao cho T , s1 |= φ.
- T , s |= EGφ khi và chỉ khi có một s-path s0 s1 . . . sao cho T , si |= φ. nắm giữ
với mọi i.
- Xem thêm -