- Quá trình sinh các ca kiểm thử tự động dựa trên mô hình gồm các công đoạn chính: Xây dựng mô hình, nhúng mã C, áp dụng công cụ Spin để sinh các ca kiểm thử. - Trong đó xây dựng mô hình là công đoạn đầu tiên, nhiệm vụ chính ở đây là từ mô tả các yêu cầu của hệ thống và chức năng xác định cùng với dữ liệu đầu vào và ra phải xây dựng được mô hình của hệ thống. - Xây dựng mô hình có vai trò hết sức quan trọng, nếu việc xây dựng mô hình không chính xác thì các công đoạn về sau trong hệ thống kiểm thử dựa trên mô hình không thể chính xác được. - Do tầm quan trọng đó của việc xây dựng mô hình, khóa luận này đề cập tới các lý thuyết cơ bản về xây dựng mô hình của hệ thống bằng ngôn ngữ mô hình promela. - Trong khóa luận này tôi trình bày phương pháp nhúng mã nguồn C vào trong mô tả promela để lọc các trạng thái và sinh các ca kiểm thử một cách tự động bằng công cụ hỗ trợ kiểm thử Spin. - 3CHƯƠNG 2 CƠ SỞ LÝ THUYẾT CHO KIỂM THỬ MÔ HÌNH. - Khái niệm kiểm thử dựa trên mô hình. - Thuận lợi và khó khăn của kiểm thử dựa trên mô hình. - Máy hữu hạn trạng thái ( Finite State Machines. - Bài toán Kitchen Timer. - Xây dựng mô hình. - Phương pháp sinh các ca kiểm thử tự động. - Máy hữu hạn trạng thái của Kitchen Timer. - Đặc tả kitchen timer bằng promela có nhúng mã C. - 33Phụ lục A: Đặc tả của kitchen timer bằng promela có nhúng mã C. - 42Phụ lục B: Một số ca kiểm thử. - 4Hình 1: Các bước thực hiện kiểm thử mô hình. - 7Hình 2: Mô hình chuyển đổi trạng thái của kitchen timer.. - 23Hình 11: Kiến trúc hệ thống kitchen timer.. - 24Hình 12: Mô hình máy hữu hạn trạng thái kitchen timer.. - Trong các công ty phát triển phần mềm hầu hết công việc kiểm thử của kiểm thử viên được thực hiện thủ công bằng tay. - Trong khi đó số lượng tình huống kiểm tra quá nhiều mà các kiểm thử viên không thể hoàn tất bằng tay trong thời gian cụ thể nào đó. - Để khắc phục điều này, đối với từng phiên bản, kiểm thử viên 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 đó. - Để giải quyết vấn đề này chúng ta áp dụng kỹ thuật kiểm thử dựa trên mô hình cho quá trình sinh các ca kiểm thử tự động. - Do đó, khoá luận này tập trung trình bày về việc nghiên cứu kiểm thử dựa trên mô hình và ứng dụng công cụ Spin vào việc tự động sinh các ca kiểm thử: Xây dựng mô hình hệ thống và thực nghiệm.. - Bài toán thực hiện trong khóa luận này là bài toán kiểm thử dựa trên mô hình để sinh ra các ca kiểm thử một cách tự động. - Thiết kế hệ thống bằng ngôn ngữ Promela và nhúng mã C vào thiết kế Promela là hai nội dung quan trong nhất của quá trình sinh ca kiểm thử tự động. - Tôi nghiên cứu phương pháp được sử dụng để thực hiện các nội dung đó, và áp dụng nó vào bài toán sinh ca kiểm thử tự động của hệ thống máy hẹn giờ kitchen timer.. - Quá trình thực nghiệm sẽ bao gồm các thực nghiệm về thiết kế hệ thống kitchen timer bằng Promela, nhúng mã nguồn C vào thiết kế Promela của hệ thống và sử dụng Spin sinh các ca kiểm thử một cách tự động. - 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, các bước thực hiện, lợi ích của kiểm thử mô hình và cách thức xây dựng mô hình (máy hữu hạn trạng thái). - Chương 3 trình bày các khái niệm về ngôn ngữ mô hình promela, bao gồm các định nghĩa cơ bản về khai báo biến và kiểu, định danh, hằng số, biểu thức, tiến trình. - Chương 4 trình bày về các kết quả thực nghiệm của quá trình mô tả máy hẹn giờ kitchen timer, thiết kế mô hình hệ thống kitchen timer bằng Promela, và quá trình sinh ca kiểm thử tự động. - CƠ SỞ LÝ THUYẾT CHO KIỂM THỬ MÔ HÌNH. - Quá trình thiết kế mô hình của hệ thống bằng ngôn ngữ mô hình Promela làm việc dựa trên các khái niệm về kiểm thử mô hình. - Chương này sẽ lần lượt trình bày những khái niệm cơ bản về kiểm thử mô hình. - Theo Colin Campbell, kiểm thử dựa trên mô hình là một kỹ thuật kiểm thử mà các hoạt động của hệ thống được chạy thử trong một thời gian sẽ được dự đoán trước, nó được thực hiện bởi một đặc tả hình thức hoặc một mô hình của hệ thống.. - Các mẫu thiết kế hay mô hình là mô tả đơn giản của hệ thống dựa trên yêu cầu hệ thống và chức năng xác định, giúp chúng ta có thể hiểu và dự đoán được hành vi của hệ thống.. - Quá trình kiểm thử 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 ra các ca kiểm thử. - Chúng ta có thể biết kết quả đầu ra mong đợi từ mô hình hoặc từ quy định chuẩn ( oracle. - Từ đó quyết định hành động tiếp theo như sửa đổi mô hình hoặc dừng kiểm thử,…. - Các bước để thực hiện kiểm thử dựa trên mô hình:. - Xây dựng mô hình dựa trên các yêu cầu và chức năng của hệ thống. - Chạy kịch bản kiểm thử. - 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 ) Các bước thực hiện kiểm thử dựa trên mô hình được minh họa bằng sơ đồ sau:. - Hình 1: Các bước thực hiện kiểm thử mô hình.. - Trong 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 phương pháp truyền thống nên thường thiếu thời gian để thực hiện kiểm thử, hoặc giá thành sản phẩm khi hoàn thành thường cao…. - Và kiểm thử dựa trên mô hình sẽ khắc phục được một số nhược điểm đó:. - Do quá trình sinh ca kiểm thử là tự động vì vậy mà rút ngắn thời làm phần mềm, và chất lượng phần mềm tốt hơn.. - Đặc biệt tuy chi phí lớn cho việc xây dựng mô hình nhưng điều này sẽ được khấu trừ do chi phí bảo dưỡng thấp hơn nhiều khi hệ thống được hoạt động. - Quá trình sinh ra các ca kiểm thử được thực hiện một cách tự động nên sinh ra nhiều ca kiểm thử và phát hiện nhiều lỗi. - Người kiểm thử phần mềm cần thường xuyên trao đổi với người phát triển phần mềm trong khi xây dựng mô hình hệ thống vì vậy mà tăng khả năng giao tiếp trao đổi giữa người phát triển phần mềm, và người kiểm thử.. - Người kiểm thử sẽ không bị nhàm chán khi phải thực hiện lặp lại nhiều lần một công việc, điều đó làm cho người kiểm thử hài lòng với công việc của mình.. - Sớm phát hiện lỗi và sự không rõ ràng trong đặc điểm kỹ thuật và thiết kế vì vậy sẽ tăng thời gian giải quyết vấn đề trong kiểm thử.. - Tự động tạo và kiểm tra chánh các ca kiểm thử trùng nhau hoặc không hữu hiệu.. - Khi một yêu cầu của hệ thống thay đổi việc thay đổi các ca kiểm thử là rất phức tạp nhưng nó được giải quyết khi mà kiểm thử dựa trên mô hình. - Việc thay đổi các ca kiểm thử chỉ việc thay đổi mô hình của hệ thống.. - Mặc dù có nhiều thuận lợi nhưng bên cạnh đó cũng có những trở ngại nhất định của kiểm thử dựa trên mô hình:. - Do phải xây dựng mô hình của hệ thống vì vậy người kiểm thử phần mềm phải yêu cầu là những người có khả năng phân tích và thiết kế hệ thống.. - Trong kiểm thử dựa trên mô hình công việc quan trọng nhất là xây dựng mô hình. - Người kiểm thử phải đầu tư đáng kể cả về thời gian, trí tuệ và tiền bạc cho việc xây dựng mô hình hệ thống.. - Giống như các phương pháp kiểm thử khác, việc kiểm thử dựa trên mô hình chỉ phát hiện được lỗi của hệ thống mà không thể phát hiện được hệ thống còn lỗi hay không.. - Trong kiểm thử phần mềm có nhiều kiểu mô hình được sử dụng như : Finite State Machines, UML, Grammars. - Trong nghiên cứu này trình bày về mô hình máy hữu hạn trạng thái: Finite State Machines.. - Một máy trạng thái mô tả cho hệ thống phần mềm được định nghĩa dựa vào ( I, S, T, F, L), trong do:. - I : Tập hợp các yếu tố đầu vào của hệ thống.. - S : Tập các trạng thái của hệ thống.. - F : Tập hợp các trạng thái kết thúc.. - L : Trạng thái ban đầu của hệ thống.. - Bài toán Kitchen Timer Chúng ta sẽ dựa vào các khái niệm của máy hữu hạn trạng thái để xây dựng mô hình hệ thống kitchen timer.. - Biểu diễn: “Kitchen Timer. - Mô hình chuyển đổi trạng thái Hình 2: Mô hình chuyển đổi trạng thái của kitchen timer. - Chương này chúng ta sẽ biết cách sinh các ca kiểm thử một cách tự động bằng công cụ Spin. - Để có thể làm việc được với Spin chúng ta phải xây dựng mô hình của hệ thống bằng ngôn ngữ Promela. - Chương này sẽ lần lượt trình bày những khái niệm cơ bản về ngôn ngữ mô hình Promela, công cụ Spin, và giao diện người dùng XSpin.. - Xây dựng mô hình hệ thống bằng ngôn ngữ Promela là một công đoạn quan trọng trong kiểm thử dựa trên mô hình, để từ đó có thể dùng công cụ Spin sinh ra các ca kiểm thử. - Ngôn ngữ mô hình Promela có nhiều nét tương đồng với ngôn ngữ C.. - Promela là ngôn ngữ mô hình dùng để mô tả hệ thống đồng thời [The Spin Model Checker: Primer and Reference Manual]. - Ví dụ: Giao thức mạng, hệ thống điện thoại, các chương trình giao tiếp đa luồng,…. - Một biểu thức được xây dựng từ các biến, hằng số và sử dụng các toán tử sau đây:. - ::in_time==0. - Bởi vì kiểu dữ liệu mới này được tham chiếu tới các khai báo khác, vì vậy chúng ta phải chắc chắn rằng định nghĩa của nó được đặt đầu đoạn mã mô hình Promela. - Cấu trúc của ca kiểm thử: Input: Output:. - Label là nhãn của trạng thái tiếp theo,. - Alm_time là thời gian báo chuông, bTimeClk là trạng thái của đồng hồ (0 là OFF, 1 là ON). - Sau đây là một vài trạng thái trích trong ca kiểm thử được sinh ra từ chương trình ( tham khảo thêm tại Phụ lục B). - Trong khóa luận này tôi đã tìm hiểu lý thuyết cơ bản nhất về kiểm thử mô hình, bên cạnh đó tìm hiểu ngôn ngữ mô hình Promela từ đó áp dụng cho việc xây dựng một mô hình của hệ thống. - Sau khi xây dựng được mô hình của hệ thống, kết hợp nhúng mã C vào mô tả promela và sử dụng công cụ hỗ trợ kiểm thử Spin để tự động sinh ra các ca kiểm thử.. - Luận văn đã áp dụng lý thuyết đã tìm hiểu để tự động sinh ca kiểm thử cho ví dụ kitchen timer. - Kết quả thực nghiệm thu được là các ca kiểm thử, kết quả đó cho thấy ứng dụng là có ích, có thể sử dụng các ca kiểm thử đó để xác minh tính đúng đắn của phần mềm với thiết kế ban đầu của hệ thống.. - Tuy nhiên vì thời gian có hạn nên khóa luận mới chỉ dừng lại ở việc xây dựng mô hình từ đó tự động sinh các ca kiểm thử mà chưa kiểm tra trên cài đặt kitchen timer. - Bên cạnh đó chưa kiểm tra được tính đúng đắn của việc xây dựng mô hình so với yêu cầu của bài toán.. - Trong tương lai tôi sẽ tiếp tục nghiên cứu phương pháp giải quyết bài toán kiểm tra tính đúng đắn của việc xây dựng mô hình với mô tả ban đầu của hệ thống đồng thời kiểm tra trên chương trình thực tế.. - Phụ lục A: Đặc tả của kitchen timer bằng promela có nhúng mã C. - Kitchen timer. - in_time=0. - in_time. - Phụ lục B: Một số ca kiểm thử. - KIỂM THỬ DỰA TRÊN MÔ HÌNH