Luận văn: Phương pháp tạo giả định tối thiểu kiểm chứng phần mềm hướng thành phần

Kiểm chứng phần mềm hướng thành phần: Xây dựng giả định tối thiểu để kiểm tra hiệu quả, đảm bảo chất lượng và độ tin cậy của phần mềm.

• Tác giả: Nguyễn Văn Hiếu
• Người hướng dẫn: TS. Lê Anh Cường
• Trường học: Trường Đại Học Công Nghệ - Đại Học Quốc Gia Hà Nội
• Chuyên ngành: Công nghệ phần mềm
• Đề tài: Phương pháp tạo giả định tối thiểu áp dụng để kiểm chứng phần mềm hướng thành phần
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2009
• Địa điểm: Hà Nội

Mục lục chi tiết

• MỤC LỤC
• DANH MỤC CÁC HÌNH VẼ
• DANH MỤC CÁC CHỮ VIẾT TẮT
• 1. CHƯƠNG 1: TỔNG QUAN VỀ KIỂM CHỨNG PHẦN MỀM HƢỚNG THÀNH PHẦN
• 1.1. Các khái niệm cơ bản
• 1.1.1. Labeled Transition System(LTS)
• 1.2. Ghép nối song song(Parallel Composition)
• 1.3. Safety LTSs, Safety Property, error LTS
• 1.4. Ôtomat đơn định hữu hạn trạng thái (Deterministic Finite State Automata)
• 1.5. Về vần đề đảm bảo giả định
• 2. CHƢƠNG 2: TẠO GIẢ ĐỊNH SỬ DỤNG THUẬT TOÁN HỌC L*
• 2.1. Thuật toán học L*
• 2.2. Tạo giả định sử dụng thuật toán học L*
• 3. CHƢƠNG 3: GIẢI THUẬT TẠO GIẢ ĐỊNH TỐI THIỂU
• 3.1. Định nghĩa giả định tối thiểu
• 3.2. Giải thuật tạo giả định tối thiểu
• 3.2.1. Tƣ tƣởng của giải thuật
• 3.2.2. Chi tiết giải thuật tạo giả định tối thiểu
• 3.2.3. Tính dừng và đúng đắn của giải thuật tạo giả định tối thiểu
• 3.2.3.1. Đặc điểm không gian tìm kiếm
• 3.2.3.2. Tính dừng và tính đúng đắn của giải thuật
• 3.3. Ví dụ tạo giả định tối thiểu
• 4. CHƢƠNG 4: THỰC NGHIỆM
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Về Kiểm Chứng Phần Mềm Hướng Thành Phần

Phát triển phần mềm hướng thành phần (CBSD) đã trở thành một kỹ thuật quan trọng trong kỹ nghệ phần mềm. CBSD tập trung vào việc lựa chọn và ghép nối các thành phần riêng biệt để tạo nên một hệ thống hoàn chỉnh. Ưu điểm của CBSD là rút ngắn thời gian phát triển, nâng cao chất lượng và độ tin cậy. Tuy nhiên, việc đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần (Component-Based Software) lại là một thách thức. Các thành phần có thể được phát triển độc lập hoặc từ các nhà cung cấp thứ ba (third parties), dẫn đến khó khăn trong việc kiểm soát lỗi. Các công nghệ hỗ trợ như CORBA, COM/DCOM, .NET hiện tại chưa có cơ chế kiểm tra lỗi khi các thành phần tương tác. Để giải quyết vấn đề này, phương pháp kiểm chứng mô hình (Model checking) được sử dụng. Tuy nhiên, kiểm chứng mô hình gặp phải vấn đề "bùng nổ không gian trạng thái" khi phần mềm có kích thước lớn. Một giải pháp tiềm năng là kiểm chứng từng phần (modular verification - MV), kiểm chứng trên từng thành phần thay vì toàn bộ hệ thống. Kiểm chứng đảm bảo giả định (Assume-Guarantee Verification - AGV) là một phương pháp hỗ trợ ý tưởng này. AGV chia nhỏ bài toán kiểm chứng thành các bài toán con nhỏ hơn. AGV được đánh giá là một phương pháp hứa hẹn cho phần mềm hướng thành phần, có khả năng giải quyết vấn đề bùng nổ không gian trạng thái. Trong phương pháp này, các giả định (assumptions) được tạo ra đóng vai trò như môi trường của các thành phần. Việc tạo lập các giả định chính là bài toán quan trọng nhất. Kích thước của các giả định (số lượng trạng thái) nên được cực tiểu hóa vì chi phí cho quá trình kiểm chứng mô hình phụ thuộc vào thông số này.

1.1. Phát Triển Phần Mềm Hướng Thành Phần CBSD và Thách Thức

