Khóa luận Kiểm thử dựa trên mô hình

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Đoàn Trung Kiên KIỂM THỬ DỰA TRÊN MÔ HÌNH KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin HÀ NỘI - 2010 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Đoàn Trung Kiên KIỂM THỬ DỰA TRÊN MÔ HÌNH KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin Cán bộ hướng dẫn: TS. Phạm Ngọc Hùng Cán bộ đồng hướng dẫn: ThS. Đặng Việt Dũng HÀ NỘI - 2010 Kiểm thử dựa trên mô hình Đoàn Trung Kiên i LỜI CẢM ƠN Lời đầu tiên em xin bày tỏ lòng biết ơn sâu sắc tới TS. Phạm Ngọc Hùng và ThS. Đặng Việt Dũng, các thầy đã hướng dẫn em tận tình trong suốt năm học vừa qua. Em xin bày tỏ lòng biết ơn tới các thầy, cô giáo trong Khoa Công nghệ thông tin - Trường Đại học Công nghệ - ĐHQGHN. Các thầy cô đã dạy bảo, chỉ dẫn em và luôn tạo điều kiện tốt nhất cho em học tập trong suốt quá trình học đại học đặc biệt là trong thời gian làm khoá luận tốt nghiệp. Con xin chân thành cảm ơn Ông Bà, Cha Mẹ đã luôn động viên, ủng hộ vật chất lẫn tinh thần trong suốt thời gian qua. Tôi xin cảm ơn sự quan tâm, giúp đỡ và ủng hộ của anh chị, bạn bè, đặc biệt là các bạn sinh viên lớp K51CB trường Đại học Công nghệ trong quá trình thực hiện khóa luận. Mặc dù đã cố gắng hoàn thành khóa luận trong phạm vi và khả năng cho phép nhưng chắc chắn sẽ không tránh khỏi những thiếu sót. Em rất mong nhận được sự thông cảm, góp ý và tận tình chỉ bảo của quý Thầy Cô và các bạn. Hà Nội, ngày 05 tháng 05 năm 2008 Đoàn Trung Kiên Kiểm thử dựa trên mô hình Đoàn Trung Kiên ii TÓM TẮT 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. Từ đó áp dụng các kỹ thuật trên vào bài toán cụ thể kitchen timer. Kiểm thử dựa trên mô hình Đoàn Trung Kiên iii MỤC LỤC CHƯƠNG 1 GIỚI THIỆU.......................................................................................1 1.1 Đặt vấn đề.....................................................................................................1 1.2 Nội dung nghiên cứu của khóa luận ..............................................................1 1.3 Cấu trúc khóa luận ........................................................................................1 CHƯƠNG 2 CƠ SỞ LÝ THUYẾT CHO KIỂM THỬ MÔ HÌNH...........................3 2.1 Khái niệm kiểm thử dựa trên mô hình ...........................................................3 2.2 Các bước thực hiện .......................................................................................3 2.3 Thuận lợi và khó khăn của kiểm thử dựa trên mô hình ..................................4 2.4 Máy hữu hạn trạng thái ( Finite State Machines ) ..........................................5 2.5 Bài toán Kitchen Timer .................................................................................6 2.5.1 Miêu tả bài toán .....................................................................................6 2.5.2 Xây dựng mô hình .................................................................................6 CHƯƠNG 3 GIỚI THIỆU PROMELA VÀ SPIN....................................................8 3.1 Ngôn ngữ Promela ........................................................................................8 3.1.1 Khái niệm cơ bản...................................................................................8 3.1.2 Biến và Kiểu ..........................................................................................9 3.1.3 Định danh, Hằng số và Biểu thức.........................................................10 3.1.4 Tiến trình .............................................................................................11 3.2 Công cụ Spin ..............................................................................................12 3.2.1 Sơ lược về Spin....................................................................................12 3.2.2 Công cụ XSpin.....................................................................................12 CHƯƠNG 4 SINH CA KIỂM THỬ TỰ ĐỘNG VÀ THỰC NGHIỆM .................21 4.1 Phương pháp sinh các ca kiểm thử tự động .................................................21 4.2 Ví dụ áp dụng..............................................................................................22 4.2.1 Mô tả bài toán......................................................................................23 4.2.2 Máy hữu hạn trạng thái của Kitchen Timer ..........................................23 4.2.3 Đặc tả kitchen timer bằng promela có nhúng mã C ..............................24 4.2.4 Kết quả ................................................................................................30 CHƯƠNG 5 KẾT LUẬN ......................................................................................32 Phụ lục A: Đặc tả của kitchen timer bằng promela có nhúng mã C ........................33 Phụ lục B: Một số ca kiểm thử ...............................................................................42 TÀI LIỆU THAM KHẢO......................................................................................44 Kiểm thử dựa trên mô hình Đoàn Trung Kiên iv DANH MỤC HÌNH VẼ Hình 1: Các bước thực hiện kiểm thử mô hình. . ......................................................4 Hình 2: Mô hình chuyển đổi trạng thái của kitchen timer. ........................................7 Hình 3: Màn hình cửa sổ chính của XSpin. ............................................................13 Hình 4: Cửa sổ chức năng Run Slicing algorithm...................................................14 Hình 5: Cửa sổ chính chức năng Set Simulation Parameters. .................................15 Hình 6: Cửa sổ khi chạy chức năng Run Simulation. .............................................16 Hình 7: Cửa sổ chính chức năng Set Verification Parameters.................................17 Hình 8: Cửa sổ khi chạy chức năng Run Verification.............................................18 Hình 9: Cửa sổ khi chạy chức năng LTL Property Manager...................................19 Hình 10: Cửa sổ khi chạy chức năng View Spin Automaton. .................................20 Hình 11: Kiến trúc hệ thống kitchen timer. ............................................................23 Hình 12: Mô hình máy hữu hạn trạng thái kitchen timer. .......................................24 Kiểm thử dựa trên mô hình Đoàn Trung Kiên 1 CHƯƠNG 1 GIỚI THIỆU 1.1 Đặt vấn đề 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 đó. Hoặc khi nhóm lập trình đư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 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, 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 đó. Điều này khó khả thi về mặt thời gian nếu kiểm tra thông thường. Để 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. 1.2 Nội dung nghiên cứu của khóa luận 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. 1.3 Cấu trúc khóa luận Các phần còn lại của khóa luận có cấu trúc như sau: Kiểm thử dựa trên mô hình Đoàn Trung Kiên 2 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. Chương 5 tóm tắt các kết quả đã đạt được, kết luận, những hạn chế và hướng nghiên cứu phát triển trong tương lai. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 3 CHƯƠNG 2 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. 2.1 Khái niệm kiểm thử dựa trên 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. 2.2 Các bước thực hiện 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 ). Khi chạy kịch bản 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ử,… 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.  Tạo đầu ra dự kiến từ mô tả bài toán.  Chạy kịch bản kiểm thử.  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 ) 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: Kiểm thử dựa trên mô hình Đoàn Trung Kiên 4 Hình 1: Các bước thực hiện kiểm thử mô hình. 2.3 Thuận lợi và khó khăn của kiểm thử dựa trên mô hình  Thuận lợi 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à Kiểm thử dựa trên mô hình Đoàn Trung Kiên 5 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.  Có khả năng đánh giá chất lượng phần mềm.  Khó khăn 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. 2.4 Máy hữu hạn trạng thái ( Finite State Machines ) 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: Kiểm thử dựa trên mô hình Đoàn Trung Kiên 6 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. T : Tập hợp hàm chuyển đổi trạng thái khi đầu vào là một trạng thái cụ thể. 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. 2.5 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. 2.5.1 Miêu tả bài toán Kitchen timer là một thiết bị hẹn giờ đơn giản dùng trong nhà bếp. Chúng ta ấn nút SW1 để thiết lập thời gian cho hệ thống, ấn nút SW2 để bắt đầu đếm ngược thời gian. Thời gian có thể thiết lập được là 1 phút đến 3 phút (đơn vị thời gian thiết lập là phút). Thời gian thiết lập được hiển thị bằng 2 đèn LED. Khi đếm ngược thời gian, 2 đèn LED sẽ nhấp nháy. Nếu đang trong lúc đang đếm ngược, ấn nút SW1 thì đếm ngược sẽ bị dừng (trở về trạng thái thiết lập), ấn nút SW2 thì đếm ngược sẽ tạm thời dừng. Nếu đếm ngược kết thúc (thời gian trở về 0) thì 2 đèn LED sẽ cùng sáng trong vòng 3 giây để thông báo cho người dùng biết. 2.5.2 Xây dựng mô hình  Biểu diễn: “Kitchen Timer” = (I, S, T, F, L) trong đó: I = {, , , ,<Đếm ngược kết thúc>} S = {[Chờ], [Thiết lập thời gian], [Đếm ngược], [Tạm dừng]} T: Thay đổi từ [Chờ] sang [Thiết lập thời gian] Thay đổi từ [Thiết lập thời gian] sang [Đếm ngược] Thay đổi từ [Đếm ngược] sang [Tạm dừng] Thay đổi từ [Tạm dừng] sang [Đếm ngược] Thay đổi từ [Đếm ngược] sang [Chờ] Kiểm thử dựa trên mô hình Đoàn Trung Kiên 7 F = [Chờ] L = [Chờ]  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. Thiết lập Đếm ngược Chờ Thiết lập thời gian Đếm ngược Tạm dừng Tiếp tục Tạm dừng Đếm ngược kết thúc Kiểm thử dựa trên mô hình Đoàn Trung Kiên 8 CHƯƠNG 3 GIỚI THIỆU PROMELA VÀ SPIN 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. 3.1 Ngôn ngữ Promela 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. 3.1.1 Khái niệm cơ bản  Định nghĩa Promela (Process meta language ) 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,…  Cấu trúc chương trình Promela Một chương trình Promela cơ bản gồm:  Khai báo kiểu.  Khai báo biến.  Khai báo tiến trình.  [init process]. // Các khai báo kiểu và biến mtype = {MSG, ACK}; chan toS = ... chan toR = ... bool flag; // Một tiến trình Kiểm thử dựa trên mô hình Đoàn Trung Kiên 9 proctype Sender() { // Thân một tiến trình ... } proctype Receiver() { ... } // Tiến trình init init { // Tạo một tiến trình ... } 3.1.2 Biến và Kiểu Giống như nhiều ngôn ngữ lập trình khác, Promela yêu cầu các biến phải được khai báo trước khi chúng có thể được sử dụng. Khai báo biến theo phong cách của ngôn ngữ lập trình C. Theo mặc định tất cả các biến của các loại biến cơ bản được bắt đầu từ 0. Cũng như trong C thì 0 được coi như sai và khác 0 được coi là đúng. Một biến có thể là biến toàn cục hoặc là biến địa phương của mỗi tiến trình.  Kiểu dữ liệu Type Domain bit or bool { 0, 1} byte 0…255 short -215 … 215 - 1 int -231 … 231 – 1  Kiểu khai báo int ii; bit bb; bb = 1; ii = 2;  Kiểu cấu trúc Records (structs): Có thể tìm ra xung đột khi chạy Typedef record{ short f1; Kiểm thử dựa trên mô hình Đoàn Trung Kiên 10 byte f2; } Truy cập như C Record rr; rr.f1 = …  Kiểu mảng Một mảng có cấu trúc như sau: int table[max] Lưu ý rằng điều này tạo ra một mảng max-1 số nguyên: table[0], table[1], ... table[max-1]  Kiểu liệt kê Một bộ các hằng số tượng trưng được khai báo như sau: mtype = {LINE_CLEAR, TRAIN_ON_LINE, LINE_BLOCKED} 3.1.3 Định danh, Hằng số và Biểu thức  Định danh Định danh có thể là một chữ cái, một ký tự.  Hằng số Hằng số là một chuỗi ký tự đại diện cho một số nguyên thập phân. Hằng số tượng trưng có thể được định nghĩa như sau: #define MAX 999  Biểu thức 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: +, -, *, /, %, --, ++, >, >=, <, <=, ==, !=, &&, ||, !, Kiểm thử dựa trên mô hình Đoàn Trung Kiên 11 &, |, ~, ^, >>, <<, !, ?, (), [], 3.1.4 Tiến trình  Một tiến trình được khai báo bắt đầu bằng một từ khóa proctype và gồm có: Tên Danh sách thông số chính Khai báo biến cục bộ Thân chương trình  Cú pháp của một khai báo tiến trình proctype name( /* formal parameter list */ ) { /* các khai báo địa phương và các lệnh */ … } /* và */ quy định giới hạn chú thích trong promela  Tiến trình init Tất cả các chương trình promela đều cần một tiến trình init nó giống như hàm main() trong ngôn ngữ C. Việc thực thi một chương trình promela được bắt đầu từ tiến trình init. Một tiến trình init có dạng: init { /* Các khai báo địa phương và các biểu thức. */ } Đơn giản nhất có thể là chương trình promela có dạng: init { skip } Skip có nghĩa là không có biểu thức nào trong tiến trình init; Kiểm thử dựa trên mô hình Đoàn Trung Kiên 12 Mỗi tiến trình được định nghĩa bởi một proctype, nó được thực thi đồng thời với tất cả các tiến trình khác, nó giao tiếp với các tiến trình khác thông qua việc sử dụng các biến công cộng hoặc các kênh. Tiến trình thực thi sau khi thực hiện hàm run. 3.2 Công cụ Spin 3.2.1 Sơ lược về Spin Spin là công cụ mã nguồn mở, phổ biến và được sử dụng bởi hàng ngàn người trên toàn cầu. Nó được sử dụng cho việc xác minh thẩm định của các hệ thống phân phối phần mềm. Từ năm 1980 Spin được phát triển tại Bell Labs của nhóm Unix thuộc trung tâm nghiên cứu Khoa học máy tính. Phần mềm này phát triển rộng rãi từ năm 1991. Tháng 4 năm 2002 Spin được trao giải thưởng phần mềm uy tín cho năm 2001 của ACM. Spin cung cấp một giả lập cho phép các nhà thiết kế đạt được kết quả phản hồi từ hệ thống mô hình của họ. Những kết quả phản hồi đó đóng vai trò quan trọng trong sự hiểu biết của các nhà thiết kế về hệ thống trước khi họ đầu tư vào phân tích chính thức. 3.2.2 Công cụ XSpin Có giao diện thân thiện người dùng cửa sổ soạn thảo chính với khả năng chỉnh sửa và tìm kiếm là đơn giản. XSpin là công cụ thuận tiện để tiếp cận với Spin. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 13 Hình 3: Màn hình cửa sổ chính của XSpin.  Run Syntax Check  Kiểm tra cú pháp ngôn ngữ Promela.  Luôn luôn là bước đầu tiên sau khi thay đổi chương trình Promela. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 14 Hình 4: Cửa sổ chức năng Run Slicing algorithm.  Run Slicing Algorithm  Xác định những thành phần không liên quan của mô hình.  Biểu diễn sự phân tích lưu lượng dữ liệu.  Set Simulation Parameters (Hỗ trợ gỡ lỗi quan trọng nhất) Thiết lập thông số hiển thị:  Message Sequence Chart (MSC) Panel: Cung cấp quá trình giao tiếp theo thời gian. Kiểm soát cách trình bay các liên kết giữa MSC và Promela bên trong của sổ văn bản chính được hỗ trợ thông qua bảng điều khiển này.  Time Sequence Panel: Cung cấp quá trình giao tiếp theo thời gian.  Data Values Panel: Trình bay dữ liệu theo thời gian. Tùy chọn gồm các kênh đệm các biến địa phương và biến toàn cục. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 15  Random : Yêu cầu người sử dụng cung cấp một giá trị seed. Hình 5: Cửa sổ chính chức năng Set Simulation Parameters.  Run Simulation  Việc thiết lập các thông số hiển thị phải được thực hiện ít nhất một lần trước khi thực hiện chạy Simulation.  Việc thiết lập mặc định thông số hiển thị sẽ sinh ra 3 của sổ sau:  Simulation Output: Cung cấp 2 phương thức : Chạy từng bước (Single Step) hoặc chạy liên tục (Run).  Data Values.  Sequence Chart. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 16 Hình 6: Cửa sổ khi chạy chức năng Run Simulation.  Thiết lập thông số Verification Kiểm tra mô hình. Đảm bảo thực hiện an toàn và xác minh tính chất.  Correctness Properties: Safety, Liveness.  Search mode.  A full queue.  Verify an LTL property.  Set advance options. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 17 Hình 7: Cửa sổ chính chức năng Set Verification Parameters.  Run Verification  Set verification parameters.  (Re)run verification. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 18 Hình 8: Cửa sổ khi chạy chức năng Run Verification.  LTL Temporal Logic Formulae LTL = Mệnh đề Logic + toán tử điều khiển thời gian. Giúp chỉnh sửa và bảo trì các công thức logic. Theo thời gian trong Spin  Bước 1: Chạy “LTL Property Manager”  Bước 2: Nhập vào đặc tính thời gian mà bạn muốn thẩm định. Chú ý phải là biểu thức bất biến và tên bằng chữ thường.  Bước 3: Chỉ ra là có hay không đặc tính thời gian cần giữ: all executions (desired behaviour) hoặc no executions (error behaviour)  Bước 4: Nhập vào một định nghĩa vi mô đối với mỗi hằng số mệnh đề trong của sổ phụ “Symbol Definitions” Kiểm thử dựa trên mô hình Đoàn Trung Kiên 19  Bước 5: Ấn vào nút “Run Verification” và tiếp tục ấn vào nút “Run” trong của sổ “LTL Verification” Chú ý là những thông số của LTL có thể lưu lại để sử dụng trong tương lai bằng nút “Save As” và “Load” Hình 9: Của sổ khi chạy chức năng LTL Property Manager.  View Spin Automaton (FSM View) Kiểm thử dựa trên mô hình Đoàn Trung Kiên 20 Hình 10: Của sổ khi chạy chức năng View Spin Automaton. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 21 CHƯƠNG 4 SINH CA KIỂM THỬ TỰ ĐỘNG VÀ THỰC NGHIỆM Sau khi thiết kế mô hình hệ thống bằng ngôn ngữ mô hình Promela, kết hợp nhúng mã C vào đặc tả promela và sử dụng công cụ hỗ trợ kiểm chứng Spin để tự động sinh các ca kiểm thử. Kitchen Timer là một ví dụ nhỏ được tiến hành để đánh giá các phương pháp đã đề xuất. 4.1 Phương pháp sinh các ca kiểm thử tự động Từ mô tả các yêu cầu và chức năng xác định của hệ thống cùng với dữ liệu đầu vào, ra ta thiết kế mô hình của hệ thống. Mô hình đó biểu diễn không gian các trạng thái có thể đạt được của hệ thống. Nhúng một đoạn mã nguồn C vào đặc tả promela để khi dịch chuyển giữa các trạng thái thì ta hiển thị ra các trạng thái đó một cách tự động. Ta có thể sử dụng một ngăn xếp để lưu các trạng thái đó lại. Cấu trúc của ngăn xếp có thể định nghĩa như sau: typedef struct Node{ char state[256]; char input[256]; char output[256]; }Node; #define MAXSIZE 1000000 Node State_Stack[MAXSIZE]; Tiếp theo tới mỗi trạng thái ta lưu trạng thái đó và ngăn xếp: char tempLable[256] ="FIRST"; char tempInput[256] = ""; char tempOutput[256] = ""; Node tempNode = {"FIRST","",""}; Kiểm thử dựa trên mô hình Đoàn Trung Kiên 22 void setNode(char* cur_label, char* cur_input, char* cur_output) { strcpy(tempNode.label,cur_label); strcpy(tempNode.input, cur_input); strcpy(tempNode.output, cur_output); } In ra trạng thái đó: void printNode(Node n) { printf("Input: %s\n",n.input); printf("Output: %s\n",n.output); printf("STATE\n",n.label); } 4.2 Ví dụ áp dụng Áp dụng các phương pháp đã đề xuất ở được tìm hiểu trong khóa luận cho bài toán Kitchen Timer. Kitchen timer một thiết bị hẹn giờ đơn dùng trong các nhà bếp. Đầu vào của thiết bị thông qua 2 nút bấm SW1 và SW2. Đầu ra là thông qua 2 đèn báo hiệu LED. Timer CPU Flash Memory RAM LED LED SW1 SW2 IO Port Kiểm thử dựa trên mô hình Đoàn Trung Kiên 23 Hình 11: Kiến trúc hệ thống kitchen timer. 4.2.1 Mô tả bài toán  Khởi động kitchen timer Bật công tắc khởi động kitchen timer. Khi bạn bắt đầu chương trình cả hai đèn LED đã được chờ đợi ở chế độ tắt.  Thiết lập thời gian Thiết lập thời gian bằng công tắc 1. Thiết lập thời gian được hiển thị ở đèn LED ở dạng số nhị phân. Thời gian thiết lập là từ 1 tới 3 phút.  Bắt đầu tính giờ Bắt đầu đồng hồ đếm ngược bằng công tắc 2. Nếu đồng hồ bắt đầu đếm ngược thì đèn LED sẽ nháy.  Tạm dừng  Nếu bấm công tắc 1 trong khi đang tính giờ, thì sẽ kết thúc việc tính giờ và cả 2 đèn LED sẽ tắt hoàn toàn.  Nếu bấm công tắc 2 thì đồng hồ đếm ngược tạm dừng và đèn LED cũng dừng. Bấm lại công tắc 2 lần nữa thì đồng hồ tiếp tục tính giờ và đèn LED tiếp tục nháy.  Hiển thị thời gian hết và báo động Nếu kết thúc thời gian đã thiết lập,chuông báo hiệu sẽ khởi động để thông báo cho người sử dụng, đèn LED sẽ nhấp nháy trong vòng 3 giây. Trong khi báo động nếu bấm công tắc 1 hoặc công tắc 2 chuông báo động ngừng lại, và đèn LED sẽ tắt. Ngoài ra trong khi dừng chuông báo hiệu nếu lại thiết lập thời gian bằng công tắc 1 và bấm công tắc 2 thì đồng hồ đếm ngược lại bắt đầu. 4.2.2 Máy hữu hạn trạng thái của Kitchen Timer Từ những thông số kỹ thuật được mô tả ở trên chúng ta xây dựng được mô hình máy trạng thái của Kitchen Timer như hình vẽ sau. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 24 Hình 12: Mô hình máy hữu hạn trạng thái kitchen timer. Bộ Yếu tố Ý nghĩa Nhãn NUMINPUT COUNTDOWN PAUSE ALARM ALARMOFF Thiết lập thời gian Đếm ngược Tạm dừng Báo giờ Ngừng báo giờ Biến in_t t alarm_t Biến đại diện cho thời gian thiết lập Biến đại diện cho thời gian đếm ngược Biến đại diện cho thời gian báo chuông Kiểm thử dựa trên mô hình Đoàn Trung Kiên 25 bTimeClk Biến đại diện cho hoạt động chu kỳ Đặt biểu tượng đầu vào xSTART xTIME_SET TIMER_CLK Thông báo hoạt động từ SW2 Thông báo hoạt động từ SW1 Thông báo hoạt động dựa vào chu kỳ Đặt biểu tượng đầu ra Thời gian thiết lập Đặt lại thời gian thiết lập Đặt lại thời gian đếm ngược Đặt lại thời gian báo thức Đặt thời gian đếm ngược Stop clock Start clock Giá trị in_t có thể là 0, 1, 2, 3 in_t = 0 t = 0 alarm_t = 0 t = in_t * 6 bTimeClk = 0 bTimeClk = 1 4.2.3 Đặc tả kitchen timer bằng promela có nhúng mã C Mô tả Kitchen Timer bằng Promela gồm hai tiến trình song song gồm : Bộ hẹn giờ (Timer) và các hành động của môi trường (Trigger). Tiến trình Timer mô tả sự tính toán thời gian. Tiến trình Trigger xử lý và giám sát để mô tả nhiệm vụ trọng tâm. Một đoạn mã mô tả tiến trình Timer() (tham khảo Phụ lục A). /* Tien trinh Timer() */ proctype Timer() { mtype evt; /*-------------------------------------------------------------------*/ /* Thiet lap thoi gian */ NUMINPUT_ST: Kiểm thử dựa trên mô hình Đoàn Trung Kiên 26 printf("TIMER: ST NUMINPUT\n"); NUMINPUT: c_code{ strcpy(tempLabel,"NUMINPUT"); setNode(tempLabel,now.in_time,now.time,now.alm_time,now.bTime Clk,tempInput,tempOutput); printNode(tempNode); }; GetEvtTimer(evt); if ::evt==TIMER_CLK -> atomic{ MUSI; c_code{ strcpy(tempInput,"TIME_CLK"); strcpy(tempOutput, ""); } } ::evt==xTIME_SET -> IncInTime(); atomic { printf("NumDsp.\n"); c_code{ Kiểm thử dựa trên mô hình Đoàn Trung Kiên 27 strcpy(tempInput,"xTIME_SET"); strcpy(tempOutput,"Increase InTime"); } } ::evt==xSTART -> if ::in_time==0 -> atomic{ MUSI; c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, ""); } } ::else -> SetTime(); SetTimerClk(ON); printf("STA_CNTDOWN.\n"); atomic{ c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, "Set Time = InTime * 6; Start clock"); }; Kiểm thử dựa trên mô hình Đoàn Trung Kiên 28 goto COUNTDOWN_ST; } fi; fi; goto NUMINPUT; …. Đoạn mã mô tả tiến trình Environment. /* Tien trinh Environment */ proctype Environment(){ do ::true -> SetEvtTimer(xTIME_SET); ::true -> SetEvtTimer(xSTART); ::true -> if ::bTimeClk==1 -> SetEvtTimer(TIMER_CLK); ::bTimeClk==0 -> ; fi od }  C_decl sẽ định nghĩa một kiểu dữ liệu mới tên Node. Để tránh xung đột trùng tên, thì tên kiểu dữ liệu mới này không được trùng với bất kỳ tên dữ liệu nào đã tồn tại trong Spin. Trình biên dịch C sẽ thông báo nếu điều này vô tình xảy ra. Spin không tự phát hiện ra những xung đột này. Kiểm thử dựa trên mô hình Đoàn Trung Kiên 29 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. Đoạn mã c_decl chỉ để định nghĩa kiểu dữ liệu mới C trong Promela. Đoạn mã định nghĩa dữ liệu Node. c_decl{ typedef struct Node{ char label[256]; /* Nhan cua trang thai tiep theo */ int in_time; /*Thoi gian thiet lap*/ int time; /*Thoi gian dem nguoc*/ int alm_time; /*Thoi gian bao dong*/ unsigned bTimeClk; /*Chu ky dieu khien*/ char input[256]; /* bieu tuong dau vao */ char output[256]; /* bieu tuong dau ra */ }Node; }… Đoạn mã sau có nhiệm vụ thiết lập các thông số cho dữ liệu kiểu Node và in ra input, output và các trạng thái cùng các thông số của nó. Đoạn mã lưu các trạng thái vào Node và in ra Node. c_code{ char tempLabel[256] = "NUMINPUT"; char tempInput[256] = ""; char tempOutput[256] = ""; Node tempNode = {"NUMINPUT",0,0,0,0,"",""}; void setNode(char* cur_label, int cur_in_time, int cur_time, int cur_alm_time, unsigned cur_bTimeClk, char* cur_input, char* cur_output) { strcpy(tempNode.label,cur_label); Kiểm thử dựa trên mô hình Đoàn Trung Kiên 30 tempNode.in_time = cur_in_time; tempNode.time = cur_time; tempNode.alm_time = cur_alm_time; tempNode.bTimeClk = cur_bTimeClk; strcpy(tempNode.input, cur_input); strcpy(tempNode.output, cur_output); } void printNode(Node n) { printf("Input: %s\n",n.input); printf("Output: %s\n",n.output); printf("STATE\n",n.label,n.in_time,n.tim e,n.alm_time,n.bTimeClk); } }; 4.2.4 Kết quả Cấu trúc của ca kiểm thử: Input: Output: STATE Trong đó: Input là biểu tượng đầu vào, Output là biểu tượng đầu ra, Label là nhãn của trạng thái tiếp theo, In_time là thời gian thiết lập, Time là thời gian của đồng hồ đếm ngược, Alm_time là thời gian báo chuông, Kiểm thử dựa trên mô hình Đoàn Trung Kiên 31 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). Input: Output: STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xSTART Output: STATE Input: xSTART Output: STATE Input: xSTART Output: STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xSTART Output: Set Time = InTime * 6; Start clock STATE Input: xTIME_SET Output: Clear InTime; Clear Time; Stop clock STATE Kiểm thử dựa trên mô hình Đoàn Trung Kiên 32 CHƯƠNG 5 KẾT LUẬN 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ụ luc A Đoàn Trung Kiên 33 Phụ lục A: Đặc tả của kitchen timer bằng promela có nhúng mã C /* Kitchen timer */ /* Nhung ma C */ /* Cau truc du lieu cho mot Node */ c_decl{ typedef struct Node{ char label[256]; /*Nhan cua trang thai tiep theo */ int in_time; /*Thoi gian thiet lap*/ int time; /*Thoi gian dem nguoc*/ int alm_time; /*Thoi gian bao dong*/ unsigned bTimeClk; /*Chu ky dieu khien*/ char input[256]; /* bieu tuong dau vao */ char output[256]; /* bieu tuong dau ra */ }Node; } c_code{ char tempLabel[256] = "NUMINPUT"; char tempInput[256] = ""; char tempOutput[256] = ""; Node tempNode = {"NUMINPUT",0,0,0,0,"",""}; /* Thiet lap gia tri cho cac Node */ void setNode(char* cur_label, int cur_in_time, int cur_time, int cur_alm_time, unsigned cur_bTimeClk, char* cur_input, char* cur_output) { strcpy(tempNode.label,cur_label); tempNode.in_time = cur_in_time; tempNode.time = cur_time; tempNode.alm_time = cur_alm_time; tempNode.bTimeClk = cur_bTimeClk; strcpy(tempNode.input, cur_input); strcpy(tempNode.output, cur_output); } /* In ra cac Node */ void printNode(Node n) { printf("Input: %s\n",n.input); printf("Output: %s\n",n.output); printf("STATE\n",n.label,n.in_time, n.time,n.alm_time,n.bTimeClk); Phụ luc A Đoàn Trung Kiên 34 } }; /*----------------------------------------------------*/ #define ON 1 #define OFF 0 #define MUSI skip mtype = {xTIME_SET, xSTART, TIMER_CLK } chan chanTimer = [0] of {mtype}; bool bTimeClk=0; int in_time=0; int time=0; int alm_time=0; /* Dat lai thoi gian thiet lap */ inline ClrInTime() { in_time=0; } /* Cap nhat thoi gian */ inline IncInTime() { in_time++; in_time=in_time&3; } /* Thiet lap thoi gian */ inline SetInTime(value) { in_time=value; } /* Dat lai thoi gian dem nguoc */ inline ClrTime() { time=0; } /* Thiet lap thoi gian dem nguoc */ inline SetTime() { time=in_time*6; } /* Dat lai thoi gian bao chuong */ inline ClrAlmTime() { alm_time=0; } /*Thong bao dong ho la ON hay OFF*/ inline SetTimerClk( value ) { d_step{ bTimeClk=value; if ::value==OFF ->printf("TIMER: STP TIMER_CLK\n") ::value==ON ->printf("TIMER: STA TIMER_CLK\n") fi } } inline SetEvtTimer( evt ) { chanTimer!evt } inline GetEvtTimer( evt ) { chanTimer?evt } Phụ luc A Đoàn Trung Kiên 35 /*----------------------------------------------------*/ /* Tien trinh Timer() */ proctype Timer() { mtype evt; /*----------------------------------------------------*/ /* Thiet lap thoi gian */ NUMINPUT_ST: NUMINPUT: c_code{ strcpy(tempLabel,"NUMINPUT"); setNode(tempLabel,now.in_time,now.time,now.alm_time ,now.bTimeClk,tempInput,tempOutput); printNode(tempNode); }; GetEvtTimer(evt); if ::evt==TIMER_CLK -> atomic{ MUSI; c_code{ strcpy(tempInput,"TIME_CLK"); strcpy(tempOutput, ""); } } ::evt==xTIME_SET -> IncInTime(); atomic { c_code{ strcpy(tempInput,"xTIME_SET"); strcpy(tempOutput,"Increase InTime"); } } ::evt==xSTART -> if ::in_time==0 -> atomic{ MUSI; c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, ""); } } Phụ luc A Đoàn Trung Kiên 36 ::else -> SetTime(); SetTimerClk(ON); /* Bat dong ho */ atomic{ c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, "Set Time = InTime * 6; Start clock"); }; /* Chuyen sang trang thai COUNTDOWN */ goto COUNTDOWN_ST; } fi; fi; goto NUMINPUT; /*----------------------------------------------------*/ /* Dem nguoc */ COUNTDOWN_ST: COUNTDOWN: c_code{ strcpy(tempLabel,"COUNTDOWN"); setNode(tempLabel,now.in_time,now.time,now.alm_time ,now.bTimeClk,tempInput,tempOutput); printNode(tempNode);}; GetEvtTimer(evt); if ::evt==TIMER_CLK -> time--; if ::time>0 -> atomic{ MUSI; c_code{ strcpy(tempInput,"TIMER_CLK"); strcpy(tempOutput, "Time--"); } } ::else -> ClrAlmTime(); atomic{ c_code{ strcpy(tempInput,"TIMER_CLK"); strcpy(tempOutput, "Time--; Clear AlarmTime"); Phụ luc A Đoàn Trung Kiên 37 }; /* Chuyen sang trang thai ALARM */ goto ALARM_ST; } fi; ::evt==xTIME_SET -> ClrInTime(); ClrTime(); SetTimerClk(OFF); /* Tat dong ho */ atomic{ c_code{ strcpy(tempInput,"xTIME_SET"); strcpy(tempOutput, "Clear InTime; Clear Time; Stop clock"); }; /* Chuyen sang trang thai NUMINPUT */ goto NUMINPUT_ST; } ::evt==xSTART -> SetTimerClk(OFF); /* Tat dong ho */ atomic{ c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, "Stop clock"); }; /* Chuyen sang trang thai PAUSE */ goto PAUSE_ST; } fi; goto COUNTDOWN; /*------------------------------------------------------ -------------*/ /* Tam dung */ PAUSE_ST: PAUSE: c_code{ strcpy(tempLabel,"PAUSE"); setNode(tempLabel,now.in_time,now.time,now.alm_time ,now.bTimeClk,tempInput,tempOutput); printNode(tempNode); }; GetEvtTimer(evt); if ::evt==TIMER_CLK -> Phụ luc A Đoàn Trung Kiên 38 atomic{ MUSI; c_code{ strcpy(tempInput,"TIMER_CLK"); strcpy(tempOutput, ""); } } ::evt==xTIME_SET -> ClrInTime(); ClrTime(); atomic{ c_code{ strcpy(tempInput,"xTIME_SET"); strcpy(tempOutput, "Clear InTime; Clear Time"); }; /* Chuyen sang trang thai NUMINPUT */ goto NUMINPUT_ST; } ::evt==xSTART -> SetTimerClk(ON); atomic{ c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, "Start clock"); }; /* Chuyen sang trang thai COUNTDOWN */ goto COUNTDOWN_ST; } fi; goto PAUSE; /*------------------------------------------------------ -------------*/ /* Bao gio */ ALARM_ST: ALARM: c_code{ strcpy(tempLabel,"ALARM"); setNode(tempLabel,now.in_time,now.time,now.alm_time ,now.bTimeClk,tempInput,tempOutput); printNode(tempNode); }; GetEvtTimer(evt); if Phụ luc A Đoàn Trung Kiên 39 ::evt==TIMER_CLK -> if ::alm_time atomic{ alm_time++; c_code{ strcpy(tempInput,"TIMER_CLK"); strcpy(tempOutput, "AlarmTime++"); } } ::else -> ClrAlmTime(); SetTimerClk(OFF); atomic{ c_code{ strcpy(tempInput,"TIMER_CLK"); strcpy(tempOutput, "Clear AlamrTime; Stop clock"); }; /* Chuyen sang trang thai ALARM_OFF */ goto ALARM_OFF_ST; } fi; ::evt==xTIME_SET -> ClrAlmTime(); SetTimerClk(OFF); atomic{ c_code{ strcpy(tempInput,"xTIME_SET"); strcpy(tempOutput, "Clear AlamrTime; Stop clock"); }; /* Chuyen sang trang thai ALARM_OFF */ goto ALARM_OFF_ST; } ::evt==xSTART -> ClrAlmTime(); SetTimerClk(OFF); atomic{ c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, "Clear AlamrTime; Stop clock"); }; /* Chuyen sang trang thai ALARM_OFF */ goto ALARM_OFF_ST; } Phụ luc A Đoàn Trung Kiên 40 fi; goto ALARM; /*------------------------------------------------------ -------------*/ /* Ngung bao gio */ ALARM_OFF_ST: ALARM_OFF: c_code{ strcpy(tempLabel,"ALARMOFF"); setNode(tempLabel,now.in_time,now.time,now.alm_time ,now.bTimeClk,tempInput,tempOutput); printNode(tempNode); }; GetEvtTimer(evt); if ::evt==TIMER_CLK -> atomic{ MUSI; c_code{ strcpy(tempInput,"TIMER_CLK"); strcpy(tempOutput, ""); } } ::evt==xTIME_SET -> SetInTime(1); atomic{ c_code{ strcpy(tempInput,"xTIME_SET"); strcpy(tempOutput, "Set InTime = 1"); }; /* Chuyen sang trang thai NUMINPUT */ goto NUMINPUT_ST; } ::evt==xSTART -> SetTime(); SetTimerClk(ON); atomic{ c_code{ strcpy(tempInput,"xSTART"); strcpy(tempOutput, "Set Time = InTime * 6; Start clock"); }; ;/* Chuyen sang trang thai COUNTDOWN */ Phụ luc A Đoàn Trung Kiên 41 goto COUNTDOWN_ST } fi; goto ALARM_OFF; } /*----------------------------------------------------*/ /* Tien trinh Environment */ proctype Environment(){ do ::true -> SetEvtTimer(xTIME_SET); ::true -> SetEvtTimer(xSTART); ::true -> if ::bTimeClk==1 -> SetEvtTimer(TIMER_CLK); ::bTimeClk==0 -> ; fi od } /*------------------------------------------------------ -------------*/ /* Tien trinh init */ init{ run Timer(); /* Chay tien trinh Timer() */ run Environment(); /*Chay tien trinh Environment()*/ } Phụ luc B Đoàn Trung Kiên 42 Phụ lục B: Một số ca kiểm thử Input: Output: STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xSTART Output: STATE Input: xSTART Output: STATE Input: xSTART Output: STATE Phụ luc B Đoàn Trung Kiên 43 Input: xTIME_SET Output: Increase InTime STATE Input: xTIME_SET Output: Increase InTime STATE Input: xSTART Output: Set Time = InTime * 6; Start clock STATE Input: xTIME_SET Output: Clear InTime; Clear Time; Stop clock STATE Input: TIME_CLK Output: STATE Input: TIME_CLK Output: STATE Input: TIME_CLK Output: STATE Input: xSTART Output: Set Time = InTime * 6; Start clock STATE Input: xSTART Output: Stop clock STATE … Tài liệu tham khảo Đoàn Trung Kiên 44 TÀI LIỆU THAM KHẢO [1] Andrew Ireland. Distributed Systems Programming F21DS1. Promela School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh [2] By Nedret OZAY. Automated Software Test Generation. Model-Based Testing, 2007 [3] El-Far and JA Whittaker. Model-Based Software Testing. Encyclopedia of Software Engineering (edited by J. J. Marciniak). Wiley, 2001 [4] Gerard Holzmann. The Spin Model Checker. Primer and Reference Manual. Addison Wesley, 2003 [5] [6] [7]