Kiểm chứng từng phần cho chương trình C

  • Số trang: 48 |
  • Loại file: PDF |
  • Lượt xem: 18 |
  • Lượt tải: 0
nhattuvisu

Đã đăng 26946 tài liệu

Mô tả:

ĐẠ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  × LTLlà 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 -