CBSD đã được áp dụng rộng rãi, nhưng một trong những hạn chế chính là đảm bảo tính đúng đắn khi các thành phần được ghép nối. Việc các thành phần được phát triển độc lập hoặc từ các công ty thứ ba tạo ra rủi ro về tính tương thích và lỗi tiềm ẩn. Hiện tại, các công nghệ hỗ trợ CBSD như CORBA, COM/DCOM, .NET không cung cấp cơ chế kiểm tra toàn diện, có nghĩa là tính năng 'plug-and-play' không được đảm bảo. Các phương pháp Kiểm thử phần mềm hướng thành phần phải tính đến điều này.

1.2. Giải Pháp Kiểm Chứng Mô Hình và Kiểm Chứng Từng Phần

Để giải quyết vấn đề đảm bảo chất lượng trong CBSD, kiểm chứng mô hình (Model Checking) là một giải pháp. Tuy nhiên, kiểm chứng mô hình đối mặt với vấn đề 'bùng nổ không gian trạng thái' khi kích thước phần mềm tăng lên. Kiểm chứng từng phần (modular verification) là một cách tiếp cận tiềm năng, tập trung vào việc kiểm chứng từng thành phần riêng lẻ thay vì toàn bộ hệ thống. Kiểm chứng đảm bảo giả định (Assume-Guarantee Verification) là một phương pháp hỗ trợ kiểm chứng từng phần. Đây là một phương pháp hứa hẹn để Xác minh phần mềm hướng thành phần

1.3. Tầm Quan Trọng Của Giả Định Tối Thiểu Trong Kiểm Chứng

Trong phương pháp kiểm chứng đảm bảo giả định, việc tạo lập các giả định (assumptions) đóng vai trò quan trọng. Kích thước của các giả định (số lượng trạng thái) cần được cực tiểu hóa vì chi phí của quá trình kiểm chứng mô hình phụ thuộc vào kích thước của giả định. Mục tiêu của nghiên cứu này là đề xuất một phương pháp tạo giả định tối thiểu (Assumption Generation) để cải tiến phương pháp kiểm chứng đảm bảo giả định. Giả định tối thiểu sẽ giảm chi phí kiểm chứng hệ thống.

II. Các Khái Niệm Cơ Bản Về Kiểm Chứng Thành Phần Phần Mềm

Bộ ứng dụng LTSA sử dụng LTSs để mô hình hoá các đặc tính giao tiếp giữa các thành phần. LTS là một đồ thị định hướng với các cạnh được gán nhãn. Tập trạng thái, phép biến đổi và tập nhãn kết hợp tạo nên một hệ thống. Act là tập các hành động có thể kiểm soát, τ là một hành động cục bộ. Một LTS M là một bộ bốn (Q, αM, δ, q0) trong đó: Q là một tập các trạng thái không rỗng. αM là tập các hành động có thể kiểm soát được. q0 là trạng thái ban đầu. δ là hàm chuyển. Một dẫn xuất t của một LTS M là một chuỗi các hành động có thể kiểm soát được. Tập tất cả các dẫn xuất của M gọi là ngôn ngữ đoán nhận M, ký hiệu L(M). Ghép nối song song || là thao tác thực hiện hai hành động thay thế và kết hợp, kết hợp các đặc tính của hai thành phần bằng cách đồng bộ hoá các hành động chung. Một Safety LTS là một LTS hữu hạn không chứa bất kỳ trạng thái lỗi π. Một Safety Property được xác định là một LTS an toàn p. Một error LTS, ký hiệu perr phát sinh trong quá trình kiểm thử LTS M thỏa mãn thuộc tính p. Cách tiếp cận này sử dụng thuật toán học L* để tạo giả định. Deterministic Finite State Automata (DFA) M_i được xây dựng từ bảng quan sát. DFA được định nghĩa như sau: M = <Q, αM, δ, qo, F>.

2.1. Labeled Transition System LTS và Dẫn Xuất Traces

LTS là một công cụ quan trọng để mô hình hóa các đặc tính giao tiếp giữa các thành phần trong hệ thống. Một LTS có thể được biểu diễn như một đồ thị định hướng, trong đó các cạnh được gán nhãn. Dẫn xuất (traces) là một chuỗi các hành động có thể kiểm soát được, và ngôn ngữ của LTS là tập hợp tất cả các dẫn xuất có thể. Hiểu rõ LTS và dẫn xuất là nền tảng cho việc kiểm chứng phần mềm. Điều này liên quan đến Kiểm chứng thành phần phần mềm.

2.2. Ghép Nối Song Song Parallel Composition và Safety Property

Ghép nối song song (Parallel Composition) là một thao tác kết hợp các thành phần bằng cách đồng bộ hóa các hành động chung. Safety LTS là một LTS không chứa trạng thái lỗi. Safety Property được xác định như một LTS an toàn. Để kiểm chứng một thành phần thỏa mãn một thuộc tính, cần biểu diễn cả hai dưới dạng Safety LTS và thực hiện phép ghép nối song song. Một trạng thái lỗi trong kết quả ghép nối cho thấy sự vi phạm thuộc tính. Đây là một kỹ thuật cốt lõi trong Kiểm chứng thành phần phần mềm.

