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

- Kiểm chứng từng phần cho chương trình C.
- Trình bày các khái niệm cơ bản liên quan như các khái niệm về mô hình chuyển trạng thái được gán nhãn Hệ chuyển trạng thái 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 Trìu tượng hóa thủ tục (PA), cũng như các khái niệm cần thiết trong kĩ thuật kiểm chứng … Trình bày nội dung chính của Kiểm thử từng phần cho chương trình C: 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 dựng sơ đồ luồng xử lý Otomat luồng điều khiển (CFA);.
- sơ đồ luồng xử lý mở rộng (Expanding Control flow Automata) của chương trình có sử dụng các LTS giả thiết.
- Kiểm chứng mô hình.
- 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 đó.
- Việc kiểm chứng theo mô hình một chương trình như vậy sẽ gặp khó khăn và phức tạp vì hoặc có thể chúng ta chưa có được đầy đủ mã nguồn của các thư viện hàm hoặc dễ gây ra bùng nổ không gian trạng thái.
- Trong luận văn này tôi xin giới thiệu một phương pháp mới 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..
- 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].
- 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, 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 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.
- Đầ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.
- 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.
- Định nghĩa 2.1: Hệ thống chuyển trạng thái được gán nhãn (Labeled Transition System – LTS[4]).
- Một hệ chuyển trạng thái được gán nhãn M là một bộ có thứ tự gồm 4 thành phần trong đó:.
- S là một tập khác rỗng các trạng thái của M.
- là trạng thái khởi tạo.
- là hàm chuyển trạng thái.
- Ta kí hiệu nếu có một hành động 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.
- 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.
- Ở trên là một ví dụ về hệ chuyển trạng thái được gán nhãn M.
- S0 là trạng thái khởi đầu..
- Định nghĩa 2.2: 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 = là một chuỗi hữu hạn các hành động với , (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.
- Một dẫn xuất = a1a2..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.
- Ta nói rằng một hành động a đượ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ương tự vậy ta nói rằng một dẫn xuất a1a2 …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.
- Cho một dẫn xuất = và hai trạng thái s, t của hệ chuyển trạng thái được gán nhãn M.
- Ta nói rằng t có thể đi đến được từ s thông qua dẫn xuất (viết là ) nếu tồn tại một tập các trạng thái với s = và t = sao cho.
- Để 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ục đích chính của chúng ta là cần phải kiểm chứng xem phần cài đặt mã nguồn của một chương trình C có thõa mãn với đặc tả của nó (được biểu diễn bằng một LTS) hay không? Để làm được việc đó thì trước hết từ phần cài đặt chúng ta phải xây dựng được một mô hình (biểu diễn bằng một LTS) mô tả hành vi của phần cài đặt, sau đó sử dụng kĩ thuật kiểm chứng để kiểm định sự thõa mãn của với.
- 3.1 Xây dựng mô hình.
- Cho một chương trình C và một tập các mệnh đề logic (predicates) P, hệ trạng thái được gán nhãn.
- là đặc tả của chương trình và các PAs giả thiết .
- Trong phần này sẽ trình bày cách xây dựng từ mã nguồn của chương trình bằng cách sử dụng các PA giả thiết, các điều kiện (Guard) và tập một các mệnh đề logic P.
- Mỗi trạng thái của được mô hình từ một trạng thái của chương trình trong quá trình thực hiện, vì vậy mỗi trạng thái sẽ bao gồm một thành phần điều khiển (control component) và một thành phần dữ liệu (data component)..
- Thành phần dữ liệu là đại diện trừu tượng cho trạng thái các biến của chương trình, được tính toán dựa trên tập các mệnh đề logic P..
- Các bước chuyển trạng thái trên tương ứng với các bước chuyển trạng thái trên CFA..
- Việc xây dựng mô hình từ mã nguồn của một chương trình C bắt đầu bằng việc xây dựng otomat luồng điều khiển (CFA) của chương trình theo nguyên tắc:.
- Mỗi trạng thái của CFA là một điểm điều khiển (control location) trong chương trình (tương ứng với một câu lệnh trong chương trình)..
- Mỗi bước chuyển trạng thái trong CFA tương ứng với một bước chuyển giữa hai điểm điều khiển (hai câu lệnh) trong chương trình..
- Định nghĩa 3.1: CFA của một chương trình C.
- CFA của một chương trình là một bộ gồm 4 thành phần trong đó:.
- là tập các trạng thái..
- là trạng thái khởi tạo..
- là tập các chuyển đổi trạng thái..
- là hàm gán nhãn các trạng thái của CFA..
- {Final} là trạng thái kết thúc duy nhất của CFA.
- Như vậy CFA là mô hình đơn giản nhất của chương trình tuy nhiên nó chỉ mới mô hình được luồng điều khiển của chương trình mà chưa trừu tượng hóa được dữ liệu các biến tại các trạng thái của chương trình.
- Mô hình otomat luồng điều khiển mở rộng là sự kết hợp giữa mỗi trạng thái s của CFA với một tập con của Exp thu được từ P gọi là (P thường là các điều kiện rẽ nhánh trong chương trình).
- trạng thái trong CFA sẽ tương ứng với trạng thái trong CFA mở rộng.
- Với mỗi trạng thái trong CFA, chúng ta bổ sung trạng thái trong , mỗi trạng thái trong CFA mở rộng là tổ hợp trạng thái trong CFA và giá trị của tập các mệnh đề logic đang xem xét..
- Lúc đó mỗi và sẽ tương ứng với trạng thái trong tập các trạng thái .
- Như vậy có khả năng chuyển đổi trạng thái tương ứng trong .
- Tuy nhiên không phải tất cả các khả năng chuyển trạng thái đều thuộc .
- Chúng ta cũng sẽ chỉ loại bỏ những chuyển trạng thái nào bị loại trừ bởi theorem prover..
- Gọi π là một chương trình C và P là một tập các mệnh đề logic (predicates) của các biến trong π, ta kí hiệu A(π,P) là một mô hình trừu tượng của π theo P (hay A(π,P) chính là CFA mở rộng của π).
- Như ta đã biết thì CFA là mô hình đơn giản nhất của một chương trình và từ cách xây dựng CFA ta có thể thấy CFA tương đương với A(π,.
- Mô hình A(π,P) là sự kết hợp giữa mỗi trạng thái s của CFA với một tập con của Exp thu được từ P, gọi là .
- Inference sau đây với chú ý là nếu s là trạng thái kết thúc Final hoặc là một lệnh return và P là một tập con của các lệnh rẽ nhánh trong π..
- Output: Tập các được kết hợp với tương ứng từng trạng thái s trong CFA của π..
- Trạng thái và tập các bước chuyển trạng thái trong mô hình.
- Mỗi trạng thái của mô hình A(π,P) (hay trong CFA mở rộng) sẽ tương ứng với một trạng thái trong CFA kết hợp với tập các giá trị của tập mệnh đề logic tại các trạng thái đó..
- Cho một CFA của một chương trình và một trạng thái s trên CFA đó, giả sử thì giá trị của là một véc tơ kiểu Boolean .
- Việc xây dụng các bước chuyển trạng thái trong mô hình yêu cầu phải sử dụng theorem prover.
- Như vậy với CFA của một chương trình là ta có thể định nghĩa CFA mở rộng (hay mô hình A(π,P)) như sau đây.
- là tập các trạng thái khởi tạo..
- là tập các bước chuyển đổi trạng thái và được xây dựng như.
- là lệnh return và là trạng thái kết thúc (FINAL)..
- 3.2 Kiểm chứng.
- Như vậy chúng ta đã trình bày cách xây dựng mô hình LTS từ mã nguồn của một chương trình C.
- Giả sử có 2 hệ chuyển trạng thái được gán nhãn là M1= (S1, S01, Act1, T1) và M2=.
- Theo các quy tắc trên ta xác định được hệ chuyển trạng thái song song được gán nhãn M.
- Chúng ta tiến hành loại bỏ tất cả các trạng thái không đến được từ trạng thái khởi tạo (0,a) và tất cả các hành động đưa hệ thống về trạng thái đó ta sẽ thu được một hệ thống chuyển trạng thái ghép nối song song được gán nhãn M = (S, S 0 , Act, T) trong đó:.
- 3.2.2 Kiểm chứng tính đúng đắn của chương trình Định nghĩa 3.2: Hệ chuyển trạng thái được gán nhãn an toàn.
- Hệ chuyển trạng thái được gán nhãn an toàn là một hệ chuyển trạng thái được gán nhãn không chứa bất kỳ một trạng thái lỗi π nào..
- Một thuộc tính an toàn p được biểu diễn dưới dạng một hệ chuyển trạng thái được gán nhãn an toàn p = (S p , S 0p , Act p , T p.
- Định nghĩa 3.4: Hệ chuyển trạng thái được gán nhãn lỗi.
- Hệ chuyển trạng thái được gán nhãn lỗi của một thuộc tính p = (S p , S 0p , Act p , T p.
- Ví dụ 3.7: Xây dựng hệ chuyển trạng thái được gán nhãn lỗi từ một hệ chuyển trạng thái ứng với thuộc tính p.
- Một hệ chuyển trạng thái được gán nhãn M được gọi là thỏa mãn thuộc tính p, ký hiệu M╞ p khi và chỉ khi.
- Nếu LTS thu được sau phép ghép nối tồn tại một dẫn xuất có thể tới trạng thái lỗi π, khi đó ta nói thành phần vi phạm thuộc tính p..
- Trong các phần trước của luận văn đã đề cập phương pháp kiểm chứng mô hình cho một chương trình viết bằng ngôn ngữ C, trong chương này chúng ta sẽ tìm hiểu một vài ví dụ ứng dụng thực tế của phương pháp trên công cụ có tên là Copper..
- Copper là một công cụ kiểm chứng tự động mã nguồn một chương trình C được phát triển bởi một nhóm tác giả của viện nghiên công nghệ phần mềm (SEI) của trường đại học Carnegie Mellon University (CMU)..
- Đầu vào của Copper là một file chứa mã nguồn C của chương trình và một file đặc tả của nó.
- File đặc tả sẽ cung cấp thông tin về các LTS của các hàm thư viện được dùng trong chương trình (kể cả các hàm không có mã nguồn) cũng như các LTS của thuộc tính cần kiểm chứng.
- Chúng ta xem xét một chương trình C đơn giản như trong ví dụ 2.4..
- Như vậy trong hành vi của 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 máy trạng thái đơn giản như sau:.
- Hình 4.2: LTS miêu tả hành vi của chương trình.
- Công cụ Copper sử dụng khái niệm FSP mở rộng để đặc tả máy trạng thái.
- Như vậy máy trạng thái ở trên có thể được đặc tả như sau:.
- Lưu chương trình C ở trên vào một file có đuôi là “.pp”, ví dụ như là my_proc.pp.
- Xem xét chương trình C như sau.
- Luận văn tập trung vào nghiên cứu phương pháp kiểm chứng mô hình một chương trình C từ mã nguồn và ứng dụng thực tiễn của phương pháp trên công cụ kiểm chứng tự động Copper..
- Chương 1 và chương 2 trình bày ngữ cảnh và các khái niệm cơ sở của đề tài như các khái niệm về hệ chuyển trạng thái, phương thức trừu tượng hóa hành vi PA của một hàm…