Tài liệu Sinh dữ liệu test tự động dựa vào kỹ thuật kiểm chứng mô hình

TÓM TẮT Đề tài nghiên cứu về sinh dữ liệu test tự động dựa vào kỹ thuật kiểm chứng mô hình, quá trình phát triển từ kiểm chứng phần cứng đến kiểm chứng cho các mô hình phần mềm. Test tự động là việc sử dụng phần mềm để kiểm soát việc thực thi các test, so sánh kết quả thực tế để dự đoán kết quả, thiết lập các tiền điều kiện test và điều khiển các test khác và các hàm báo cáo test. Kiểm chứng mô hình (model checking) là một hướng tiếp cận hiệu quả cho việc đảm bảo chất lượng phần mềm. Kĩ thuật này được áp dụng để chứng minh một cách tự động tính đúng đắn của phần mềm hoặc chỉ ra tại sao phần mềm không chạy đúng thông qua phản ví dụ. Hiện nay có rất nhiều công cụ kiểm chứng mô hình phần mềm như NuSMV, SPIN, KRONOS ... Khóa luận này nghiên cứu lý thuyết cơ bản vè kiểm chứng mô hình, ngôn ngữ SMV dùng để mô hình hóa hệ thống và cách sử dụng NuSMV để kiểm chứng mô hình phần mềm. Kiểm chứng mô hình thường được áp dụng ở giai đoạn thiết kế vì việc mô hình hóa bản thiết kế hệ thống dễ dàng hơn mô hình hóa mã nguồn của hệ thống. Ngoài ra, việc sớm tìm ra lỗi ở bản thiết kế sẽ giúp giảm thiểu rủi ro của quá trình phát triển phần mềm. Vì thế chúng tôi tập trung tìm hiểu và đề xuất quy trình kiểm chứng mô hình sử dụng NuSMV ở giai đoạn thiết kế phần mềm. Qua đó sinh ra dữ liệu test cho các trường hợp kiểm chứng bị sai. Đồng thời áp dụng quy trình này để sinh dữ liệu test cho bài toán thang máy. LỜI CẢM ƠN Lời đầu tiên cho em xin chân thành cám ơn tới Ths. Nguyễn Hồng Tân, thầy đã trực tiếp hướng dẫn em tần tình trong suốt năm học vừa qua. 1 Em xin bày tỏ lòng biết ơn tới các thầy, cô giáo trong bộ môn Công nghệ phần mềm nói riêng, và trong toàn trường nói chung. Các thầy cô đã dạy bảo, chỉ dẫn chúng em và luôn tạo điều kiện tốt nhất cho chúng em học tập, trong suốt quá trình học đại học, đặc biệt là trong khoảng thời gian làm đồ án tốt nghiệp. Tôi xin chân thành cảm ơn tới các bạn sinh viên lớp công nghệ phần mềm – K6B và tập thể lớp K6H đã cho tôi những ý kiến đóng góp giá trị cùng những lời động viên khích lệ khi thực hiện đề tài này. Xin cảm ơn bạn bè và gia đình đã động viên, cổ vũ, đóng góp ý kiến, trao đổi trong suốt quá trình học tập, nghiên cứu và làm việc giúp em hoàn thành đề tài đúng thời hạn. Thái Nguyên, tháng 06 năm 2012 Sinh viên Nguyễn Văn Đoàn LỜI CAM ĐOAN Tôi xin cam đoan: Đồ án tốt nghiệp này là công trình nghiên cứu thực sự của cá nhân tôi và được thực hiện trên cơ sở kiến thức lý thuyết kinh điển dưới sự hướng dẫn khoa học của Thạc sỹ Nguyễn Hồng Tân. Các nội dung nghiên cứu và kết quả trong đồ án là trung thực và chưa từng được công bố dưới bất kỳ hình thức nào trước khi bảo vệ. Đồ án có sử dụng một số nhận xét đánh giá cũng như số liệu của các tác giả, điều này được thể hiện trong phần tài liệu tham khảo. 2 Nếu phát hiện có bất kỳ sự gian lận nào tôi xin hoàn toàn chịu trách nhiệm trước Hội đồng bảo vệ, cũng như kết quả đồ án của mình. Thái Nguyên, tháng 06 năm 2012 Sinh viên Nguyễn Văn Đoàn DANH MỤC TỪ VIẾT TẮT Ký hiệu AG AF AX ACTL* BDD CTL* CTL F LTL OBB OBBD Thuật ngữ All Globally All Future All Next All Computation Tree Logic Binary Decision Diagram Computation Tree Logic branChing-Time-temporal Logic Future Linear Time Logic Ordered Binary Decision Ordered Binary Decision Diagrams 3 MỤC LỤC TÓM TẮT----------------------------------------------------------------------------i LỜI CẢM ƠN-----------------------------------------------------------------------ii LỜI CAM ĐOAN------------------------------------------------------------------iii DANH MỤC TỪ VIẾT TẮT-----------------------------------------------------iv MỤC LỤC---------------------------------------------------------------------------v DANH MỤC HÌNH VẼ----------------------------------------------------------vii CHƯƠNG 1: TỔNG QUAN------------------------------------------------------1 1.1. Nhu cầu tự động hóa---------------------------------------------------------1 1.2. Tiến trình của kiểm chứng phần mềm-------------------------------------2 1.3. Trình tự logic và kiểm chứng mô hình------------------------------------3 CHƯƠNG 2: PHÁT SINH DỮ LIỆU TEST TỰ ĐỘNG & KIỂM CHỨNG MÔ HÌNH----------------------------------------------------------------------------7 2.1. Phát sinh dữ liệu test tự động----------------------------------------------7 2.1.1. Khái niệm về kiểm thử tự động---------------------------------------7 2.1.2. Mục đích-----------------------------------------------------------------7 2.1.3. Phân loại kiểm thử tự động--------------------------------------------9 2.1.4. Quy trình kiểm thử tự động------------------------------------------11 2.2. Kiểm chứng mô hình------------------------------------------------------13 2.2.1. Cây tính toán logic CTL*(Computation Tree Logics)-----------13 4 2.2.2. Sơ đồ quyết định Nhị phân(BDD-Binary Decision Diagrams)- 17 2.2.3. Kiểm chứng mô hình-------------------------------------------------19 2.2.4. Phân hoạch và yêu cầu giữa các cấu trúc--------------------------25 2.2.5. Lý luận thành phần----------------------------------------------------34 2.2.6. Trừu tượng hóa--------------------------------------------------------43 CHƯƠNG 3: SINH DỮ LIỆU TEST-------------------------------------------64 3.1. Bài toán mô phỏng---------------------------------------------------------64 3.1.1. Phát biểu bài toán-----------------------------------------------------64 3.1.2.Đặc tả--------------------------------------------------------------------64 3.2. Tìm hiểu công cụ test------------------------------------------------------73 3.2.1.Ngôn ngữ SMV--------------------------------------------------------73 3.2.2. Bộ công cụ kiểm chứng mô hình NuSMV-------------------------74 3.3. Kết quả-----------------------------------------------------------------------76 KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN--------------------------------------78 TÀI LIỆU THAM KHẢO--------------------------------------------------------80 NHẬN XÉT CỦA GIÁO VIÊN HƯỚNG DẪN------------------------------81 5 DANH MỤC HÌNH VẼ Hình 2.1. Quy trình kiểm thử tự động. Hình 2.2. Các toán tử CTL cơ bản. Hình 2.3. OBDD cho công thức (a ⋀ b) ⋀ (c ⋀ d). Hình 2.4. Ví dụ hệ thống điều khiển đèn giao thông. Hình 3.1. Biểu đồ ca sử dụng của hệ thống thang máy. Hình 3.2. Biểu đồ lớp hệ thống thang máy. Hình 3.3. Biểu đồ lớp của hệ thống thang máy. Hình 3.4. Biểu đồ trạng thái. Hình 3.5. Biểu đồ trình tự. Hình 3.6. Biểu đồ cộng tác. Hình 3.7. Biểu đồ lớp chi tiết. Hình 3.8. Sơ đồ kiến trúc NuSMV. Hình 3.9. Kết quả biên dịch chương trình. Hình 3.10. Kết quả kiểm chứng chương trình. Hình 3.11. Dữ liệu test. 6 CHƯƠNG 1: TỔNG QUAN Kiểm chứng mô hình là một kỹ thuật tự động để xác minh trang thái hữu hạn của hệ thống hiện tại. Nó có một số lợi ích hơn cách tiếp cận truyền thống để giải quyết vấn đề này dựa trên việc mô phỏng, kiểm thử và suy luận. Phương pháp được sử dụng thành công trong thực hành xác minh các thiết kế mạch tuần tự phức tạp và các giao thức truyền thông.Thách thức trong kiểm chứng mô hình là giải quyết được vấn đề bùng nổ không gian trạng thái. Vấn đề này xuất hiện khi các hệ thống có nhiều thành phần mà có thể tương tác với nhau hoặc tương tác với các hệ thống khác mà cấu trúc dữ liệu có thể nhận nhiều giá trị giả sử khác nhau (ví dụ, đường dẫn của một mạch). Trong những trường hợp như thế này số các trạng thái mục tiêu có thể rất lớn. Trong khoảng hơn 10 năm qua đã có tiến bộ đáng kể trong giải quyết vấn đề này. Chúng ta cũng mô tả cách làm như thế nào để kiểm chứng mô hình được sử dụng để xác minh các thiết kế hệ thống phức tạp. Chúng ta cũng lưu vết phát triển của các thuật toán kiểm chứng mô hình khác và các hướng tiếp cận thảo luận khác nhau mà mục đích để giải quyết vấn đề bùng nổ không gian trạng thái. 1.1. Nhu cầu tự động hóa Ngày nay, các hệ thống phần cứng và phần mềm được sử dụng rộng rãi trong các ứng dụng mà các lỗi là không chấp nhận được trong thương mại điện tử, chuyển mạch mạng điện thoại, đường cao tốc và hệ thống điều khiển đường không, dụng cụ y tế và các ví dụ khác có quá nhiều để ghi vào danh sách. Chúng ta thường đọc các sự cố mà một vài lỗi được sinh ra với một lỗi phần cứng hoặc phần mềm. Một ví dụ gần đây của một lỗi như thế là tên lửa Ariane 5 phát nổ ngày 4/6/1996 sau chưa đầy 40 giây được đưa ra. Uỷ ban điều tra tìm thấy nguyên nhân của tai nạn là do một lỗi phần mềm trong máy tính để tính toán sự di chuyển của tên lửa. Trong khi khởi động, một ngoại lệ xuất hiện khi số thực lớn 64 bit được chuyển thành số nguyên 16 bit. Sự chuyển đổi này không được bảo vệ bởi mã nguồn điều khiển ngoại lệ và gây ra lỗi. Lỗi tương tự cũng được sinh ra khi sao lưu lỗi. Kết quả là dữ liệu không chính xác được chuyển đến máy 1 tính gây ra sự phá huỷ tên lửa. Nhóm điều tra lỗi đã đề nghị một vài phương pháp để giải quyết sự cố trong tương lai bao gồm cả việc xác minh phần mềm Ariane 5. Rõ ràng nhu cầu về độ tin cậy phần cứng và hệ thống phần mềm là quan trọng. Sự tham gia của những hệ thống như vậy sự gia tăng không đảm bảo tính đúng đắn của chúng. Thật không may, nó không khả thi để tắt hệ thống bị trục trặc để khôi phục an toàn. Chúng ta phụ thuộc rất nhiều vào những hệ thống như vậy đối với các hoạt động liên tục, trong thực tế một vài trường hợp các thiết bị ít an toàn hơn khi tắt chúng. Thậm chí khi các lỗi không nghiêm trọng, hậu quả của việc thay thế các mã quan trọng hoặc mạch thể thiệt hại về kinh tế. Vì sự thành công của Internet và các hệ thống nhúng như điện thoại di động, máy bay và các hệ thống an toàn khác, chúng ta có thể sẽ phụ thuộc nhiều hơn vào các chức năng đúng đắn của cac thiết bị máy tính trong tương lai. Thực tế, tốc độ thay đổi có thể sẽ tăng tốc trong một vài năm tới. Bởi tốc độ phát triển nhanh chóng của công nghệ, nó sẽ trở nên không quan trọng để phát triển các phương pháp làm tăng sự tự tin trong sự chính xác của các hệ thống như vậy. 1.2. Tiến trình của kiểm chứng phần mềm Áp dụng kiểm chứng mô hình để một thiết kế mô hình bao gồm một số nhiệm vụ: Mô hình hóa Nhiệm vụ đầu tiên là chuyển từ một thiết kế thành một dạng mà công cụ kiểm chứng mô hình có thể chấp nhận. Trong nhiều trường hợp, điều này chỉ đơn giản là nhiệm vụ biên dịch. Trong các trường hợp khác, do hạn chế về thời gian và bộ nhớ, mô hình hóa một thiết kế có thể yêu cầu sử dụng trừu tượng hóa để loại bỏ các chi tiết không liên quan hoặc không quan trọng Đặc tả Trước khi xác minh, cần phải xác định trạng thái của các đặc tả mà thiết kế phải đáp ứng được. Đặc tả thường được đưa ra trong một số hình thức logic. Đối với các hệ thống phần cứng và phần mềm, người ta thường sử dụng logic thời gian có thể khẳng định như thế nào là hành vi của hệ thống tiến hóa theo thời gian. Một vấn đề quan trọng trong đặc tả là sự hoàn chỉnh. Kiểm chứng mô hình yêu cầu các phương tiện kiểm tra thiết kế của một mô hình có đáp ứng được đặc 2 tả không, nhưng nó thể xác định đặc tả bao gồm tất cả các tính năng của hệ thống phải đáp ứng. Xác minh Sự xác minh lý tưởng là hoàn toàn tự động. Tuy nhiên, trong thực tế nó thường liên quan đến con người. Một trong những hoạt động là phân tích các kết quả xác minh. Trong trường hợp một kết quả phủ định, người sử dụng thường đưa ra vết lỗi. Điều này có thể được sử dụng như một counterEXample đối với các tính năng đã được kiểm tra và có thể giúp nhà thiết kế theo dõi khi xuất hiện lỗi. Trong trường hợp này, phân tích lỗi có thể yêu cầu chỉnh sửa hệ thống và áp dụng lại các thuật toán kiểm chứng mô hình. Một vết lỗi có thể là kết quả của một mô hình hệ thống không chính xác hoặc của một đặc tả không đúng. Một vết lỗi có thể hữu ích trong xác định và sửa hai vấn đề này. Khả năng cuối cùng là nhiệm vụ xác minh sẽ dừng lại không bình thường, do kích thước của mô hình quá lớn không phù hợp với bộ nhớ máy tính. Trong trường hợp này, cần xác minh lại sau khi thay đổi một số tham số của mô hình kiếm tra hay điều chỉnh mô hình. 1.3. Trình tự logic và kiểm chứng mô hình Các đặc tả được diễn tả theo trình tự thời gian, và các hệ thống tương tác được mô hình hóa như một đồ thị chuyển trạng thái. Một thủ tục tìm kiếm hiệu quả được sử dụng để xác định có hay không đồ thị chuyển trạng thái đáp ứng những những đặc tả đó. Kỹ thuật được phát triển năm 1981 bởi Clarke và Allen Emerson. Quyelle và Sifakis độc lập phát hiện một kỹ thuật xác minh tương tự ngay sau đó. Một hướng tiếp cận khác dựa vào việc hiển thị nội dung giữa các Otomat được phát minh bởi Robert Kurshan tại phòng thí nghiệm ATT Bell. Kỹ thuật này có một vài lợi ích quan trọng trên các công cụ thử định lý cơ học hoặc bộ kiểm tra chứng cứ để xác minh các mạch và giao thức. Quan trọng nhất là các thủ tục được tự động hóa cao. Thông thường, người sử dụng cung cấp một mức biểu diễn mô hình và đặc tả được kiểm tra cao. Bộ kiểm chứng mô hình hoặc kết thúc với câu trả lời true, chỉ ra rằng mô hình đáp ứng được đặc tả hoặc đưa ra một bộ đếm mẫu thực thi hiển thị tại sao mà công thức không đáp ứng được. Bộ đếm mẫu đặc biệt quan trọng trong khi tìm kiếm các lỗi nhỏ trong các hệ thống tương tác phức tạp. 3 Bộ kiểm chứng mô hình đầu tiên có thể tìm thấy các lỗi nhỏ trong các mạch và giao thức nhỏ. Tuy nhiên, chúng không thể xử lý các vấn đề lớn như vấn đề bùng nổ không gian trạng thái. Khả năng của những hệ thống xác minh với độ phức tạp thực tế thay đổi cuối những năm 1980 với sự khám phá cách biểu diễn mối quan hệ chuyển tiếp sử dụng biểu đồ quyết định Nhị phân trình tự (ordered binary decision diAGrams - OBDD). Sự khám phá này phụ thuộc bởi 3 đội nghiên cứu và là cơ sở khá đơn giản. Giả sử rằng hành vi của một hệ thống tương tác được xác định bởi n biến trạng thái logic v 1 ,v 2 ,…., v n . Sau đó mối quan hệ chuyển tiếp của hệ thống có thể được biểu diễn như biểu thức logic sau: R(v1,v2,…., vn , v’1,v'2,..., v'n) Với v 1 ,v 2 , … . , v n biểu diễn trạng thái hiện tại, v'1,v'2,...,v'n biểu diễn trạng thái tiếp theo. Bằng cách biến đổi công thức này tới một sơ đồ chuyển tiếp Nhị phân, một đại diện ngắn gọn của mối quan hệ chuyển tiếp có thể chứa. Thuật toán kiếm chứng mô hình nguyên thủy, cũng với cách biểu diễn mới đối với các quan hệ chuyển tiếp được gọi là kiểm chứng mô hình tượng trưng. Bằng cách sử dụng sự kết hợp này, nó có thể thực sự xác minh được các hệ thống tương tác lớn. Thực tế, một vài ví dụ có hơn 10 120 trạng thái được xác minh. Đây là điều có thể bởi vì số lượng các nút trong biểu đồ quyết định Nhị phân phải được xây dựng không phụ thuộc vào số lượng trạng thái thực tế hoặc kích thước của quan hệ chuyển tiếp. Bởi vì đây là bước đột phá cách làm có thể xác minh các hệ thống tương tác với độ phức tạp thực tế, và một số công ty bao gồm cả Intel, Motorola, Fujitsu và ATT bắt đầu sử dụng bộ kiểm chứng mô hình tượng trưng để xác minh các mạch và giao thức thực sự. Trong một vài trường hợp lỗi tìm thấy được bỏ qua bởi mô phỏng mở rộng. Trong khi biểu tượng biểu diễn làm tăng thêm đáng kể kích thước của hệ thống mà chúng ta có thể xác minh được, nhiều hệ thống thực tế vẫn quá lớn để xử lý. Do đó, quan trọng là tìm được các kỹ thuật có thể sử dụng kết hợp các phương pháp tượng trưng để mở rộng kích cỡ của các hệ thống mà có thể xác minh được. Kỹ thuật khai thác cầu trúc của các mạch và giao thức phức tạp. Nhiều hệ thống trạng thái hữu hạn gồm nhiều tiến trình chạy song song. Các đặc tả đối với 4 những hệ thống sao cho có thể thường được chia thành các tính năng mà có thể mô tả hành vi của một phần nhỏ hệ thống. Một chiến lược rõ ràng để kiểm tra mỗi tính năng cục bộ chỉ sử dụng một phần hệ thống mà nó mô tả. Nếu có thể cho thấy rằng hệ thống đáp ứng được từng tính năng cục bộ, và nếu kết hợp các tính năng cục bộ của đặc tả tổng thể sau đó hệ thống hoàn chỉnh phải đáp ứng tốt được những đặc tả. Ví dụ, xem xét các vấn đề xác minh một giao thức truyền thông là mô hình hóa bởi ba tiến trình trạng thái hữu hạn: một máy phát, một vài kiểu mạng và một máy thu. Giả sử rằng đặc tả cho hệ thống là dữ liệu được truyền đi một cách chính xác từ máy phát đến máy thu. Một đặc tả phải được tách thành ba tính băng cục bộ. Đầu tiên, dữ liệu được truyền một cách chính xác từ máy phát tới mạng. Thứ hai, dữ liệu truyền chính xác từ một thiết bị cuối của mạng đến thiết bị của mạng khác. Cuối cùng, máy dữ liệu được truyền chính xác từ mạng tới máy thu. Chúng ta có thể xác minh điều đầu tiên trong ba tính năng cục bộ chỉ sử dụng máy phát và mạng, thứ hai chỉ sử dụng mạng và thứ ba chỉ sử dụng mạng và máy thu. Bằng cách tách sự xác minh theo cách này, chúng ta không bao giờ gồm tất cả các tiến trình và do đó tranh được hiện tượng bùng nổ không gian trạng thái. Kỹ thuật liên quan đến việc sử dụng trừu tượng hóa. Kỹ thuật này xuất hiện chủ yếu để lý luận về các hệ thống tương tác gồm đường dẫn dữ liệu. Theo truyền thống, trạng thái hữu hạn xác minh các phương thức được sử dụng chính đối với hệ thống hướng điều khiển. Những phương pháp tượng trưng có thể xử lý một vài hệ thống liên quan đến thao tác dữ liệu không tầm thường, nhưng sự phức tạp của sự xác minh thường cao. Hướng tiếp cận này dựa trên sự quan sát những đặc tả của hệ thống bao gồm đường dẫn dữ liệu thường bao gồm các quan hệ đơn giản giữa những giá trị dữ liệu trong hệ thống. Ví dụ, trong xác minh toán tử cộng của một vi xử lý, chúng ta có thể yêu cầu một giá trị thực sự bằng tổng của 2 giá trị khác. Trong những tình huống sao cho, sự trừu tượng hóa có thể được sử dụng để giảm độ phức tạp của kiểm chứng mô hình. Sự trừu tượng hóa thường được đặc tả bằng cách ánh xạ giữa giá trị của dữ liệu thực tế trong hệ thống và một tập nhỏ các giá trị của dữ liệu trừu tượng. Bằng cách mở rộng ánh xạ các trạng thái và sự chuyển tiếp, có thể đưa ra một phiên bản trừu tượng hóa 5 mới của hệ thống được xem xét. Hệ thống trừu tượng thường nhỏ hơn hệ thống thực, và như một kết quả nó thường đơn giản hơn để xác minh các tính năng ở mức trừu tượng. CHƯƠNG 2: PHÁT SINH DỮ LIỆU TEST TỰ ĐỘNG & KIỂM CHỨNG MÔ HÌNH 2.1. Phát sinh dữ liệu test tự động 2.1.1. Khái niệm về kiểm thử tự động Test tự động là việc sử dụng phần mềm để kiểm soát việc thực thi các test, so sánh kết quả thực tế để dự đoán kết quả, thiết lập các tiền điều kiện test và điều khiển các test khác và các hàm báo cáo test. Đặc điểm của kiểm thử tự động phần mềm (Test Automation) là: - Quá trình xử lý một cách tự động các bước thực hiện các test case (trong cả một dự án). - Kiểm thử tự động bằng một công cụ nhằm rút ngắn thời gian kiểm thử. 6 2.1.2. Mục đích 2.1.2.1. Tại sao phải kiểm thử tự động? - Giảm bớt công sức và thời gian thực hiện quá trình kiểm thử cho cả một test plan. - Tăng độ tin cậy bởi vì có những việc kiểm thử con người khó có thể làm được hoặc quên. - Giảm sự nhàm chán cho các tester khi đồng thời thực hiện các công việc kiểm thử - Rèn luyện kỹ năng lập trình cho kiểm thử viên, ví dụ điển hình là tạo ra các test script. - Giảm chi phí cho tổng quá trình kiểm thử. 2.1.2.2. Test Tool kiểm thử tự động? Test Tool trong lĩnh vực phát triển phần mềm là công cụ giúp thực hiện việc kiểm tra phần mềm một cách tự động. Tuy nhiên không phải mọi việc kiểm tra đều có thể tự động hóa, câu hỏi đặt ra là trong điều kiện hoặc tình huống nào dùng Test Tool là thích hợp? Việc dùng Test Tool thường được xem xét trong một số tình huống sau:  Không đủ tài nguyên: Khi số lượng Test Case quá nhiều mà Tester không thể hoàn tất trong thời gian cụ thể Ví dụ khi thực hiện kiểm tra chức năng của một website. Website này sẽ được kiểm tra với 6 môi trường gồm 5 trình duyệt và 2 hệ điều hành. Tình huống này đòi hỏi số lần kiểm tra tăng lên và lặp lại 10 lần so với việc kiểm tra cho một môi trường cụ thể.  Kiểm tra hồi quy: Trong quá trình phát triển phần mềm, nhóm lập trình thường đưa ra nhiều phiên bản phần mềm liên tiếp để kiểm tra. Thực tế cho thấy việc đưa ra các phiên bản phần mềm có thể là hàng ngày, mỗi phiên bản bao gồm những tính năng mới, hoặc tính năng cũ được sửa lỗi hay nâng cấp. Việc bổ sung hoặc sửa lỗi code cho những tính năng ở phiên bản mới 7 có thể làm cho những tính năng khác đã kiểm tra tốt chạy sai mặc dù phần code của nó không hề chỉnh sửa. Để khắc phục điều này, đối với từng phiên bản, Tester không chỉ kiểm tra chức năng mới hoặc được sửa, mà phải kiểm tra lại tất cả những tính năng đã kiểm tra tốt trước đó. Điều này khó khả thi về mặt thời gian nếu kiểm tra thủ công. Ví dụ các trình duyệt: IE, Netscape, Opera, Fire Fox, Google Chrome, Safari  Kiểm tra khả năng vận hành phần mềm trong môi trường đặc biệt: Đây là kiểm tra nhằm đánh giá xem vận hành của phần mềm có thỏa mãn yêu cầu đặt ra hay không. Thông qua đó Tester có thể xác định được các yếu tố về phần cứng, phần mềm ảnh hưởng đến khả năng vận hành của phần mềm. Có thể liệt kê một số tình huống kiểm tra tiêu biểu thuộc loại này như sau: - Đo tốc độ trung bình xử lý một yêu cầu của Web server - Thiết lập 1000 yêu cầu, đồng thời gửi đến web server, kiểm tra tình huống 1000 người dùng truy xuất web cùng lúc. - Xác định số yêu cầu tối đa được xử lý bởi web server hoặc xác định cấu hình máy thấp nhất mà tốc độ xử lý của phần mềm vẫn có thể hoạt động ở mức cho phép. - Xác định cấu hình máy thấp nhất mà phần mềm vẫn có thể hoạt động tốt. Việc kiểm tra thủ công cho những tình huống trên là cực khó, thậm chí "vô phương". Cần lưu ý là hoạt động kiểm thử tự động nhằm mục đích kiểm tra, phát hiện những lỗi của phần mềm trong những trường hợp đoán trước. Điều này cũng có nghĩa là nó thường được thực hiện sau khi đã thiết kế xong các tình huống (test case). Tuy nhiên, như đã nói, không phải mọi trường hợp kiểm tra đều có thể hoặc cần thiết phải tự động hóa, trong tất cả test case thì Tester phải đánh giá và chọn ra những test case nào phù hợp hoặc cần thiết để áp dụng kiểm thử tự động dựa trên những tiêu chí đã đề cập bên trên. 8 2.1.3. Phân loại kiểm thử tự động Vì kiểm thử phần mềm thường chiếm tới 40% tất cả các nổ lực dành cho một dự án xây dựng phần mềm, nên công cụ có thể làm giảm thời gian kiểm thử (không làm giảm tính kỹ lưỡng) sẽ rất có giá trị. Thừa nhận lợi ích tiềm năng này, các nhà nghiên cứu và người thực hành đã phát triển một số thế hệ các công cụ kiểm thử tự động: 2.1.3.1. Công cụ kiểm thử tự động mã trình  Bộ phân tích tĩnh: Các hệ thống phân tích chương trình này hỗ trợ cho "việc chứng minh" các lý lẽ tĩnh - những mệnh đề yếu kém về cấu trúc và định dạng của chương trình.  Bộ kiểm toán mã: Những bộ lọc chuyên dụng này được dùng để kiểm tra chất lượng của phần mềm để đảm bảo rằng nó đáp ứng các chuẩn mã hoá tối thiểu.  Bộ xử lý khai báo: Những hệ thống tiền xử lý/hậu xử lý này được sử dụng để cho biết liệu những phát biểu do người lập trình nêu, được gọi là các khẳng định, về hành vi của chương trình có thực sự được đáp ứng trong việc thực hiện chương trình thực hay không. 2.1.3.2. Công cụ kiểm thử tự động dữ liệu  Bộ sinh tệp kiểm thử: Những bộ xử lý này sinh ra, và điền các giá trị đã xác định, vào các tệp đọc vào điển hình cho chương trình đang được kiểm thử.  Bộ sinh dữ liệu kiểm thử: Những hệ thống phân tích tự động này hỗ trợ cho người dùng trong việc chọn dữ liệu kiểm thử làm cho chương trình hành xử theo một cách đặc biệt.  Bộ xác minh kết quả: Những công cụ này đo mức bao quát kiểm thử bên trong, thường được diễn tả dưới dạng có liên quan tới cấu trúc điều khiển của sự vật kiểm thử, và báo cáo về giá trị bao quát cho chuyên gia đảm bảo chất lượng. 9 2.1.3.3. Công cụ kiểm thử tự động cài đặt Các trợ giúp cho quá trình kiểm thử: Các công cụ này hỗ trợ cho việc xử lý các phép kiểm thử bằng cách làm gần như không khó khăn để: - Thiết lập một chương trình ứng cử viên trong môi trường kiểm thử. - Nuôi chương trình đó bằng dữ liệu vào. - Mô phỏng bằng các cuống cho hành vi của các module phụ.  Bộ so sánh đầu ra. Công cụ này làm cho người ta có thể so sánh một tập cái ra từ một chương trình này với một tập cái ra khác (đã được lưu giữ trước) để xác định sự khác biệt giữa chúng.  Hệ tiến hành ký hiệu: Công cụ này thực hiện việc kiểm thử chương trình bằng cách dùng cái vào đại số, thay vì giá trị dữ liệu số. Phần mềm được kiểm thử vậy xuất hiện để kiểm thử các lớp dữ liệu, thay vì chỉ là một trường hợp kiểm thử đặc biệt. Cái ra là đại số và có thể được so sánh với kết quả trông đợi cũng được xác định dưới dạng đại số.  Bộ mô phỏng môi trường. Công cụ này là một hệ thống dựa trên máy tính giúp người kiểm thử mô hình hoá môi trường bên ngoài của phần mềm thời gian thực và rồi mô phỏng các điều kiện vận hành thực tại một cách động.  Bộ phân tích dòng dữ liệu. Công cụ này theo dõi dấu vết luồng dữ liệu đi qua hệ thống (tương tự về nhiều khía cạnh với bộ phân tích đường đi) và cố gắng tìm ra những tham khảo dữ liệu không xác định, đặt chỉ số sai và các lỗi khác có liên quan tới dữ liệu. Hiện nay việc dùng các công cụ tự động hoá cho kiểm thử phần mềm đang phát triển, và rất có thể là ứng dụng đó sẽ phát triển nhanh trong thập kỷ tới. Các công cụ kiểm thử có thể sẽ gây ra những thay đổi lớn trong cách chúng ta kiểm thử phần mềm và do đó cải tiến độ tin cậy của các hệ thống dựa trên máy tính. 10 2.1.4. Quy trình kiểm thử tự động 2.1.4.1. Khái quát về quy trình: Hình 2.1. Quy trình kiểm thử tự động.  Kiểm thử tự động giống như là phát triển một dự án.  Mối tương quan giữa Kiểm thử tự động với toàn bộ chu trình Kiểm thử phần mềm. 2.1.4.2. Các bước cơ bản của quá trình Kiểm thử tự động  Xây dựng yêu cầu: Thu thập các đặc tả yêu cầu hoặc xây dựng Test Case, lựa chọn những phần cần Kiểm thử tự động  Phân tích, thiết kế: Xây dựng mô hình phát triển Kiểm thử tự động  Phát triển TestScript: Tạo TestScript > Chỉnh sửa TestScript > Chạy TestScript > Test Report - Tạo TestScript dùng test tool để ghi lại các thao tác lên PM cần kiểm tra và tự động sinh ra test script. - Chỉnh sửa TestScript thực hiện kiểm tra theo đúng yêu cầu đặt ra, cụ thể là làm theo test case cần thực hiện. - Chạy TestScript nhằm giám sát hoạt động kiểm tra PM của test script. - Test Report Kiểm tra kết quả thông báo sau khi thực hiện KTTĐ. Sau đó bổ sung, chỉnh sửa những sai sót.  Đánh giá kết quả: Thông qua Test Report 11 2.1.4.3. Thuận lợi và khó khăn:  Thuận lợi - Kiểm thử không cần can thiệp của Tester. - Giảm chi phí khi thực hiện kiểm tra số lượng lớn test case  Khó khăn - hoặc test case lặp lại nhiều lần. Giả lập tình huống khó có thể thực hiện bằng tay. Mất chi phí tạo các script để thực hiện kiểm thử tự động. Tốn chi phí dành cho bảo trì các script. Đòi hỏi Tester phải có kỹ năng tạo script kiểm thử tự động Không áp dụng được trong việc tìm lỗi mới của phần mềm. 2.2. Kiểm chứng mô hình 2.2.1. Cây tính toán logic CTL*(Computation Tree Logics) Cây tính toán logic CTL* kết hợp cả 2 toán tử thời gian nhánh và thời gian tuyến tính: một đường dẫn định lượng, hoặc A(đối với tất cả đường dẫn tính toán) hoặc E(đối với một vài đường dẫn tính toán) có thể đặt trước một sự khẳng định bao gồm sự kết hợp duy nhất của tính toán thời gian tuyến tính - thời gian tính toán G ("always"), F ("sometimes"), X ("nEXttime"), U ("until") và V("unless"). Phần còn lại của phần này đưa ra một mô tả chính xác của cú pháp và ngữ ngĩa của logic. Có hai loại công thức trong CTL*: công thức trạng thái (đúng trong một trạng thái cụ thể) và công thức đường dẫn (đúng theo một đường dẫn cụ thể). Lấy AP là tập tên nguyên tử gợi ý. Cú pháp của công thức trạng thái được đưa ra bởi những luật sau: - Nếu p ⋀ AP, thì p là một công thức trạng thái. Nếu f và g là các công thức trạng thái thì f ⋀g ⌐f , f ⋀g , là các công thức trạng thái. là một công thức đường dẫn thì E( f ) là một công thức - Nếu - trạng thái. Nếu f là một công thức đường dẫn thì A( f ) là một công thức f trạng thái. 12 Hai luật bổ sung là cần thiết để cụ thể cú pháp của các công thức đường dẫn - Nếu - đường dẫn. Nếu f và f f ⋀g , là một công thức trạng thái thì g X f , f cũng là một công thức là các công thức đường dẫn thì ⌐ f , f U g , f V g f ⋀g , là các công thức đường dẫn. CTL* là tập các công thức trạng thái được phát sinh bởi các luật trên. Các hệ thống trạng thái hữu hạn được mô hình hóa bởi cấu trúc Kripke với ràng buộc công bằng. Một cấu trúc Kripke M = (S,S0 ,AP,L,R,F) là một bộ 6 thành phần dưới đây: 1. 2. 3. 4. S là một tập hữu hạn các trạng thái. S0 ⋀ S là tập các trạng thái khởi tạo. AP là một tập hữu hạn các mệnh đề nguyên tử. L : S → P(AP) là một hàm mà các nhãn của mỗi trạng thái với tập mệnh đề nguyên tử đúng trong trạng thái đó. 5. R ⋀ S x S là một quan hệ chuyển tiếp. 6. F ⋀ P(S) là một tập các ràng buộc công bằng đưa ra các điều kiện chấp nhận Buchi. Một đường dẫn tại M là một chuỗi hữu hạn các trạng thái Với i π = s0s1s2…. ≥ 0. R(si, si+1). Định nghĩa inf( π ) = { s | s = si, với i vô hạn}. Một đường dẫn π trong M là bằng nhau nếu và chỉ nếu đối với mọi P ⋀ F, inf( π ) ⋀ P ≠ Ø . Chúng ta sẽ sử dụng các kí hiệu π n cho các hậu tố của π mà bắt đầu là sn. Trừ khi có quy định khác, tất cả các kết quả của chúng tôi chỉ áp dụng cho các cấu trúc Kripke hữu hạn. Nếu f là một công thức trạng thái, kí hiệu M,s ⋀ f nghĩa là f giữ tại một trạng thái s trong cấu trúc Kripke M. Tương tự, nếu f là một công thức đường dẫn, M, π ⊨ f nghĩa là f giữ theo đường dẫn π trong cấu trúc Kripke M. Khi cấu trúc Kripke M rõ ràng từ ngữ cảnh, chúng thường bỏ qua nó. Quan hệ ⊨ được định nghĩa quy nạp như sau(giả sử rằng f1 và f2 là các công thức trạng thái và g1, g2 là các công thức đường dẫn): 13 1. 2. 3. 4. 5. s⊨p s ⊨ ⌐ f1 s ⊨ f1 ⋀ f2 s ⊨ f1 ⋀ f2 s ⊨ E(g1) như là π 6. s ⊨ A(g1) ⋀ p ⋀ L(s) ⋀ s | ≠ f1 ⋀ s ⊨ f1 và s ⊨ f2 ⋀ s ⊨ f1 hoặc s ⊨ f2 ⋀ tồn tại một đường dẫn bằng π bắt đầu với s ⊨ g1 ⋀ đối với tất cả các đường dẫn bắt đầu với s, π ⊨ g1 7. 8. 9. 10. 11. 12. π π π π π π ⊨ f1 ⊨ ⌐ ⊨ g1 ⊨ g1 ⊨ Xg1 ⊨ g1 g1 ⋀ g2 ⋀ g2 ⋀ g2 tất cả 0 ≤ j - Xem thêm -