2.3. Ôtomat Đơn Định Hữu Hạn Trạng Thái DFA và Thuật Toán Học L

Cách tiếp cận sử dụng thuật toán học L* để tạo giả định (Assumption Generation). Thuật toán L* sử dụng một Deterministic Finite State Automata (DFA) M_i được xây dựng từ một bảng quan sát. DFA là một mô hình trừu tượng để đoán nhận ngôn ngữ. Việc chuyển đổi từ DFA sang LTS an toàn cho phép áp dụng các kỹ thuật kiểm chứng mô hình. Thuật toán L* đóng vai trò quan trọng trong việc tạo giả định cho Kiểm thử dựa trên thành phần.

III. Vấn Đề Đảm Bảo Giả Định Trong Kiểm Chứng Phần Mềm

Xác minh đảm bảo giả định các phần mềm hướng thành phần là một cách tiếp cận được đưa ra bởi D. Cách tiếp cận này dựa trên tư tưởng của kiểm chứng mô hình giả định. Nó đưa ra một cách tiếp cận đầy hứa hẹn để giải quyết vấn đề xác minh đối với những hệ thống lớn. Cách tiếp cận này dựa trên tư tưởng của chiến lược “Chia để trị”, thuộc tính của hệ thống được biến đổi thành các thuộc tính của các thành phần sau đó thay vì kiểm tra trên toàn hệ thống chúng ta sẽ chỉ cần kiểm tra độc lập trên từng thành phần. Xét một hệ thống đơn giản gồm hai thành phần độc lập M1 và M2. Bài toán quan trọng, cũng là xuyên suốt quá trình nghiên cứu của chúng ta là cần xác minh xem, một hệ thống M1||M2 có thoả mãn một thuộc tính p nào đó hay không? Nếu chúng ta xác minh trên toàn bộ hệ thống M1 || M2, giải pháp này sẽ dẫn tới vấn đề “bùng nổ không gian trạng thái”. Đảm bảo giả định nhằm đưa ra giải pháp nhằm kiểm tra hệ thống M1 || M2 có thoả thuộc tính p hay không mà không cần thực hiện phép ghép nối song song giữa M 1 và M2. Đảm bảo giả định sử dụng tư tưởng của chiến lược “Chia để trị”, phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhưng kích thước nhỏ hơn. Nếu M1 thoả mãn p với một điều kiện nào đó, và M2 cũng thoả mãn điều kiện đó, khi đó hệ thống M gồm M1 và M2 cũng thoả mãn điều kiện p. Điều kiện ở đây được thể hiện bởi các giả định (Assumption). Như vậy để kiểm chứng hệ thống sử dụng phương pháp này, đòi hỏi chúng ta phải xác định được giả định, bài toán này chúng ta sẽ xem xét sau. Ở đây chúng ta giả thiết có một giả định A đã được xác định và thuật toán trên của chúng ta đã được chứng minh là đúng đắn. Giả định A được đưa ra, yêu cầu phải trừu tượng hơn M2 nhưng vẫn thể hiện được các đặc tính của M2. Hơn nữa, giả định phải đủ mạnh để M1 thoả mãn p (Hình 1.5 minh hoạ tổng quan về mục tiêu và giải pháp cho cách tiếp cận xác minh đảm bảo giả định). Như vậy, bài toán kiểm chứng hệ thống M = M1|| M2 có thoả mãn thuộc tính p hay không? Ta đã đưa được về việc giải quyết hai bài toán con: A M1 P và true M 2 A.Để kiểm chứng công thức A M1 P ta thực hiện phép ghép nối song song A||M1||perr. Trong đó, A, M1, p, perr được biểu diễn bởi các LTS. Nếu không có dẫn xuất để trạng thái lỗi xảy ra trong A||M1||perr thì công thức A M1 P thỏa mãn. Hay nói cách khác là A||M1 thỏa p. Ngược lại, A||M1 không thỏa p. Với công thức true M 2 A , kiểm tra xem M2 có thoả mãn thuộc tính A hay không với bất kỳ điều kiện gì của môi trường. Để kiểm chứng công thức này ta chỉ cần thực hiện phép ghép nối M2||A, nếu LTS kết quả không tồn tại một dẫn xuất nào dẫn tới trạng thái lỗi khi đó M2 thoả A, ngược lại M2 không thoả A.

3.1. Phương Pháp Kiểm Chứng Đảm Bảo Giả Định AGV

