đặt vấn đề cho việc kiểm thử hộp đen. Trong nghiên cứu này, nhiều chiến lƣợc đƣợc trình bày để kiểm chứng phần mềm từ khi chúng ta chƣa có mô hình. Mô hình đƣợc sinh ra trong các lần lặp kiểm chứng phần mềm. Nghiên cứu [25] trình bày một phƣơng pháp sinh mô hình thành phần phần mềm trong quá trình thành phần đó tiến hóa.
Những mô hình này đƣợc sinh ra sử dụng các mô hình chƣa đúng hiện có dựa vào các kỹ thuật kiểm thử hộp đen và học máy. Tuy nhiên, phƣơng pháp này sinh mô hình cho toàn bộ phần mềm. Với những phần mềm lớn thì phƣơng pháp này có thể dẫn đến sự bùng nổ trạng thái của mô hình. Với cách tiếp cận này, những mô hình đƣợc sinh ra nhƣ là một phần của quá trình khác nhƣ kiểm thử hộp đen, kiểm chứng mô hình.
Luận văn này tập trung vào việc chỉ sinh mô hình cho thành phần phần mềm. Bằng cách này, chúng ta tập trung vào việc có đƣợc mô hình bằng một cách thực tế hơn nhƣ từ biểu đồ tuần tự [23]. Những mô hình này sau đó có thể đƣợc dùng nhƣ là đầu vào cho các phƣơng pháp khác nhƣ kiểm chứng mô hình, kiểm thử dựa trên mô hình. Để giải quyết vấn đề trên, trong luận văn này, tôi nghiên cứu về phƣơng pháp nhằm xây dựng một công cụ hỗ trợ phân tích biểu đồ dòng điểu khiển dựa trên biểu đồ tuần tự UML 2.0 và ứng dụng để sinh bộ kiểm thử.
3 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Phƣơng pháp nghiên cứu gồm hai quá trình chính là chuyển đồi biểu đồ tuần tự về đồ thị dòng điều khiển và từ đồ thị dòng điều khiển sinh bộ kiểm thử. Biểu đồ tuần tự đƣợc cung cấp dƣới dạng tệp xmi sẽ đƣợc phân tích để cho ra một đƣờng kiểm thử tƣơng ứng đặc tả hoạt động. Đây chính là giá trị đầu vào. Qua quá trình phân tích, dữ liệu từ tệp xmi đƣợc chuyển đổi thành cấu trúc dữ liệu biểu đồ tuần tự tƣơng ứng.
Ứng với mỗi khối trong biểu đồ tuần tự, tiến hành bóc, tách từng khối và dựa vào quan hệ giữa các khối để lồng các khối nhằm sinh ra đồ thị dòng điều khiển. Kế tiếp, một đƣờng kiểm thử tƣơng ứng đƣợc trả về đặc tả chính xác hoạt động của đồ thị dòng điều khiển. Kỹ thuật đƣợc sử dụng để xây dựng hệ ràng buộc tƣơng ứng cho tập đƣờng kiểm thử ở đây là thực thi tƣợng trƣng (symbolic execution - SE). Cuối cùng, bằng cách kết hợp kỹ thuật sinh ngẫu nhiên và tận dụng thế mạnh các công cụ giải các hệ ràng buộc (SMT-Solver), hệ ràng buộc đƣợc giải để sinh ca kiểm thử.
Bộ kiểm thử này sẽ đƣợc sử dụng để kiểm tra xem việc lập trình có đúng với thiết kế hay không. Phần còn lại của luận văn đƣợc cấu trúc nhƣ sau: Chƣơng 2 trình bày cơ sở lý thuyết của kiểm thử mô hình, bao gồm các khái niệm cơ bản, quy trình thực hiện, phƣơng pháp đặc tả mô hình bằng máy trạng thái UML, thuận lợi và khó khăn của kiểm thử dựa trên mô hình và áp dụng cho kiểm thử phần mềm. Phƣơng pháp sinh đồ thị dòng điều khiển từ biểu đồ tuần tự bao gồm tổng quan về đồ thị dòng điều khiển, cách đặc tả biểu đồ tuần tự, phƣơng pháp sinh đồ thị dòng điều khiển đƣợc trình bày trong chƣơng 3. Chƣơng 4 trình bày về phƣơng pháp sinh ca kiểm thử từ đồ thị dòng điều khiển bao gồm bƣớc xây dựng hệ ràng buộc và bƣớc tìm nghiệm thỏa mãn hệ ràng buộc dựa trên SMT - Solver.
Chƣơng 5 trình bày kết quả đã đạt đƣợc. Cuối cùng, chƣơng 6 tóm tắt lại nội dung nghiên cứu, đƣa ra những hạn chế và hƣớng nghiên cứu phát triển trong tƣơng lai. 4 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chƣơng 2. TỔNG QUAN KIỂM THỬ DỰA TRÊN MÔ HÌNH Khi chạy một dự án phần mềm, yêu cầu từ phía khách hàng là yếu tố để hình thành và phát triển dự án.
Thực tế, các yêu cầu này thƣờng không ổn định mà sẽ thay đổi tùy theo nhu cầu của khách hàng. Mỗi khi có sự thay đổi xảy ra, thƣờng sẽ kéo theo những thứ khác ảnh hƣởng. Vì thế, hoạt động kiểm thử phải thực hiện để đảm bảo chất lƣợng của sản phẩm. Có những trƣờng hợp, một sự thay đổi nhỏ cũng có thể gây ảnh hƣởng lớn, kéo theo việc kiểm thử viên có thể không đáp ứng đƣợc tiến độ của dự án đề ra.
Nhƣ vậy, việc phát triển một phƣơng pháp kiểm thử để hạn chế tác động của sự thay đổi, đồng thời tiết kiệm đƣợc chi phí về thời gian và tiền bạc là thực sự cần thiết. Phƣơng pháp kiểm thử dựa trên mô hình nhằm kiểm tra tính đúng đắn của lập trình so với thiết kế, là giải pháp giúp giải quyết đƣợc vấn đề trên. Trong chƣơng này, tôi sẽ trình bày lý thuyết về phƣơng pháp kiểm thử dựa trên mô hình và ứng dụng cho kiểm thử phần mềm. Khái niệm kiểm thử dựa trên mô hình Trong quá trình kiểm thử tự động phần mềm, kiểm thử viên trƣớc tiên sẽ tạo ra các kịch bản kiểm thử bằng cách ghi lại tính năng của phần mềm đó.
Sau đó, kiểm thử viên tiến hành kiểm thử theo kịch bản đã đƣợc tạo ra với những tham số khác nhau. Quá trình kiểm thử đƣợc chạy tự động. Tuy nhiên, việc tạo kịch bản kiểm thử lại đƣợc tiến hành thủ công. Hầu hết các công cụ kiểm thử ngày nay đều kiểm thử tự động dựa trên các kịch bản có sẵn, do đó việc tạo kịch bản tốn nhiều công sức của kiểm thử viên và mất rất nhiều thời gian.
Để tránh việc sai sót trong quá trình kiểm thử, việc tạo kịch bản phải đƣợc xây dựng chu đáo. Thêm vào đó, mỗi khi yêu cầu từ phía ngƣời dùng thay đổi thì kịch bản cũng phải thay đổi theo. Vì vậy, việc tạo tự động các kịch bản kiểm thử là thật sự cần thiết. Hƣớng tiếp cận ở đây là kiểm thử dựa trên mô hình nhằm khắc phục đƣợc các vấn đề về chi phí, thời gian.
Kiểm thử dựa trên mô hình là một phƣơng pháp kiểm thử nơi mà các ca kiểm thử đƣợc sinh ra từ mô hình đặc tả hành vi của hệ thống đang đƣợc kiểm thử. Mô hình này 5 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com đƣợc biểu diễn bằng máy hữu hạn trạng thái, ôtômat, đặc tả đại số, biểu đồ trạng thái bằng UML, v. Quy trình chung của kiểm thử dựa trên mô hình Quá trình kiểm thử tự động dựa trên mô hình đƣợc bắt đầu bằng việc xác định yêu cầu của hệ thống từ đó xây dựng mô hình dựa vào các yêu cầu và chức năng của hệ thống. Việc xây dựng mô hình còn phải dựa trên các yếu tố dữ liệu đầu vào và đầu ra.
Mô hình này đƣợc sử dụng để sinh đầu vào cho các ca kiểm thử. Tiếp đến, chúng ta sẽ sinh giá trị đầu ra mong muốn ứng với mỗi bộ đầu vào. Khi kết thúc bƣớc này, chúng ta đã có các ca kiểm thử [1]. Các ca kiểm thử đó đƣợc tiến hành chạy và kết quả thu đƣợc sẽ đƣợc so sánh với kết quả mong đợi.
Từ đó quyết định hành động tiếp theo nhƣ sửa đổi mô hình hoặc dừng kiểm thử, v. Thiết kế Các bản đặc tả yêu cầu Mô hình Phản hồi Phản hồi Tạo tự động Các chuổi kiểm thử Kiểm thử dự đoán Đưa ra Kết luận: Pass hay Fail Theo dõi Điều khiển Thực thi Phản hồi Hình 2. Quy trình của kiểm thử dựa trên mô hình [11] Hình 2.1 mô tả về quy trình chung của kiểm thử tự động dựa trên mô hình. Kiểm thử tự động dựa trên mô hình gồm các giai đoạn sau: 6 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com - Sinh mô hình dựa trên các yêu cầu và chức năng của hệ thống.
- Sinh các ca kiểm thử (bộ đầu vào và giá trị đầu ra mong đợi cho mỗi ca kiểm thử). - Chạy các kịch bản kiểm thử để phát hiện các lỗi/khiếm khuyết của sản phẩm. - So sánh kết quả đầu ra thực tế với kết quả đầu ra dự kiến. - Quyết định hành động tiếp theo (sửa đổi mô hình, tạo thêm ca kiểm thử, dừng kiểm thử, đánh giá chất lƣợng của phần mềm) [1].
Phƣơng pháp đặc tả mô hình bằng máy trạng thái UML Theo [1], phƣơng pháp đặc tả mô hình bằng máy trạng thái thƣờng đƣợc áp dụng trong công nghiệp. Nó có thể đƣợc sử dụng để đặc tả hành vi động (chuyển trạng thái) của các lớp đối tƣợng, các ca sử dụng (use cases), các hệ thống con và thậm chí là toàn bộ hệ thống. Tuy nhiên, máy trạng thái UML thƣờng đƣợc sử dụng cho các lớp đối tƣợng. Theo [10], biểu đồ cộng tác đặc tả bằng UML là một mô hình quan trọng trong việc kiểm thử hệ thống bởi mô hình này đặc tả chính xác hành vi (tƣơng tác giữa các đối tƣợng) của hệ thống cần kiểm thử.
Trong UML, một trạng thái ứng với một điều kiện quan trọng của một đối tƣợng. Trạng thái này đƣợc quyết định bởi các giá trị hiện thời của đối tƣợng, các mối quan hệ với các đối tƣợng khác và các hành động (phƣơng thức) mà đối tƣợng này thực hiện. Một phép chuyển trạng thái là mối quan hệ giữa hai trạng thái. Một phép chuyển trạng thái trong UML bao gồm một sự kiện đƣợc kích hoạt, điều kiện và hành động tƣơng ứng.
Các sự kiện đƣợc kích hoạt của các phép chuyển trạng thái có thể là một trong các sự kiện sau: - Một lời gọi ứng với một phƣơng thức. - Một tín hiệu nhận đƣợc từ các trạng thái khác trong máy trạng thái. - Một sự thay đổi giá trị của một thuộc tính nào đó của một đối tƣợng. - Hết thời gian (timeout).
Thuận lợi và khó khăn của kiểm thử tự động dựa trên mô hình Trong quá trình phát triển phần mềm, các kiểm thử viên thƣờng thực hiện công việc của mình bằng các phƣơng pháp truyền thống (thủ công) nên thời gian và 7 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com chi phí dành cho các hoạt động này thƣờng rất cao. Kiểm thử dựa trên mô hình hứa hẹn sẽ là một giải pháp hiệu quả nhằm góp phần giải quyết vấn đề này [1]. Cụ thể, kiểm thử dựa trên mô hình có các ƣu điểm sau: - Giảm chi phí và thời gian: Do quá trình kiểm thử hầu hết đƣợc thực hiện tự động nên tính hiệu quả của phƣơng pháp này rất cao trong khi thời gian đƣợc giảm một cách tối thiểu.