ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
HOÀNG MẠNH KHÔI
KIỂM CHỨNG TỪNG PHẦN CHO CHƯƠNG
TRÌNH C
LUẬN VĂN THẠC SĨ
Hà Nội - 2012
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
HOÀNG MẠNH KHÔI
KIỂM CHỨNG TỪNG PHẦN CHO CHƯƠNG
TRÌNH C
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Ĩ
NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS.TS. Nguyễn Việt Hà
Hà Nội - 2012
i
MỤC LỤC
MỤC LỤC .......................................................................................................... i
BẢNG CÁC CHỮ VIẾT TẮT ........................................................................... ii
DANH MỤC HÌNH VẼ .................................................................................... iii
Chương 1: Giới Thiệu ........................................................................................ 1
Chương 2: Một Số Khái Niệm Cơ Bản ............................................................... 4
2.1
2.2
Hệ chuyển trạng thái được gán nhãn - LTS .................................... 4
Các phương pháp biểu diễn LTS .................................................... 8
2.2.1 Phương pháp liệt kê ............................................................. 8
2.2.2 FSP ...................................................................................... 8
2.3
2.4
2.5
Trừu tượng hóa thủ tục - PA ......................................................... 10
Logic thời gian tuyến tính - LTL .................................................. 12
Đồ thị luồng điều khiển - CFG ..................................................... 14
Chương 3: Phương Pháp Kiểm Chứng ............................................................. 16
3.1
Xây dựng mô hình MImp ............................................................. 16
3.1.1 Otomat luồng điều khiển ................................................... 17
3.1.2 Otomat luồng điều khiển mở rộng ..................................... 19
3.1.3 Phương pháp trừu tượng mệnh đề ...................................... 20
3.2
Kiểm chứng .................................................................................. 26
3.2.1 Phép ghép nối song song ................................................... 27
3.2.2 Kiểm chứng tính đúng đắn của chương trình ..................... 28
Chương 4: Ứng Dụng Với Công Cụ Copper ..................................................... 30
4.1
4.2
Công cụ Copper ........................................................................... 30
Một số ứng dụng .......................................................................... 32
Ví dụ 4.1: ..................................................................................... 32
Ví dụ 4.2: ..................................................................................... 38
KẾT LUẬN ...................................................................................................... 42
TÀI LIỆU THAM KHẢO ................................................................................ 43
ii
BẢNG CÁC CHỮ VIẾT TẮT
STT
Từ viết tắt
Tiếng anh
Nghĩa tiếng Việt
1
LTS
Labeled Transition System
Hệ chuyển trạng thái được
gán nhãn
2
FSP
Finite State Process
Tiến trình hữu hạn trạng thái
3
PA
Procedure Abstraction
Trừu tượng hóa thủ tục
4
CFG
Control Flow Graph
Đồ thị luồng điều khiển
5
CFA
Control Flow Automata
Otomat luồng điều khiển
6
WP
Weakest Preconditon
Tiền điều kiện yếu nhất
iii
DANH MỤC HÌNH VẼ
Hình 2.1: Một hệ thống chuyển trạng thái được gán nhãn. ..................... 5
Hình 2.2: Hệ chuyển trạng thái được gán nhãn không đơn định. ............ 6
Hình 2.3: Hệ chuyển trạng thái được gán nhãn đơn định. ....................... 6
Hình 2.4: Dạng biểu diễn liệt kê của LTS............................................... 8
Hình 2.4: Biểu diễn FSP của LTS Switch. .............................................. 9
Hình 2.6: Biểu diễn FSP của một LTS. .................................................. 9
Hình 2.7: Hệ trạng thái được gán nhãn L1. ........................................... 11
Hình 2.8: Hệ trạng thái được gán nhãn L2. ........................................... 11
Hình 2.9: Ngữ nghĩa LTL cho các từ vô hạn trên 2AP . ......................... 13
Hình 2.10: Minh hoạ ngữ nghĩa của LTL. ............................................ 14
Hình 2.11: Một chương trình C và CFG của nó. ................................... 15
Hình 3.1: CFA của một chương trình C. ............................................... 18
Hình 3.2: Spec của chương trình C trong ví dụ 3.1. .............................. 22
Hình 3.3: LTS biểu diễn hàm do_a. ...................................................... 22
Hình 3.4: LTS biểu diễn hàm do_b. ..................................................... 22
Hình 3.5: CFA với các trạng thái được gán tập các mệnh đề logic. ...... 23
Hình 3.6: MImp của một chương trình C. ............................................. 26
Hình 3.7: LTS Input và Output. ............................................................ 27
Hình 3.8: LTS ghép nối song song Input||Output. ................................. 28
Hình 3.9: LTS của thuộc tính p và LTS lỗi tương ứng của p. ............... 29
Hình 4.1: Input/Ouput của công cụ Copper. ......................................... 30
Hình 4.2: Kiến trúc minh họa công cụ Copper. .................................... 32
Hình 4.3: LTS miêu tả hành vi của chương trình. ................................. 33
Hình 4.4: LTS miêu tả hành vi của chương trình. ................................. 33
Hình 4.5 Kết quả chạy ví dụ 1 với công cụ Copper. ............................. 36
Hình 4.6 Kết quả chạy ví dụ 1 với công cụ Copper. ............................. 37
Hình 4.7 Kết quả chạy ví dụ 2 với công cụ Copper. ............................. 39
Hình 4.8 Kết quả chạy ví dụ 2 với công cụ Copper. ............................. 40
1
Chương 1: Giới Thiệu
Đảm bảo chất lượng phần mềm là một trong những hoạt động quan trọng và khó
khăn nhất trong quy trình phát triển phần mềm. Hoạt động này cũng chiếm thời
gian và kinh phí rất lớn (khoảng 15-20%) trong kinh phí của mỗi dự án phát
triển phần mềm. Có rất nhiều phương pháp được sử dụng trong việc đảm bảo
chất lượng phần mềm. Kiểm thử phần mềm đang là giải pháp được sử dụng phổ
biến nhất trong công nghiệp. Tuy nhiên, kiểm thử chỉ cho phép chỉ ra các lỗi của
phần mềm chứ không có khả năng chứng minh hệ thống không còn lỗi. Để
chứng minh tính đúng đắn của các hệ thống, kiểm chứng mô hình [6] đang được
quan tâm như một giải pháp hiệu quả nhất và ngày càng được sử dụng rộng rãi,
đặc biệt là trong các hệ thống phần mềm đòi hỏi độ chính xác cao.
Kiểm chứng mô hình là một nhóm các kĩ thuật ứng minh tự động tính
đúng đắn của hệ thống với các đặc tả thuộc tính nào đó. Với mục đích này, các
kỹ thuật kiểm chứng mô hình phải xây dựng mô hình hình thức đặc tả chính xác
hành vi của hệ thống cần kiểm chứng. Mô hình là một hệ thống bao gồm tập hợp
có giới hạn các trạng thái và tập hợp các bước chuyển tiếp giữa các trạng thái
đó. Kiểm chứng mô hình là chứng minh tính đúng đắn của mô hình bằng cách
xác định xem thuộc tính mà người dùng mong muốn có được thõa mãn bởi mô
hình đó hay không [6].
Trong kiểm chứng mô hình phần mềm có hai bài toán được quan tâm
chính đó là kiểm chứng tính đúng đắn của đặc tả thiết kế và kiểm chứng tính
đúng đắn của mã nguồn. Bài toán kiểm chứng tự động mã nguồn được xem là
ứng dụng đầu tiên của kiểm chứng mô hình trong việc đảm bảo chất lượng phần
mềm. Dù cách tiếp cận này đã được đề xuất từ lâu nhưng đến nay nó vẫn là vấn
đề mở và chưa có giải pháp thõa đáng do gặp phải vấn đề bùng nổ không gian
trạng thái và khó khăn trong việc xây dựng mô hình đặc tả hành vi của mã
nguồn. Vì vậy kiểm chứng mã nguồn vẫn nhận được sự quan tâm rộng rãi trong
nghiên cứu cũng như trong ứng dụng công nghiệp.
Xem xét một chương trình C có mã nguồn lớn và tồn tại nhiều lời gọi đến
các hàm thư viện hoặc các hàm do người phát triển định nghĩa. Phương pháp
hiện tại để kiểm chứng chương trình này là xây dựng một mô hình đặc tả toàn bộ
hành vi của chương trình bao gồm cả hành vi của các hàm được gọi trong
chương trình. Để làm được việc này, yêu cầu là phải có tất cả mã nguồn của các
hàm này. Tuy nhiên, chúng ta thường khó khăn trong việc có đầy đủ mã nguồn
2
và tài liệu đặc tả của các hàm được gọi vì trong nhiều trường hợp chúng ta sử
dụng đến thư viện của các bên thứ ba. Kết quả là, chúng ta không áp dụng được
phương pháp hiện tại cho bài toán này. Cho dù chúng ta có đủ mã nguồn của các
hàm được gọi, việc áp dụng phương pháp kiểm chứng này cũng sẽ gặp phải bài
toán bùng nổ không gian trạng thái vì kích thước của chương trình cộng với mã
nguồn của các hàm được gọi là rất lớn.
Trong luận văn này tôi xin giới thiệu một phương pháp mới [3] [4] trong
kiểm chứng tự động để kiểm chứng một cài đặt của chương trình C có mã nguồn
lớn và có nhiều thành phần nhằm giải quyết các vấn đề nêu trên.
Cách tiếp cận của phương pháp là chúng ta đưa việc kiểm chứng một
chương trình phần mềm lớn về việc kiểm chứng các thành phần con nhỏ hơn và
đơn giản hơn bằng cách trừu tượng hóa hành vi [3] (procedure abtraction-PA)
của các thành phần con (hay các hàm thư viện) theo một khái niệm đặc tả của
máy hữu hạn trạng thái đó là hệ thống chuyển trạng thái được gán nhãn LTS
(Label Transition System) [4]. Phương pháp cho phép chúng ta tự định nghĩa
các hành vi của các hàm thư viện (chưa có mã nguồn hoặc chưa rõ hành vi) và
sử dụng chúng như là giả thiết trong quá trình xây dựng mô hình kiểm chứng.
Nội dung chính của luận văn là giới thiệu phương pháp kiểm chứng phần
cài đặt của một chương trình viết bằng ngôn ngữ C có đảm bảo đúng với đặc tả
của nó. Để làm được điều đó, trước hết từ mã nguồn C chúng ta phải xây dựng
được mô hình LTS biểu diễn hành vi của chương trình bằng phương pháp trừu
tượng mệnh đề (predicate abstraction) kết hợp với các LTS giả thiết biểu diễn
hành vi của các thành phần con, sau đó sử dụng kĩ thuật kiểm chứng để kiểm
định xem nó có đảm bảo đúng với mô hình LTS của đặc tả hay không.
Nội dung của luận văn được trình bày trong 4 chương:
Chương 1 giới thiệu về đề tài, trình bày tổng quan về nội dung phương
pháp được nghiên trong đề tài, mục tiêu của đề tài và cấu trúc của luận văn.
Chương 2 trình bày các khái niệm cơ bản phục vụ cho đề tài, chương này
đưa ra các khái niệm về mô hình chuyển trạng thái được gán nhãn LTS, các
phương pháp biểu diễn LTS, khái niệm về trừu tượng hóa hành vi của hệ thống
PA, cũng như các khái niệm cần thiết trong kĩ thuật kiểm chứng …
Chương 3 trình bày nội dung chính của luận văn, đó là nêu cách xây dựng
mô hình LTS biểu diễn hành vi của hệ thống từ mã nguồn bắt đầu bằng việc xây
3
dựng sơ đồ luồng xử lý CFA (Control Flow Automata) [3] và sơ đồ luồng xử lý
mở rộng (Expanding Control flow Automata) [3] của chương trình có sử dụng
các LTS giả thiết. Giới thiệu phương pháp trừu tượng mệnh đề để xây dựng
được mô hình LTS biểu diễn hành vi của mã nguồn từ sơ đồ luồng xử lý mở
rộng. Và cuối cùng nêu cách kiểm chứng mô hình LTS của phần cài đặt có đảm
bảo với mô hình LTS của đặc tả.
Chương 4 luận văn đưa ra ứng dụng của phương pháp bằng cách giới
thiệu các công cụ Copper [2]. Đầu vào của công cụ này là tập file mã nguồn C
của chương trình và các đặc tả của các thuộc tính cần kiểm chứng, đầu ra là kết
luận phần cài đặt đã đúng với đặc tả của nó hoặc đưa ra phản ví dụ chứng minh
cài đặt không đúng với đặc tả. Trong chương này giới thiệu một vài ứng dụng
đơn giản được áp dụng thực tế trên công cụ bằng cách nêu chi tiết cách xây
dựng các file đặc tả cũng như cách xây dựng các PA giả thiết bằng ví dụ.
Phần cuối của luận văn trình bày những kết quả đạt được, hướng nghiên
cứu phát triển trong tương lai và những hạn chế cần khắc phục.
4
Chương 2: Một Số Khái Niệm Cơ Bản
Trong chương này chúng ta sẽ tìm hiểu một số khái niệm cần thiết như máy hữu
hạn trạng thái, hệ chuyển trạng thái được gán nhãn và khái niệm về trừu tượng
hóa hành vi một chương trình…
2.1 Hệ chuyển trạng thái được gán nhãn - LTS
Trong các nghiên cứu về máy trạng thái, cấu trúc Kripke [6] thường được sử
dụng để mô hình hóa và đặc tả hệ thống, tuy nhiên đối với phương pháp này
chúng ta sẽ sử dụng khái niệm hệ thống chuyển trạng thái được gán nhãn
(Labeled Transition System - LTS) [4]. LTS cũng tương tự như cấu trúc Kripke
nhưng các bước chuyển trạng thái đều được gán nhãn bởi các hành động.
Về lý thuyết sự hiện diện của hành động không làm tăng khả năng biểu
diễn của LTS hơn cấu trúc Kripke. Tuy nhiên, nó là tự nhiên hơn cho các nhà
thiết kế và kỹ sư phần mềm để thể hiện các hành vi mong muốn của hệ thống
bằng cách sử dụng sự kết hợp giữa trạng thái và hành động.
Định nghĩa 2.1: Hệ thống chuyển trạng thái được gán nhãn
Một hệ chuyển trạng thái được gán nhãn M là một bộ có thứ tự gồm bốn
thành phần S, S0 , Act, T trong đó:
S là một tập khác rỗng các trạng thái của M
S0 ⊆ S là trạng thái khởi tạo
Act là tập các hành động quan sát được
T ⊆ S × Act × S là hàm chuyển trạng thái
a
Ta kí hiệu S
S ′ nếu có một hành động a chuyển hệ thống từ trạng
thái S sang trạng thái S’. Trạng thái kết thúc STOP là trạng thái mà ở đó không
có hành động để chuyển sang một trạng thái nào khác, tức với S ′ ∈ S, ∀a ∈
Act, (STOP, a, S ′ ) ∉ T.
Chú ý 2.1: Chúng ta dùng π để kí hiệu trạng thái lỗi đặc biệt của hệ thống, và
để biểu diễn LTS <{π}, Act, ∅, π>. 𝜏 là hành động cục bộ không quan sát được
trong môi trường của một hệ thống phần mềm.
5
Ví dụ 2.1: Hệ chuyển trạng thái được gán nhãn
S0
lock
S1
return {0}
Return {1}
STOP
Hình 2.1: Một hệ thống chuyển trạng thái được gán nhãn.
Hình 2.1 mô tả một ví dụ về một hệ chuyển trạng thái được gán nhãn M =
S, S0 , Act, T , trong đó:
S = {S0, S1, STOP},
Act = {lock, return {0}, return {1}},
T = { (S0, lock, S1), (S1, return {0}, STOP), (S0, return {1}, STOP)},
S0 là trạng thái khởi đầu.
Định nghĩa 2.2: Kích thước của hệ chuyển trạng thái được gán nhãn
Kích thước của hệ chuyển trạng thái được gán nhãn M = S, S0 , Act, T là
số trạng thái của M, ký hiệu là |M|, trong đó |M| = |S|.
Định nghĩa 2.3: Hệ chuyển trạng thái được gán nhãn đơn định và không đơn
định.
Một hệ chuyển trạng thái được gán nhãn M = S, S0 , Act, T là không đơn
định nếu nó chứa τ- chuyển dịch hoặc nếu ∃ s, a, s ′ , (s, a, s′′) ∈ T thì s′ ≠ s′′.
Ngược lại, M là hệ chuyển trạng thái được gán nhãn đơn định.
Chú ý 2.2: Cho 2 hệ chuyển trạng thái được gán nhãn M = S, S0 , Act, T và M' =
S′, S0′ , Act′, T′ . Ta nói M chuyển dịch thành M' với chuyển dịch a nếu và chỉ
nếu (S0 , a, S0′ ) ∈ T, Act = Act′, S = S' và T = T′. Ta ký hiệu: M
a
M'.
6
Ví dụ 2.2: Một hệ thống chuyển trạng thái được gán nhãn đơn định và không
đơn định
a1
s1
s0
a1
a2
a3
s2
Hình 2.2: Hệ chuyển trạng thái được gán nhãn không đơn định.
Hình 2.2 mô tả một hệ chuyển trạng thái được gán nhãn không đơn định
M = S, S0 , Act, T trong đó: S = s0 , s1 , s2 , Act = a1 , a2 , a3 , s0 là trạng thái
khởi đầu và T = s0 , a1 , s1 , s0 , a1 , s2 , s1 , a2 , s2 , (s2 , a3 , s0 }.
Khi hệ thống đang ở trạng thái s0 , thực hiện một hành động a1 thì hệ
thống có thể chuyển đến trạng thái s1 hoặc trạng thái s2 . Như vậy, trạng thái kế
tiếp của s0 khi thực hiện cùng một hành động a1 là không xác định duy nhất hay
không tất định. Ta gọi đó là hệ chuyển trạng thái được gán nhãn không đơn
định.
a1
s1
s0
a2
a2
a3
s2
Hình 2.3: Hệ chuyển trạng thái được gán nhãn đơn định.
Hệ chuyển trạng thái được gán nhãn như trên hình 2.3 là một hệ chuyển
trạng thái được gán nhãn đơn định. Từ trạng thái si bất kỳ nếu thực hiện một
hành động ai nào đó thì hệ thống sẽ chuyển sang một trạng thái xác định duy
nhất sk .
7
Định nghĩa 2.4: Dẫn xuất của một hệ chuyển trạng thái được gán nhãn M.
Dẫn xuất σ của một hệ chuyển trạng thái được gán nhãn M =
S, S0 , Act, T là một chuỗi hữu hạn các hành động a1 , a2 , … , an với a1 = S0 ,
ai ∈ Act (i = 1,..,n).
Như vậy dẫn xuất σ của hệ chuyển trạng thái được gán nhãn M là một
chuỗi các hành động quan sát được mà M có thể thực hiện từ trạng thái khởi tạo
S0 .
Ví dụ 2.3: Với hệ chuyển trạng thái được gán nhãn M như trên hình 2.1, chuỗi
các hành động lock, return {0} là một dẫn xuất trên M. Từ trạng thái S0 thực
hiện hành động lock hệ thống chuyển sang trạng thái S1, tiếp tục thực hiện hành
động return{0} hệ thống chuyển sang trạng thái STOP.
Chú ý 2.3: Ta ký hiệu σ↑Σ là một dẫn xuất thu được bằng cách loại bỏ khỏi σ tất
cả các hành động a mà a ∉ Σ. Tập tất cả các dẫn xuất của M được gọi là ngôn
ngữ của M, ký hiệu L(M). Một dẫn xuất σ = a1 a2 … an là một dẫn xuất hữu hạn
trên hệ chuyển trạng thái được gán nhãn M. Ta ký hiệu hệ chuyển trạng thái
được gán nhãn Mσ = (S, S0 , Act, T) với S = {s0 , s1 , … , sn } và T = {si−1 , ai , si }
với i=1,..,n. Ta nói rằng một hành động a ∈ Act được chấp nhận từ một trạng
thái s ∈ S nếu tồn tại s′ ∈ S sao cho (s, a, s ′ ) ∈ T. Tương tự vậy ta nói rằng một
dẫn xuất a1 a2 … an được chấp nhận từ trạng thái s ∈ S nếu tồn tại một dãy các
trạng thái s0 , s1 , … , sn với s0 = S0 sao cho ∀i= 1, n thì (si−1 , ai , si ) ∈ T.
Định nghĩa 2.5:
Cho một dẫn xuất σ = 𝑎1 , 𝑎2 , … , 𝑎𝑛 và hai trạng thái s, t của hệ chuyển
trạng thái được gán nhãn M = S, S0 , Act, T . Ta nói rằng t có thể đi đến được từ
s thông qua dẫn xuất σ (viết là 𝑠
σ
𝑠0 , … , 𝑠𝑛 với s = 𝑠0 và t = 𝑠𝑛 sao cho 𝑠0
𝑡) nếu tồn tại một tập các trạng thái
𝑎1
𝑠1
𝑎2
…
𝑎𝑛
𝑠𝑛 .
Ví dụ 2.4: Với hệ chuyển trạng thái M trong ví dụ 2.1, ta có trạng thái STOP có
thể đi đến được từ S0 thông qua dẫn xuất σ1 = (lock, ruturn {0}) hoặc dẫn xuất
σ2 = (return {1}).
8
2.2 Các phương pháp biểu diễn LTS
2.2.1 Phương pháp liệt kê
Dạng liệt kê là một phương pháp biểu diễn LTS khá tự nhiên và phổ biến. Trong
phương pháp này, một LTS được biểu diễn bằng cách liệt kê tất cả các hàm
chuyển trạng thái cùng với trạng thái khởi tạo. Hình 2.4 định nghĩa đệ quy
phương pháp biểu diễn này. Trong đó State đại diện cho một trạng thái của hệ
thống, Action đại diện cho một hành động thuộc tập các hành động, Transition
là một phép chuyển trạng thái, Transitions là một dãy tuần tự các phép chuyển
trạng thái và LTS được biểu diễn bằng Transitions và kết thúc bằng trạng thái
khởi tạo.
State = Id
Action = Id
Transition = (State, Action, State)
Transitions = Transition | Transition, Transitions
LTS = Transition, State
Hình 2.4: Dạng biểu diễn liệt kê của LTS.
2.2.2 FSP
FSP là viết tắt của Finite State Process [9] (các tiến trình hữu hạn trạng thái), là
một ngôn ngữ biểu diễn tương ứng với LTS. FSP dùng để xây dựng mô hình các
tiến trình. Một tiến trình được chia làm một hoặc nhiều hành động nguyên tử
(hành động nguyên tử không thể chia được thành các hành động nhỏ hơn), các
hành động này được thực thi một cách tuần tự. Mỗi hành động gây ra một sự
chuyển tiếp từ trạng thái hiện tại sang trạng thái tiếp theo. Trình tự các hành
động xảy ra có thể được xác định bằng một đồ thị chuyển tiếp. Nói cách khác,
chúng ta có thể mô hình hóa các tiến trình thành các máy hữu hạn trạng thái.
Như vậy, chúng ta hoàn toàn có thể mô hình hóa chi tiết một hệ chuyển
trạng thái được gán nhãn (LTS) bằng các khái niệm đặc tả của FSP.
9
Các thành phần cơ bản trong FSP:
Action prefix ((x -> P)): Nếu x là hành động và P là một tiến trình thì một
action Prefix (x -> P) mô tả một tiến trình trong đó các hành động x được thực
hiện theo mô tả của tiến trình P. Tiến trình P phải viết hoa chữ cái đầu, hành
động x viêt bằng chữ cái thường.
Ví dụ 2.5:
Hình 2.5 biểu diễn bằng khái niệm Action Prefix trong FSP một LTS
SWITCH, LTS này bao gồm các trạng thái 0, 1 và các hành động on, off.
SWITCH = OFF,
OFF = (on -> ON),
ON = (off -> OFF).
Hay:
SWITCH = (on -> off -> SWITCH)
Hình 2.4: Biểu diễn FSP của LTS Switch.
Lựa chọn (| Choice): Nếu x, y là các hành động thì (x -> Q | y -> P) mô
tả một tiến trình trong đó các hành động đầu tiên tham gia là x hoặc y. Các hành
động tiếp theo hoạt động theo mô tả của Q nếu hành động đầu tiên xảy ra là x,
các hành động tiếp theo hoạt động theo mô tả của P nếu hành động đầu tiên xảy
ra là y.
Ví dụ 2.6: LTS như trên hình 2.3 có thể được biểu diễn bằng FSP như sau:
S0 = (a1
S1 |a2
S1 = (a2
S2 ),
S2 = (a3
S0 ).
S2 ),
Hình 2.6: Biểu diễn FSP của một LTS.
Biểu diễn LTS trực quan và dễ hiểu trong khi FSP mang tính tổng quát
hơn, tuy nhiên hai cách biểu diễn là tương đương nhau, tương ứng với mỗi FSP
thì có một biểu diễn LTS và ngược lại. Để biểu diễn được hết hệ thống LTS/FSP
10
còn có nhiều từ khóa và cấu trúc khác có thể tham khảo thêm trong [9] mà
không đề cập chi tiết trong luận văn này.
2.3 Trừu tượng hóa thủ tục - PA
Để kiểm chứng một chương trình từ mã nguồn chúng ta phải trừu tượng hóa
được các hành vi của chương trình và các hàm thư viện của nó bằng các đặc tả
LTS. Trong một chương trình C, một hàm thư viện có thể thực hiện những chức
năng khác nhau tùy thuộc vào tham số đầu vào hay ngữ cảnh thực hiện, trong
cách tiếp cận của phương pháp này chúng ta đưa ra khái niệm trừu tượng hóa
thủ tục (Procedure Abstraction - PA) [3] cho phép nhiều đặc tả LTS biểu diễn
cho một thủ tục hàm.
PA của một thủ tục hàm proc là một tập hữu hạn các cặp
g1 , M1 ,… g n , Mn trong đó:
g i là điều kiện (guard) ràng buộc trên các tham số của proc,
Mi là LTS trừu tượng hóa hành vi của proc ứng với điều kiện g i đạt giá
trị true.
Ví dụ 2.7: Xem xét chương trình C đơn giản sau:
int my_proc(int x)
{
int y;
if(x == 0) {
y = foo();
if(y > 0) return 10;
else return 20;
} else {
y = bar();
if(y < 0) return 30;
else return 40;
}
}
11
Hành vi của hàm my_proc ứng với trường hợp tham số đầu vào bằng 0 có
thể được mô tả bằng một hệ trạng thái được gán nhãn L1 đơn giản như trên hình
2.7.
Hình 2.7: Hệ trạng thái được gán nhãn L1.
Ứng với trường hợp tham số đầu vào bằng 1, hành vi của my_proc được
mô tả bằng máy trạng thái L2 (hình 2.8).
Hình 2.8: Hệ trạng thái được gán nhãn L2.
Như vậy PA của hàm my_proc sẽ là (g1 , M1 ), (g 2 , M2 ) với g1 = (x ==
0), M1 = L1 , g 2 = (x != 0), M2 = L2 .
Chú ý 2.4: Trong quá trình kiểm chứng, đối các hàm thư viện không có mã
nguồn thì các PA của nó được người dùng tự định nghĩa và cung cấp như là các
giả thiết trong việc xây dựng mô hình kiểm chứng, ta xem đó là các PA giả thiết.
Ví dụ 2.8: Với chương trình C ở ví dụ 2.4 ở trên có sử dụng hai hàm thư viện
không có mã nguồn là foo() và bar(). Chúng ta tự định nghĩa các LTS tương ứng
với mỗi hàm và cung cấp các PA cho quá trình kiểm chứng. LTS đặc tả tương
ứng cho hàm foo() là FOO, điều kiện (guard) tương ứng là TRUE lúc đó PA giả
thiết biểu diễn cho hàm foo() là (TRUE,FOO), điều này có nghĩa là dưới mọi
điều kiện của tham số đầu vào thì hàm foo() luôn được biểu diễn bằng LTS
FOO. Tương tự như vậy ta có PA cho hàm bar() là (TRUE, BAR).
12
2.4 Logic thời gian tuyến tính - LTL
Logic thời gian tuyến tính (Linear Temporal Logic - LTL) được đề xuất bởi
Amir Pnueli (1941-2009), là một loại logic áp dụng cho thời gian, được sử dụng
để xây dựng các công thức về tương lai. Ví dụ như một điều kiện cuối cùng sẽ
đúng hoặc một điều kiện sẽ đúng cho đến khi một điều kiện khác đúng, …
LTL là một phần của CTL* (một loại logic có thêm các lượng từ và nhánh
thời gian). LTL đầu tiên được đề xuất dùng trong kiểm chứng hình thức bởi
Amir Pnueli năm 1977.
Các toán tử trong LTL:
Ngoài các toán tử , biểu diễn các công thức trong logic mệnh đề, còn
có một số toán tử được bổ sung thêm F, G, X, U.
G đọc là Global (luôn xảy ra)
X đọc là NEXT (tiếp theo sẽ xảy ra)
U đọc là UNTIL (cho đến khi xảy ra)
F đọc là Future (cuối cùng sẽ xảy ra)
Trong đó các toán tử một ngôi có độ ưu tiên cao nhất, toán tử ¬ và toán tử
X có độ ưu tiên tương đương nhau. Toán tử U có độ ưu tiên hơn các toán tử ∧,∨
và →. Toán tử U có độ ưu tiên bên phải, tức là công thức 1 U (2 U 3 ) có thể
viết thành 1 U 2 U 3 .
Cú pháp trong LTL:
LTL được xây dựng từ các biến mệnh đề AP (Atomic Proposition), các
toán tử logic và các toán tử thời gian X, U. Một cách hình thức, các công thức
LTL được định nghĩa như sau:
Nếu p là một mệnh đề nguyên tử thì p (p AP) là một công thức
LTL.
Nếu ψ và φ là các công thức LTL thì ¬ψ, φ ∨ ψ, X ψ và φ U ψ cũng là
các công thức LTL.
::= true | a | 1 ∧ 2 | ¬ | X| 1 U 2 |
13
Ngữ nghĩa của LTL:
Công thức LTL biểu diễn các tính chất của một chuỗi hành động (gọi là
vết - trace). Một chuỗi các hành động có thể thoả một công thức LTL hoặc
không. Ngữ nghĩa của công thức LTL được định nghĩa như một ngôn ngữ
Words() chứa tất cả các từ vô hạn trên bảng chữ cái 2AP thoả mãn , sau đó
ngữ nghĩa được mở rộng để diễn giải toàn bộ các trạng thái và các chuỗi hành
động của một hệ thống dịch chuyển.
Định nghĩa 2.6: Ngữ nghĩa của LTL
Cho là một công thức LTL trên AP. Tính chất logic thời gian được sinh
ra bởi là
Words() = 2AP
| ⊨
Ở đây, quan hệ thoả được ⊨ là tập con của 2AP × LTLlà quan hệ nhỏ
nhất với thuộc tính trên hình 2.9. Ký hiệu ⊨ ⊆ 2AP ⨯ LTL.
σ ⊨ true
σ ⊨ 𝑎
nếu và chỉ nếu 𝑎 ∈ 𝐴0 (𝐴0 ⊨ 𝑎)
σ ⊨ 𝜑1 ∧ 𝜑2 nếu và chỉ nếu σ ⊨ 𝜑1 và σ ⊨ 𝜑2
σ ⊨ ¬φ
nếu và chỉ nếu σ ⊭ φ
σ ⊨ Oφ
nếu và chỉ nếu σ 1 … = 𝐴1 𝐴2 𝐴3 … ⊨ φ
σ ⊨ 𝜑1 ∪ 𝜑2 nếu và chỉ nếu ∃ 𝑗 ≥ 0. σ 𝑗 … ⊨ 𝜑2
và σ 𝑖 … ⊨ 𝜑1 cho mọi 0 ≤ 𝑖 ≤ 𝑗
Hình 2.9: Ngữ nghĩa LTL cho các từ vô hạn trên 2AP .
Ví dụ 2.9: Ngữ nghĩa của LTL
Giả sử a, b là hai mệnh đề nguyên tử, hình 2.10 minh họa ngữ nghĩa của
các phép toán đối với các mệnh đề này. Trong đó toán tử F được ký hiệu là ,
toán tử G ký hiệu là , toán tử X ký hiệu là O.
14
Hình 2.10: Minh hoạ ngữ nghĩa của LTL.
2.5 Đồ thị luồng điều khiển - CFG
Trong các kĩ thuật kiểm chứng, có một khái niệm được sử dụng rộng rãi trong
quá trình phân tích một chương trình phần mềm đó là đồ thị luồng điều khiển
(Control Flow Graph - CFG).
Đồ thị luồng điều khiển Gf = (N, E) của một chương trình f là một đồ thị có
hướng trong đó:
Mỗi đỉnh (node) nα tương ứng với một câu lệnh α trong f và bổ sung
thêm hai đỉnh nin , nout .
Cạnh (nα , nα′ ) ∈ E nếu lệnh α′ thực hiện ngay lập tức sau lệnh α. Với câu
lệnh đầu tiên α1 ta đưa vào cạnh (nin , nα 1 ). Và bổ sung cạnh (nα′ , nout )
cho mỗi đỉnh nα′ mà sau khi thực hiện lệnh α′ thì thoát khỏi hàm bởi lệnh
return hoặc kết thúc hàm.
CFG của một hàm rỗng ví dụ như hàm không có câu lệnh sẽ bao gồm
N = nin , nout và E = (nin , nout ) . Đỉnh (node) nin là đỉnh vào (entry node)
duy nhất và nout là đỉnh ra (exit node) duy nhất của Gf .
15
Ví dụ 2.10: Hình 2.11 biểu diễn hàm Search viết bằng ngôn ngữ C và CFG
tương ứng của nó. Ở đây ngoài hai đỉnh In, out tương ứng với điểm vào và điểm
ra, các đỉnh còn lại trong CFG của hàm Search đều tương ứng với từng câu lệnh
của nó.
void Search(int arr[], int key, int
In
*found, int *index)
{
=
int i = 0;
out
While
int b;
++
*found = 0;
While (i < N){
If
If (b = isabsequal(arr[i],key))
=
{
*found = b;
=
*index = I;
return;
Return
}
i ++;
}
}
Hình 2.11: Một chương trình C và CFG của nó.
- Xem thêm -
.PDF 
48 
122 
53 