Kiểm chứng đảm bảo giả định (Assume-Guarantee Verification) là một cách tiếp cận hiệu quả để xác minh phần mềm hướng thành phần. AGV chia nhỏ quá trình xác minh thành các công việc nhỏ hơn trên các thành phần độc lập, thay vì kiểm tra toàn bộ hệ thống. AGV sử dụng các giả định (assumptions) để mô tả môi trường của các thành phần. Để hệ thống M1||M2 thỏa mãn thuộc tính p, cần tìm giả định A sao cho A M1 P và true M 2 A. Cách tiếp cận này giúp giảm thiểu vấn đề bùng nổ không gian trạng thái. Phương pháp này liên quan đến Kiểm chứng thành phần phần mềm.

3.2. Xác Định Giả Định Trong Phương Pháp AGV

Vấn đề chính trong AGV là làm thế nào để tìm ra giả định A. Hiện tại, có hai phương pháp tạo giả định A một cách tự động: (1) Tìm ra giả định yếu nhất Aw. Tuy nhiên, giải pháp này có thể gặp khó khăn nếu hệ thống phức tạp với không gian trạng thái quá lớn. (2) Tạo giả định sử dụng thuật toán học L*. Cách tiếp cận này dựa trên các phản ví dụ và quá trình huấn luyện. Thay vì tìm Aw, ta sử dụng L* để huấn luyện Aw. Cần giảm kích thước của giả định, và AGR chỉ có ý nghĩa khi thời gian tính toán của A||M1 << M1||M2. Bài toán trọng tâm ở đây là Tạo giả định kiểm thử.

3.3. Giả Định Yếu Nhất và Thuật Toán Học L trong Tạo Giả Định

Phương pháp thứ nhất nhằm tìm ra giả định yếu nhất Aw (kích thước lớn nhất). Phương pháp thứ hai, tạo giả định bằng thuật toán L*, tạo ra một giả định có kích thước nhỏ hơn bằng cách sử dụng thuật toán học có tên là L*. Thuật toán này gồm nhiều bước lặp, bắt đầu từ giả định rỗng để đạt được giả định thỏa mãn yêu cầu của AGR. Tuy nhiên, giả định được đưa ra bởi cách tiếp cận này chưa phải là giả định tối thiểu. Mục tiêu là giảm kích thước của các giả định (Minimal Assumptions in Testing).

IV. Thuật Toán Học L Để Tạo Giả Định Cho Thành Phần Phần Mềm

Chương 1 đã trình bày tổng quan về cách tiếp cận xác minh phần mềm hướng thành phần. Một bài toán quan trọng trong kỹ thuật này là tạo ra một giả định. Chương này giới thiệu cách tạo ra một giả định giữa hai thành phần M1 và M2. Giả sử có một tập ký tự ∑ cho trước. Với mỗi ngôn ngữ chính quy U có bảng chữ cái là tập con của ∑, cần tìm một Otomat đơn định tối thiểu hữu hạn trạng thái(DFA) M đoán nhận ngôn ngữ U, tức là L(M) = U. Tư tưởng chính của giải thuật này dựa trên định lý Myhill – Nerode Theorem. Giải thuật học L được phát triển bởi [1] và sau đó được cải tiến bởi Rivest và Schapire [24]. Trong luận văn này, giải thuật L* được trình bày với cùng tên. Dựa trên tư tưởng học, giải thuật L* sẽ thực hiện xây dựng dần dần từng bước nghiệm của bài toán. Để huấn luyện U, L* cần thiết phải kết hợp với Minimally Adequate Teacher, từ bây giờ chúng ta sẽ gọi là Teacher (người huấn luyện).

4.1. Tổng Quan Về Thuật Toán Học L và Ứng Dụng

Thuật toán học L* là một thuật toán quan trọng để tạo giả định trong kiểm chứng phần mềm hướng thành phần (Component Verification). Thuật toán L* tìm một Otomat đơn định tối thiểu hữu hạn trạng thái (DFA) M đoán nhận ngôn ngữ U. Thuật toán này dựa trên định lý Myhill-Nerode Theorem và được cải tiến bởi Rivest và Schapire. L* kết hợp với Minimally Adequate Teacher để huấn luyện và đưa ra nghiệm của bài toán. Phương pháp này hỗ trợ Kiểm thử dựa trên thành phần.

4.2. Truy Vấn Kiểm Tra Thành Viên và Kiểm Tra Phỏng Đoán

Để huấn luyện U, L* cần thiết phải kết hợp với Teacher (người huấn luyện). Teacher trả lời chính xác hai loại câu hỏi từ L*: (1) Kiểm tra thành viên (Membership query): với một chuỗi  * , câu trả lời là true nếu  U và false nếu ngược lại. (2) Loại câu hỏi thứ hai: kiểm tra sự phỏng đoán: với mỗi ứng cử viên DFA M, khi đó, ngôn ngữ của nó có đồng nhất với U hay không? Câu trả lời là true nếu L(M) = U, ngược lại, Teacher sẽ đưa ra một phản ví dụ để minh chứng cho sự khác nhau giữa L(M) và U. Các truy vấn này giúp L* học ngôn ngữ của Thành phần phần mềm tin cậy.

4.3. Bảng Quan Sát và Quá Trình Xây Dựng DFA Trong L

L* sử dụng một bảng T để ghi lại kết quả kiểm tra một chuỗi s * có thuộc vào U hay không? Bảng quan sát T được cập nhật mỗi khi có sự thay đổi bởi các thao tác kiểm tra thành viên. Ôtomat hữu hạn Mi được xây dựng dựa trên bảng T, và khi đó với mỗi Mi, các nhà huấn luyện sẽ quyết định xem sự phỏng đoán đó có đúng hay không? Nếu phỏng đoán là chính xác, thuật toán sẽ dừng ở đây, ngược lại, L* sử dụng phản ví dụ mà nhà huấn luyện trả lại để cập nhật lại bảng T. Các phản ví dụ giúp L* cải thiện giả định trong Kiểm thử dựa trên mô hình.

V. Giải Thuật Tạo Giả Định Tối Thiểu Cho Kiểm Chứng

Xét hệ thống gồm 2 thành phần C1, C2, và một thuộc tính p. Nhiệm vụ là xác định công thức sau: C1 || C2 ╞ p có được thoả mãn hay không mà không cần thực hiện phép ghép nối C1 || C2. Để thực hiện được điều này, giải thuật yêu cầu tạo một giả định A(p) đủ mạnh để C1 thoả mãn p nhưng đủ yếu để vẫn được đảm bảo bởi C2. Hiện tại có hai giải pháp để giải quyết bài toán này: Thứ nhất, thuật toán (non-incremental): Nhằm tìm ra một giả định yếu nhất Aw. Tuy nhiên, vấn đề này sẽ gặp khó khăn nếu hệ thống với không gian trạng thái rất lớn. Thứ hai, tạo giả định sử dụng giải thuật L*. Cách tiếp cận incremental, dựa trên các phản ví dụ và quá trình huấn luyện.

5.1. Mục Tiêu Tạo Giả Định Tối Thiểu Trong Kiểm Chứng

Mục tiêu là tạo giả định A(p) đủ mạnh để C1 thoả mãn p nhưng đủ yếu để C2 vẫn đảm bảo (Assumptions and Guarantees (Contracts)). Có hai giải pháp: (1) tìm giả định yếu nhất Aw (kích thước lớn) nhưng gặp khó khăn với không gian trạng thái lớn; (2) sử dụng thuật toán L* (incremental). Ưu tiên giả định nhỏ hơn Aw. Cần tạo các Contracts in Component-Based Systems.

5.2. Quy Trình Tạo Giả Định Sử Dụng L và Luật Ghép Nối

Tại mỗi vòng lặp, mỗi giả định kiểm tra Ai sẽ được xử lý dựa trên thông tin về môi trường và kết quả bước lặp trước. Đầu tiên, giải thuật học L* xác định DFA Mi dựa trên bảng quan sát. Tiếp theo, Teacher kiểm tra xem ngôn ngữ được đoán nhận bởi Mi có đồng nhất với AW hay không? Nếu kết quả true, giải thuật L* biến đổi DFA Mi thành LTS an toàn Ai. Sau đó, LTS Ai được xem như một ứng cử viên đầu vào cho luật ghép nối. Cần có Phương pháp kiểm chứng phần mềm hiệu quả.

5.3. Phân Tích Phản Ví Dụ và Cải Tiến Giả Định Trong L

Nếu giả định Ai không thoả mãn bước thứ nhất của luật ghép nối, giải thuật phân tích phản ví dụ (cex) để tìm hậu tố e. Sau đó, e được thêm vào tập Ei của bảng quan sát OTi. Ngược lại, nếu bước thứ nhất thỏa mãn, giải thuật kiểm tra bước thứ hai của luật ghép nối. Nếu bước hai không thỏa mãn, giải thuật phân tích cex để xác định xem có phải hệ thống không thỏa mãn thuộc tính p hay giả định Ai quá mạnh. Cần xác định Giả định tối thiểu trong kiểm thử.

VI. Giải Thuật Tạo Giả Định Tối Thiểu Cải Tiến L Cho CBST

Xét một hệ thống đơn giản gồm hai thành phần độc lập M1 và M2. Cần xác minh hệ thống ghép nối song song M1||M2 có thoả mãn thuộc tính p cho trước hay không? Đảm bảo giả định đưa ra giải pháp để kiểm tra hệ thống M1 || M2 có thoả thuộc tính p hay không mà không cần thực hiện phép ghép nối song song giữa M 1 và M2. Tuy nhiên, để xác minh hệ thống sử dụng phương pháp đảm bảo giả định, đòi hỏi chúng ta phải xác định được giả định A. Mặt khác, không phải giả định nào cũng có thể chấp nhận được. Chúng ta cần phải xác định được giả định tối thiểu, vì kích thước của giả định A là rất quan trọng. Chúng ta xét một ví dụ cụ thể để minh chứng cho điều này. Xét hệ thống gồm các thành phần sau: Input, Output, Ordererr. Tuy nhiên, tồn tại một giả định A’ nhƣ sau. Dễ dàng kiểm tra được các biểu thức sau là đúng: A’ Input Order và true Output A’. Mặt khác, ta có |A’| = 2 < 4 = |A|. Nhƣ vậy, giả định được tạo ra bởi giải thuật L* chưa phải là giả định tối thiểu.

6.1. Tầm Quan Trọng Của Giả Định Tối Thiểu Trong CBST

Trong kiểm thử phần mềm dựa trên thành phần (Component-Based Software Testing - CBST), việc sử dụng giả định tối thiểu (Minimal Assumptions in Testing) giúp giảm chi phí và độ phức tạp. Giả định tối thiểu đảm bảo tính hiệu quả của quá trình kiểm chứng và dễ hiểu hơn. Giải thuật L* trong [1] không phải lúc nào cũng đưa ra giả định tối thiểu. Cần có Phương pháp kiểm chứng phần mềm hiệu quả.

6.2. Phản Ví Dụ Chứng Minh L Không Tạo Giả Định Tối Thiểu

Một phản ví dụ cho thấy giải thuật L* có thể tạo ra giả định A không tối thiểu. Tồn tại một giả định A' có kích thước nhỏ hơn (|A'| < |A|) và vẫn thỏa mãn các điều kiện của AGV. Do đó, cần có một giải thuật cải tiến để tạo giả định tối thiểu. Cần tập trung vào Tạo giả định kiểm thử hiệu quả.

6.3. Cải Tiến Giải Thuật L Để Tạo Giả Định Tối Thiểu

Giải thuật L* sử dụng một phương pháp học ngôn ngữ của giả định yếu nhất AW. Để giải quyết hạn chế này, chúng tôi sử dụng một giá trị mới gọi là “?” để gán cho giá trị của T(s) trong trƣờng hợp trên. Câu trả lời cho câu hỏi kiểm tra thành viên được cải tiến như sau: chuỗi s = a1, a2, . giải thuật học L* cải tiến sẽ xây dựng một bảng quan sát (S, E, T), trong đó S và E tương ứng là tập tiền tố và hậu tố. T là một hàm thực hiện ánh xạ tập (S  S. Giải pháp Tạo giả định kiểm thử tối thiểu cần được tìm.

Trích đoạn nội dung tài liệu

MỞ ĐẦU Phát triển phần mềm hƣớng thành phần (Component-Based Software Development - CBSD) là một trong những công nghệ quan trọng nhất trong kỹ nghệ phần mềm. Hệ thống phần mềm hƣớng thành phần đƣợc xây dựng dựa trên quá trình lựa chọn và ghép nối các thành phần riêng biệt thành một hệ thống hoàn chỉnh. Với cách tiếp cận này, phát triển phần mềm hƣớng thành phần đã góp phần rút ngắn thời gian thực hiện dự án, nâng cao chất lƣợng và độ tin cậy của sản phầm. Vì những ƣu điểm này mà công nghệ này đã đƣợc áp dụng rộng rãi trong quá trình phát triển các dự án phần mềm hiện nay.

Tuy nhiên, một trong những hạn chế của CBSD là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với nhau vì các thành phần có thể đƣợc phát triển một cách độc lập hoặc đƣợc đặt mua từ các công ty thứ 3 (third parties). Hiện tại, các công nghệ hỗ trợ phát triển phần mềm hƣớng thành phần nhƣ CORBA (OMG), COM/DCOM or. Chúng không có cơ chế kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với nhau hay không. Điều này có nghĩa là cơ chế “plug-and-play” không đƣợc đảm bảo.

Một trong những giải pháp phổ biến để giải quyết vấn đề nêu trên là sử dụng các phƣơng pháp kiểm chứng mô hình (Model checking). Tuy nhiên, một trong những hạn chế lớn nhất của kiểm chứng mô hình là vấn đề bùng nổ không gian trạng thái khi kiểm chứng các phần mềm có kích thƣớc lớn. Một trong những cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần (modular verification - MV). Thay vì tiến hành kiểm chứng trên toàn bộ hệ thống gồm các thành phần đƣợc ghép nối với nhau, cách tiếp cận này tiến hành kiểm chứng trên từng thành phần riêng biệt.

Với cách tiếp cận này, vấn đề bùng nổ không gian trạng thái hứa hẹn sẽ đƣợc giải quyết. Một trong những phƣơng pháp kiểm chứng hỗ trợ ý tƣởng này là phƣơng pháp kiểm chứng đảm bảo giả định (Assume-Guarantee Verification - AGV). Sử dụng tƣ tƣởng của chiến lƣợc “chia để trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhƣng kích thƣớc nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách riêng biệt. AVG đƣợc đánh giá là một phƣơng pháp hứa hẹn để kiểm chứng phần mềm hƣớng thành phần thông qua phƣơng pháp kiểm chứng mô hình.

AVG không những thích hợp cho phần mềm hƣớng thành phần mà còn có khả TIEU LUAN MOI download : [e-mail] 5 năng giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình. Trong phƣơng pháp này, các giả định (assumptions) (có vai trò nhƣ là môi trƣờng của các thành phần) sẽ đƣợc tạo lập. Việc tạo lập các giả định chính là bài toán quan trọng nhất trong phƣơng pháp này. Kích thƣớc của các giả định này (số lƣợng trạng thái) nên đƣợc cực tiểu hóa bởi vì chi phí cho quá trình kiểm chứng mô hình của phƣơng pháp này phụ thuộc chính vào thông số này.

Đây chính là mục tiêu nghiên cứu của luận văn này. Với mục tiêu này, chúng tôi đề xuất một phƣơng pháp tạo giả định tối thiểu (có kích thƣớc nhỏ nhất) nhƣ là một cải tiến của phƣơng pháp kiểm chứng đảm bảo giả định nhƣ đã trình bày ở trên. Ý tƣởng chính của phƣơng pháp đề xuất là tìm kiếm giả định tối thiểu trên toàn bộ không gian tìm kiếm của các ứng cử viên giả định (candidate assumptions). Giả định tối thiểu sau khi tạo lập bằng phƣơng pháp đề xuất sẽ đƣợc sử dụng để kiểm chứng lại hệ thống với chi phí thấp hơn.

Một số ví dụ minh họa và kết quả thực nghiệm cũng đƣợc trình bày trong luận văn này. Bố cục của luận văn đƣợc trình bày nhƣ sau: Chƣơng 1: Giới thiệu tổng quan phần mềm hƣớng thành phần, các khái niệm cơ bản, cách tiếp cận để kiểm chứng phần mềm hƣớng thành phần. Chƣơng 2: Trình bày chi tiết thuật toán học L*, giải thuật tạo giả định sử dụng thuật toán học L*. Chƣơng 3: Chƣơng này trình bày giải thuật tạo giả định tối thiểu.

Trong chƣơng này chúng tôi sẽ đƣa ra một phản ví dụ để minh hoạ rằng: giả định đƣợc tạo ra bởi giải thuật sử dụng thuật toán học L* chƣa phải là giả định tối thiểu. Chúng tôi cũng sẽ trình bày một ví dụ cụ thể để minh hoạ cho thuật toán tạo giả định tối thiểu. Chƣơng 4: Thực nghiệm. Chúng tôi sử dụng bộ công cụ LTSA để xác minh một số hệ thống đơn giản nhằm so sánh về thời gian cũng nhƣ bộ nhớ sử dụng của giải pháp cũ và giải pháp đƣợc đƣa ra trong luận văn.

Phần kết luận của luận văn tổng kết các kết quả đã đạt đƣợc, kết luận và đƣa ra một số hƣớng nghiên cứu tiếp theo. TIEU LUAN MOI download : [e-mail] 6 CHƢƠNG 1: TỔNG QUAN VỀ KIỂM CHỨNG PHẦN MỀM HƢỚNG THÀNH PHẦN 1.1 Giới thiệu Quá trình phát triển phần mềm hƣớng thành phần đƣợc biết đến là sự phát triển phần mềm bằng cách ghép nối các phần độc lập. Đây là một trong những kỹ thuật quan trọng nhất trong kỹ nghệ phần mềm. Cách tiếp cận này vẫn đang thu hút sự chú ý trong cộng đồng kỹ nghệ phần mềm và đƣợc xem là một cách tiếp cận mở, hiệu quả, giảm thời gian và chi phí phát triển đồng thời tăng chất lƣợng của phần mềm.

Đã có rất nhiều khái niệm, kỹ thuật đề xuất nhằm phát triển cho ý tƣởng này. Tuy nhiên, một trong những hạn chế của phát triển phần mềm hƣớng thành phần là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với nhau vì các thành phần có thể đƣợc phát triển một cách độc lập hoặc đƣợc đặt mua từ các công ty thứ 3 (third parties). Hiện tại, các công nghệ hỗ trợ phát triển phần mềm hƣớng thành phần nhƣ CORBA (OMG), COM/DCOM or. Chúng không có cơ chế kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với nhau hay không.

Điều này có nghĩa là cơ chế “plug-and-play” không đƣợc đảm bảo. Một giải pháp phổ biến hiện nay để giải quyết cho vấn đề trên là áp dụng kiểm chứng mô hình (model checking - MC) [5]. Kiểm chứng mô hình là một cách tiếp cận quan trọng để giải quyết bài toán chứng minh độ tin cậy của phần mềm. Nó cũng tạo ra một không gian trạng thái chi tiết có thể bao phủ đƣợc các hệ thống đang đƣợc kiểm tra đồng thời đạt đƣợc hiệu quả đặc biệt trong quá trình dò các lỗi tổng hợp khá phức tạp mà nguyên nhân chủ yếu do quá trình ghép nối các thành phần gây nên.

Tuy nhiên, một trong những hạn chế lớn nhất của kiểm chứng mô hình là “vấn đề bùng nổ không gian trạng thái” khi kiểm chứng các phần mềm có kích thƣớc lớn. Một trong những cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần (modular model checking - MMC) [10, 11]. Thay vì tiến hành kiểm chứng trên toàn bộ hệ thống gồm các thành phần đƣợc ghép nối với nhau, cách tiếp cận này tiến hành kiểm chứng trên từng thành phần riêng biệt. Với cách tiếp cận này, vấn đề bùng nổ không gian trạng thái hứa hẹn sẽ đƣợc giải quyết.

Một trong những phƣơng pháp kiểm chứng hỗ trợ ý tƣởng này là phƣơng pháp kiểm chứng đảm bảo giả định (Assume- TIEU LUAN MOI download : [e-mail] 7 Guarantee Verification - AGV) [2, 4, 7, 8]. Sử dụng tƣ tƣởng của chiến lƣợc “chia để trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhƣng kích thƣớc nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách riêng biệt. AVG đƣợc đánh giá là một phƣơng pháp hứa hẹn để kiểm chứng phần mềm hƣớng thành phần thông qua phƣơng pháp kiểm chứng mô hình. AVG không những thích hợp cho phần mềm hƣớng thành phần mà còn có khả năng giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình.

Trong phƣơng pháp này, các giả định (assumptions) (có vai trò nhƣ là môi trƣờng của các thành phần) sẽ đƣợc tạo lập. Việc tạo lập các giả định chính là bài toán quan trọng nhất trong phƣơng pháp này. Mục tiêu chính của cách tiếp cận này là nhằm kết hợp tốt nhất giữa lợi thế của hai phần: kiểm chứng mô hình và phát triển hƣớng thành phần. Hiện nay, đã có nhiều nghiên cứu về kiểm chứng mô hình từng phần cho phần mềm hƣớng thành phần (modular verification of component based software) [2, 4, 7, 8, 10, 11, 22].

Mỗi khi thêm một thành phần nào đó vào hệ thống, thì toàn bộ hệ thống gồm các thành phần đang tồn tại và thành phần mới phải đƣợc kiểm chứng lại. Vì thế, đối với những phần mềm phức tạp, vấn đề “bùng nổ không gian trạng thái” có thể xảy ra khi ấp dụng các phƣơng pháp trong các nghiên cứu này. Cách tiếp cận trong [2, 4, 7, 8] đề xuất phƣơng pháp kiểm chứng đảm bảo giả định nhƣ đã trình bày ở trên. Xét một hệ thống đơn giản gồm hai phần M1 và M2.

Mục đích của cách tiếp cận này là kiểm chứng hệ thống này thoả mãn một thuộc tính p mà không cần đến việc ghép nối giữa các thành phần với nhau. Dựa trên tƣ tƣởng này, AGV tìm ra một giả định A sao cho nó đủ mạnh cho M1 thoả mãn p và đủ yếu để nó đƣợc thỏa mãn bởi M2. Nếu tìm đƣợc một giả định A thỏa mãn các điều kiện trên thì hệ thống khi ghép nối M1||M2 sẽ thoả mãn thuộc tính p. Tuy nhiên, cách tiếp cận này không đề cập đến việc kiếm chứng hệ thống trong ngữ cảnh của tiến hóa thành phần phền mềm.

Nếu một thành phần bị tiến hóa sau khi thực hiện một vài thay đổi, khi đó giải pháp này sẽ phải thực hiện kiểm chứng hệ thống nhƣ một hệ thống mới. Trong khi đó việc thay đổi chỉ xảy ra ở một vài thành phần nên việc chạy lại trên toàn bộ hệ thống là không cần thiết. Để giải quyết hạn chế này, giải pháp trong [25] đã đề xuất một cách tiếp nhằm tạo lại giả định nhanh hơn trong ngữ cảnh các thành phần bị tiến hóa (thay đổi). Giả sử tồn tại một thành phần M1 có trƣớc (thành phần này không đƣợc phép thay đổi) và một phần mở rộng M2 (thành phần này đƣợc phép thay đổi).

Phần mở rộng M2 đƣợc ghép nối với TIEU LUAN MOI download : [e-mail] 8 thành phần M1 bởi một vài cơ chế nào đó. Đầu tiên, chúng ta giả thiết rằng hệ thống chứa M1 và M2 thoả mãn thuộc tính p (tức là, M1||M2╞ p).