Tài liệu Kết hợp phương pháp kiểm chứng mô hình và các kỹ thuật kiểm thử phần mềm làm tăng độ tin cậy của hệ thống phần mềm

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGÔ THỊ NGA KẾT HỢP PHƯƠNG PHÁP KIỂM CHỨNG MÔ HÌNH VÀ CÁC KỸ THUẬT KIỂM THỬ PHẦN MỀM LÀM TĂNG ĐỘ TIN CẬY CỦA HỆ THỐNG PHẦN MỀM LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 2014 1 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGÔ THỊ NGA KẾT HỢP PHƯƠNG PHÁP KIỂM CHỨNG MÔ HÌNH VÀ CÁC KỸ THUẬT KIỂM THỬ PHẦN MỀM LÀM TĂNG ĐỘ TIN CẬY CỦA HỆ THỐNG PHẦN MỀM Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ĐẶNG VĂN HƯNG Hà Nội – 2014 2 Lời cam đoan Tôi xin cam đoan rằng luận văn cao học này do chính tôi thực hiện. Những kết quả được tổng hợp và nghiên cứu từ các tài liệu tham khảo sử dụng trong luận văn này được thu thập từ các nguồn thông tin được công bố trên các sách báo, tạp chí khoa học chuyên ngành đáng tin cậy và kiến thức, kinh nghiệm của bản thân. Tôi hoàn toàn chịu trách nhiệm trước nhà trường về sự cam đoan này. Hà Nội, ngày 11 tháng 06 năm 2014 Học viên Ngô Thị Nga 3 Lời cảm ơn Em xin gửi lời cảm ơn chân thành tới các thầy cô giảng viên trong bộ môn Kỹ thuật phần mềm, khoa Công nghệ thông tin, trường Đại học Công nghệ đã giảng dạy và truyền đạt những kiến thức, kinh nghiệm cho em trong thời gian qua. Em xin được gửi lời cảm ơn sâu sắc nhất tới thầy giáo TS. Đặng Văn Hưng, thầy đã giúp đỡ, hướng dẫn và chỉ bảo cho em trong suốt quá trình học tập và thực hiện luận văn. Bên cạnh những kết quả mà em đạt được, em cũng không tránh khỏi những thiếu sót trong quá trình thực hiện luận văn, em kính mong các thầy cô thông cảm cho em. Sự góp ý, giúp đỡ của thầy cô sẽ là những kinh nghiệm quý báu cho quá trình học tập và làm việc của em sau này. Em kính chúc thầy cô luôn mạnh khỏe, công tác tốt và đạt được nhiều thành công trong cuộc sống cũng như trong sự nghiệp trồng người của mình. Hà Nội, ngày 11 tháng 06 năm 2014 Học viên Ngô Thị Nga 4 Mục lục Lời cam đoan ................................................................................................................... 2 Lời cảm ơn ....................................................................................................................... 3 Mục lục ............................................................................................................................ 4 Danh mục hình vẽ ............................................................................................................ 6 Danh mục bảng biểu ........................................................................................................ 7 Chương 1. Giới thiệu ....................................................................................................... 8 1.1. Đặt vấn đề ....................................................................................................8 1.2. Nội dung nghiên cứu....................................................................................8 1.3. Cấu trúc luận văn .........................................................................................9 Chương 2. Tổng quan về kiểm thử phần mềm .............................................................. 10 2.1. Tổng quan về kiểm thử phần mềm ............................................................ 10 2.1.1. Chất lượng phần mềm .........................................................................10 2.1.2. Kiểm thử và vai trò của kiểm thử .......................................................10 2.1.3. Các mục tiêu của kiểm thử .................................................................11 2.1.4. Ca kiểm thử ......................................................................................... 12 2.1.5. Các hoạt động kiểm thử ......................................................................12 2.1.6. Các mức độ kiểm thử ..........................................................................13 2.1.7. Các giới hạn của kiểm thử ..................................................................14 2.2. Các kỹ thuật kiểm thử phần mềm .............................................................. 14 2.2.1. Kỹ thuật phân lớp tương đương .......................................................... 15 2.2.2. Phương pháp kiểm thử đột biến (mutation testing) ............................ 15 Chương 3. Kiểm chứng mô hình ................................................................................... 19 3.1. Khái niệm kiểm chứng mô hình ................................................................ 19 3.2. Quy trình kiểm chứng mô hình ..................................................................21 3.3. Ưu và nhược điểm của kiểm chứng mô hình .............................................23 3.3.1. Ưu điểm của kiểm chứng mô hình......................................................23 3.3.2. Nhược điểm của kiểm chứng mô hình ................................................24 3.4. Logic thời gian tuyến tính (Linear Temporal Logic - LTL) ......................25 3.4.1. Trạng thái thời gian tuyến tính (Linear-Time Behavior) ....................25 3.4.2. Thuộc tính thời gian tuyến tính ........................................................... 27 3.4.3. Các thuộc tính an toàn (safety properties) ..........................................28 3.5. Các công cụ kiểm chứng mô hình ............................................................. 33 Chương 4. Ngôn ngữ Promela và công cụ kiểm chứng mô hình SPIN ........................ 35 4.1. Ngôn ngữ Promela .....................................................................................35 4.1.1 Kiểu dữ liệu, toán tử và câu lệnh ......................................................... 35 5 4.1.2. Dữ liệu và cấu trúc chương trình ........................................................37 4.1.3. Cấu trúc kiểu kênh thông điệp và tiến trình ........................................39 4.1.4. Một số hàm đặc biệt ............................................................................42 4.1.5. Biểu diễn các thuộc tính thời gian tuyến tính .....................................44 4.2. Kiểm chứng bằng công cụ SPIN ................................................................ 46 4.2.1. Công cụ SPIN .....................................................................................46 4.2.2. Kiểm chứng một chương trình bằng công cụ SPIN ............................ 48 Chương 5. Kết hợp kiểm chứng mô hình và các kỹ thuật kiểm thử phần mềm ............ 51 5.1. Ý nghĩa .......................................................................................................51 5.2. Mô hình đề xuất ......................................................................................... 51 5.3. Tính đúng đắn của cách tiếp cận ................................................................ 56 5.4. Ưu điểm và nhược điểm của cách tiếp cận ................................................57 Chương 6. Thực nghiệm ................................................................................................ 58 6.1. Mô tả bài toán thực nghiệm – bài toán ATM ............................................58 6.2. Xây dựng mô hình và kiểm chứng ............................................................. 59 6.2.1. Máy trạng thái hữu hạn mở rộng EFSM .............................................59 6.2.2. Mô hình hóa hệ thống bằng ngôn ngữ Promela ..................................60 6.2.3. Hình thức hóa và kiểm chứng các yêu cầu hệ thống .......................... 63 6.3. Biến đổi hệ thống bằng kỹ thuật kiểm thử đột biến ...................................65 6.3.1. Biến đổi mô hình hệ thống ..................................................................66 6.3.2. Biến đổi yêu cầu đặc tả của hệ thống..................................................67 6.4. Kết luận ......................................................................................................69 Kết luận.......................................................................................................................... 71 1. Kết quả của luận văn .....................................................................................71 2. Hướng nghiên cứu tiếp theo..........................................................................71 Tài liệu tham khảo ......................................................................................................... 72 Phụ lục .............................................................................................................................. i 6 Danh mục hình vẽ Hình 2.1 Mô hình chữ V trong phát triển phần mềm ....................................................13 Hình 2.2. Chương trình kiểm tra ba cạnh của tam giác .................................................16 Hình 3.1 Mối liên hệ giữa kiểm chứng hình thức, kiểm chứng mô hình và khái niệm hình thức ........................................................................................................................19 Hình 3.2 Cách tiếp cận kiểm chứng mô hình ................................................................ 21 Hình 4.1. Các toán tử trong ngôn ngữ Promela ............................................................. 36 Hình 4.2. Ví dụ về hoạt động của kênh .........................................................................39 Hình 4.3. Ví dụ về kênh gặp .......................................................................................... 40 Hình 4.4. Sơ đồ gửi nhận thông điệp trên kênh gặp ......................................................40 Hình 4.5. Sơ đồ gửi nhận thông điệp trong kênh đệm ..................................................41 Hình 4.6. Giao diện màn hình Edit trên iSPIN .............................................................. 46 Hình 4.7. Giao diện khung làm việc Simulate/ Replay .................................................47 Hình 4.8. Giao diện khung làm việc Verification ......................................................... 47 Hình 4.9. Kiến trúc của SPIN ........................................................................................48 Hình 4.10. Ví dụ về một chương trình có lỗi ................................................................ 49 Hình 4.11. Kiểm chứng chương trình trong hình 4.10 ..................................................49 Hình 4.12. Giả lập có hướng dẫn với Trial được tạo ra ở hình 4.9 ............................... 50 Hình 5.1. Kiểm thử đột biến hướng mô hình ................................................................ 52 Hình 5.2. Cách tiếp cận kiểm chứng mô hình kết hợp với kiểm thử đột biến ..............53 Hình 6.1. EFSM của máy rút tiền tự động ....................................................................60 Hình 6.2. Lược đồ truyền thông điệp trong máy ATM .................................................61 Hình 6.3. Các thông điệp trong máy ATM ....................................................................61 Hình 6.4. Các kênh thông điệp trong máy ATM ........................................................... 62 Hình 6.5. Hàm init khởi tạo các tiến trình .....................................................................62 Hình 6.6. Mã lệnh Promela của tiến trình Customer .....................................................63 Hình 6.7. Kết quả kiểm chứng với yêu cầu đặc tả thứ nhất ..........................................65 Hình 6.8. Kết quả kiểm chứng với yêu cầu đặc tả thứ hai ............................................65 Hình 6.9 Kết quả kiểm chứng mô hình với đặc tả sai Mutant 6 ....................................68 Hình 6.10. Kết quả kiểm chứng mô hình với đặc tả sai Mutant 7 .................................69 7 Danh mục bảng biểu Bảng 3.1. Các toán tử trong LTL ..................................................................................32 Bảng 3.2. Các toán tử thời gian trong LTL ...................................................................32 Bảng 3.3. Bảng chân giá trị ........................................................................................... 33 Bảng 4.1. Kiểu dữ liệu số của Promela .........................................................................35 Bảng 5.1. Các toán tử đột biến trong ngôn ngữ Promela ..............................................55 Bảng 5.2. Mối quan hệ giữa đặc tả và mô hình hệ thống ..............................................57 8 Chương 1. Giới thiệu 1.1. Đặt vấn đề Hàng ngày, mỗi chúng ta đều tiếp xúc với hàng trăm thiết bị điện tử, đồ gia dụng, máy vi tính ẩn chứa trong đó là những hệ thống máy tính và các chương trình ứng dụng phần mềm. Máy vi tính và các hệ thống thông tin đã đi sâu vào đời sống của mỗi người. Bất cứ một sai sót nào của các thiết bị này đều khó mà chấp nhận được, những sai lầm này đều phải trả giá bằng sinh mạng con người, bằng vật chất. Theo [3], ngày 04/06/1996, tàu vũ trụ Ariane-5 đã nổ tung ngay sau khi khởi động được 36 giây do lỗi chuyển đổi một số dạng dấu phẩy động 64-bit thành giá trị nguyên dương 16-bit. Theo [13], tháng 2-2014 Toyota đã phải thu hồi 1,9 triệu xe ôtô Prius trên toàn cầu vì lỗi lập trình hệ thống lai phối hợp hai hệ thống xăng và điện. Vì vậy độ tin cậy của các hệ thống máy tính là điều quan trọng nhất trong quá trình phát triển phần mềm. Các kỹ thuật kiểm thử cho chúng ta các chứng cứ về độ tin cậy của hệ thống. Vì các kỹ thuật này được thực hiện trên các mã lệnh của chương trình và tìm ra các lỗi phân tích, lỗi thiết kế và lỗi về đảm bảo tính dễ dùng của chương trình. Kiểm chứng mô hình (Model checking) là một kỹ thuật tự động kiểm tra tính đúng đắn của một mô hình được sinh ra từ hệ thống. Nếu mô hình thoả mãn được các đặc tả của hệ thống thì ta nói mô hình đó đúng đắn. Nếu mô hình không thoả mãn các đặc tả của hệ thống thì ta nói mô hình đó sai, và các phản ví dụ sẽ được tạo ra để chứng minh mô hình sai. Kiểm chứng mô hình được thực hiện tự động bởi các công cụ kiểm chứng (Model checker), và một trong những công cụ hiệu quả nhất là SPIN. Kiểm chứng mô hình la thực hiện kiểm tra bằng cách vét cạn các khả năng có thể xảy ra của mô hình trừu tượng. Nhưng trong quá trình kiểm chứng mô hình để cho việc kiểm chứng là thực hiện được, thì một số các tính chất, đặc tả chi tiết của chương trình đã bị loại bỏ. Vì vậy, dù một mô hình hệ thống đáp ứng được đặc tả của hệ thống, thì hệ thống thật chưa chắc đã đáp ứng được hết các đặc tả, mà ta cần tiến hành kiểm thử hệ thống. Cả hai phương pháp kiểm thử và kiểm chứng phần mềm đều nhằm mục đích là đảm bảo chất lượng và độ tin cậy cho hệ thống phần mềm. Mỗi phương pháp trên đều có những ưu, nhược điểm khác nhau mà người phát triển hệ thống có thể áp dụng vào quy trình phát triển phần mềm. Vì vậy, chúng ta kết hợp cả hai phương pháp này để đảm bảo tính tin cậy của hệ thống bằng việc sử dụng công cụ kiểm chứng SPIN và các kỹ thuật kiểm thử. 1.2. Nội dung nghiên cứu Luận văn tập trung nghiên cứu và khảo sát tổng quan về kiểm thử phần mềm và các kỹ thuật kiểm thử phần mềm; kỹ thuật kiểm chứng mô hình, các ưu, nhược điểm của nó và các thuộc tính thời gian; luận văn cũng nghiên cứu về ngôn ngữ Promela và sử dụng công cụ SPIN để kiểm chứng mô hình. Từ hiểu biết về kiểm thử phần mềm và 9 kiểm chứng mô hình, luận văn đưa ra phương pháp kết hợp hai kỹ thuật này. Đề tài thực hiện việc kiểm chứng trên mô hình bởi công cụ SPIN và sau đó tiến hành thẩm định chương trình bằng các kỹ thuật kiểm thử để làm tăng tính tin cậy của hệ thống. 1.3. Cấu trúc luận văn Luận văn có cấu trúc như sau: Chương 2 trình bày kiến thức tổng quan về kiểm thử phần mềm, và các kỹ thuật kiểm thử phần mềm. Chương 3 giới thiệu các khái niệm về kiểm chứng mô hình, ưu nhược điểm của kiểm chứng mô hình, logic thời gian, các thuộc tính thời gian, và logic thời gian tuyến tính. Chương 4 giới thiệu về ngôn ngữ Promela, các kiểu dữ liệu, các quy tắc trong lập trình, cách biểu diễn các thuộc tính thời gian tuyến tính và công cụ kiểm chứng SPIN. Chương 5 đề xuất mô hình kết hợp kiểm chứng mô hình và các kỹ thuật kiểm thử phần mềm. Việc ứng dụng công cụ kiểm chứng SPIN và các kỹ thuật kiểm thử để tăng tính tin cậy của hệ thống phần mềm sẽ được trình bày trong chương 6. Cuối cùng là kết luận về quá trình nghiên cứu, đưa ra các kết quả đạt được và hướng nghiên cứu tiếp theo. 10 Chương 2. Tổng quan về kiểm thử phần mềm Chương 2 trình bày tổng quan về kiểm thử phần mềm và các phương pháp kiểm thử phần mềm. 2.1. Tổng quan về kiểm thử phần mềm 2.1.1. Chất lượng phần mềm Trước khi nói về kiểm thử phần mềm, chúng ta cần hiểu rõ khái niệm “chất lượng phần mềm.” Theo [9], chất lượng phần mềm được đánh giá theo năm góc nhìn khác nhau như sau: Góc nhìn tiên nhiệm (Transcendental View): Chất lượng là một thứ gì đó dễ dàng thừa nhận nhưng khó để định nghĩa. Góc nhìn tiên nhiệm không đặc tả riêng rẽ được chất lượng phần mềm nhưng có thể ứng dụng vào những phần phức tạp khác nhau trong cuộc sống hàng ngày. Góc nhìn người dùng (User View): Chất lượng được cho là phải phù hợp với mục đích. Theo góc nhìn này thì khi đánh giá chất lượng của một sản phẩm, chúng ta phải đặt ra và trả lời cho một câu hỏi quan trọng là “Liệu sản phẩm có thỏa mãn yêu cầu và mong muốn của người dùng hay không?” Góc nhìn sản xuất (Manufacturing View): Ở đây, chất lượng được hiểu là sự đáp ứng được đặc tả. Chất lượng ở mức độ sản phẩm được xác định bởi việc là sản phẩm có gặp được đặc tả của nó hay không. Góc nhìn sản phẩm (Product View): Trong trường hợp này, chất lượng được xem như là một đặc tính vốn có của sản phẩm. Góc nhìn dựa vào giá trị (Value-Based View): Chất lượng, theo khía cạnh này phụ thuộc vào tổng giá trị mà khách hàng vui lòng trả cho nó. Khái niệm về chất lượng phần mềm và các nỗ lực để hiểu được nó theo một cách có thể định lượng được đã bắt đầu được nghiên cứu từ những năm 1970. Trong tài liệu về tiêu chuẩn ISO 9126 thì chất lượng phần mềm được định nghĩa trên sáu thuộc tính là: tính năng, tính đáp ứng, tính dễ dùng, tính hiệu quả, tính có thể bảo trì được và tính khả chuyển. Một ràng buộc về chất lượng là một thuộc tính của một yếu tố chất lượng liên quan đến quá trình phát triển phần mềm. 2.1.2. Kiểm thử và vai trò của kiểm thử Kiểm thử phần mềm đóng một vai trò quan trọng trong việc hoàn thành và đánh giá chất lượng của một sản phẩm phần mềm. Theo [9], chúng ta cải tiến chất lượng của sản phẩm bằng việc lặp đi lặp lại quá trình kiểm thử - tìm lỗi – sửa lỗi trong suốt quá trình phát triển. Mặt khác, chúng ta đánh giá cách hệ thống có thể hoạt động đúng khi chúng ta thực hiện kiểm thử ở mức hệ thống trước khi bàn giao sản phẩm. Theo Friedman và Voas đã mô tả thì kiểm thử phần mềm là một quá trình thẩm định cho việc đánh giá và cải thiện chất lượng phần mềm. 11 Thông thường, các hoạt động đánh giá phần mềm được chia làm hai loại là: phân tích tĩnh (static analysis) và phân tích động (dynamic analysis). Phân tích tĩnh là việc đánh giá chương trình mà không cần thực thi trên các mã lệnh của chương trình, nó có thể là các hoạt động xem xét (review) lại các tài liệu đặc tả, tài liệu thiết kế, tài liệu ca kiểm thử, hoặc là thanh tra mã nguồn (code inspection), … Phân tích động là việc đánh giá chương trình mà cần thực thi trên các mã lệnh của chương trình, trong đó có kỹ thuật kiểm thử hộp đen và hộp trắng. Bằng việc thực hiện phân tích tĩnh và phân tích động thì người kiểm thử viên mong muốn tìm được nhiều lỗi nhất có thể, để các lỗi này được sửa trong các giai đoạn sớm của quy trình phát triển phần mềm. Xác minh (Verification) và thẩm định (Validation) là những công việc xuyên suốt trong quá trình phát triển phần mềm, chứ không phải khi đã có mã nguồn của chương trình. Xác minh là sự kiểm tra xem phần mềm có thỏa mãn được yêu cầu đặc tả của hệ thống không? Nó trả lời cho câu hỏi “Hệ thống đã được xây dựng đúng theo đặc tả chưa?”, mục tiêu của xác minh là phát hiện các lỗi lập trình. Thẩm định là sự kiểm tra xem phần mềm có thỏa mãn được yêu cầu của người sử dụng không, nó chú trọng vào sản phẩm cuối cùng khi bàn giao cho khách hàng, mục tiêu là phát hiện các lỗi về thiết kế, về đặc tả. Một hệ thống xây dựng đúng đặc tả, nhưng chưa chắc đã đáp ứng được yêu cầu của khách hàng, vì đặc tả có thể sai, thiết kế có thể thiếu chi tiết. 2.1.3. Các mục tiêu của kiểm thử Theo tài liệu [7], các bên liên quan trong quy trình kiểm thử phần mềm bao gồm các lập trình viên, kiểm thử viên, quản trị dự án và khách hàng. Mỗi đối tượng này đều có những cái nhìn khác nhau về mục tiêu của kiểm thử. Chương trình hoạt động được: Các lập trình viên thường chỉ quan tâm đến khía cạnh là làm thế nào để chương trình hoạt động được trong các điều kiện thông thường. Chương trình không hoạt đông được: Lập trình viên ít khi quan tâm đến một khía cạnh khác của chương trình là khi nào thì chương trình không hoạt động được, làm thế nào khi chương trình bị lỗi. Giảm rủi ro của lỗi: Nhà quản trị phần mềm thường quan tâm đến khía cạnh là giảm rủi ro của lỗi gây ra. Hầu hết các hệ thống phần mềm phức tạp đều chứa lỗi - là nguyên nhân hệ thống thất bại. Bởi vậy nếu các lỗi được phát hiện và sửa trong khi thực hiện kiểm thử, tỷ lệ hệ thống gặp rủi ro sẽ giảm. Giảm chi phí của việc kiểm thử: Chi phí cho việc kiểm thử bao gồm chi phí thiết kế, bảo trì và thực thi các ca kiểm thử; chi phí phần tích kết quả thực hiện của mỗi ca kiểm thử; chi phí tài liệu hóa các ca kiểm thử và chi phí cho hệ thống hoạt động và tài liệu hóa các hoạt động đó. Khách hàng 12 thường mong muốn là giảm các chi phí của việc kiểm thử nhưng vẫn đảm bảo chất lượng. Mục tiêu chính của kiểm thử là có thể giám chi phí của việc kiểm thử bằng cách thiết kế các bộ ca kiểm thử hiệu quả bao phủ vùng kiểm thử tốt với số lượng ca kiểm thử ít hơn nhưng chất lượng vẫn được đảm bảo. 2.1.4. Ca kiểm thử Theo tài liệu [9], ca kiểm thử là một cặp . Ví dụ về các ca kiểm thử cho chương trình tính bình phương của một số là các cặp giá trị là <0, 0>, <2, 4>, <3, 9>, <10, 100> Trong các hệ thống không trạng thái (stateless systems), giá trị đầu ra chỉ phụ thuộc duy nhất vào giá trị đầu vào hiện tại, các ca kiểm thử thường rất đơn giản. Ví dụ như là chương trình tính bình phương của một số như ở trên. Trong các hệ thống hướng trạng thái (state-oriented systems), giá trị đầu ra của chương trình phụ thuộc vào cả trạng thái hiện tại của hệ thống và giá trị đầu vào hiện tại, thì một ca kiểm thử có thể chứa một chuỗi các cặp . Ví dụ như trong hệ thống ATM, hệ thống chuyển điện thoại, hệ thống đèn chiếu sáng và các hệ thống hướng trạng thái khác. 2.1.5. Các hoạt động kiểm thử Theo tài liệu [9], để kiểm thử một chương trình, một kỹ sư kiểm thử phải thực hiện một chuỗi các hoạt động như sau: Xác định đối tượng cần kiểm thử: Hoạt động đầu tiên là phải xác định được đối tượng kiểm thử. Đối tượng được xác định là mục đích để thiết kế một hay nhiều ca kiểm thử đảm bảo chương trình thỏa mãn đối tượng đó. Một đối tượng rõ ràng sẽ kết nối tới một ca kiểm thử. Lựa chọn các giá trị đầu vào: Việc lựa chọn này dựa vào đặc tả yêu cầu, mã nguồn hoặc mong muốn của chúng ta. Tính toán giá trị đầu ra mong muốn: Hoạt động thứ ba là tính toán giá trị đầu ra mong muốn của chương trình tương ứng với giá trị đầu vào. Thiết lập môi trường kiểm thử của chương trình: Chuẩn bị môi trường kiểm thử của chương trình, ở bước này tất cẩ các giả định ngoài của chương trình phải được thỏa mãn. Ví dụ: các hệ thống mạng, các cơ sở dữ liệu cần được thiết lập một cách đúng đắn. Tiến hành kiểm thử chương trình: Trong bước thứ năm, các kỹ sư kiểm thử thực hiện chương trình với các tập giá trị đầu vào và quan sát giá trị đầu ra thực tế của chương trình. Để thực hiện một ca kiểm thử, các giá trị đầu vào phải được cung cấp cho chương trình ở các thời điểm khác nhau. Phân tích kết quả kiểm thử: Bước cuối cùng là phân tích các kết quả kiểm thử để so sánh kết quả đầu ra thực tế với kết quả đầu ra mong muốn. Độ phức tạp của phép so sánh này phụ thuộc vào độ phức tạp của dữ liệu quan sát. Cuối 13 cùng là đưa ra quyết định về kết quả hoạt động của chương trình là thỏa mãn (pass), không thoải mãn (fail) yêu cầu của người dùng hay không đưa ra được quyết định. 2.1.6. Các mức độ kiểm thử Kiểm thử phần mềm là một chuỗi các hoạt động tiến hình song song cùng hoạt động phát triển phần mềm, từ lập kế hoạch và kiểm soát quá trình kiểm thử, phân tích yêu cầu và thiết kế ca kiểm thử, viết ca kiểm thử, tiến hành kiểm thử phần mềm, đánh giá các kết quả kiểm thử, báo cáo và tổng hợp các hoạt động kết thúc quá trình kiểm thử. Mô hình chữ V ở Hình 2.1 sẽ cho chúng ta thấy mối liên hệ giữa hoạt động phát triển và hoạt động kiểm thử. Hình 2.1 Mô hình chữ V trong phát triển phần mềm Các hoạt động kiểm thử bao gồm: kiểm thử đơn vị, kiểm thử tích hợp, kiểm thử hệ thống và kiểm thử chấp nhận. Mỗi hoạt động này tương ứng với các pha trong phát triển phần mềm từ đặc tả yêu cầu của khách hàng đến hoạt động lập trình. Kiểm thử đơn vị được các lập trình viên thực hiện độc lập trên các đơn vị chương trình, như là các lớp và các hàm. Kiểm thử tích hợp được thực hiện bởi các kỹ sư lập trình và kỹ sư kiểm thử phần mềm nhằm đảm bảo rằng chương trình có thể hoạt động đúng khi tích hợp các đơn vị lại với nhau. Kiểm thử tích hợp tương đương với việc kiểm tra thiết kế chi tiết, xem chương trình có thoải mãn thiết kế chi tiết hay không. Kiểm thử hệ thống được thực hiện bởi kỹ sư kiểm thử và sử dụng nhiều phương pháp, kỹ thuật khác nhau để tìm ra các lỗi, sửa lỗi và đảm bảo không phát sinh những lỗi mới. Kiểm thử hệ thống là một pha rất quan trọng trong quy trình phát triển phần 14 mềm nhằm đảm bảo chất lượng của phần mềm trước khi bàn giao sản phẩm cho khách hàng. Kiểm thử chấp nhận được thực hiện bởi khách hàng, những người sẽ kiểm tra xem phần mềm có đáp ứng được yêu cầu của người dùng hay không. Quá trình kiểm thử này không nhằm mục đích tìm ra lỗi mà là đo xem sản phẩm có đáp ứng được nhu cầu của người dùng hay không. 2.1.7. Các giới hạn của kiểm thử Lý tưởng nhất là tất cả các chương trình đều phải hoạt động đúng, không có lỗi xảy ra trong chương trình. Nhưng thực tế là để chứng minh được một chương trình là hoạt động đúng thì khách hàng và các nhà lập trình đều phải dựa vào việc kiểm thử phần mềm. Theo [9], ta xem xét đến hai giới hạn lớn của kiểm thử: Kiểm thử có nghĩa là thực thi một chương trình với một tập con đúng đắn của miền giá trị đầu vào của chương trình. Một tập con đúng đắn của miền giá trị đầu vào được chọn bởi vì các chi phí phần mềm không cho phép một tập con lớn hơn được chọn, ví dụ như là tập các đầu vào đầy đủ. Kiểm thử với tập các đầu vào đầy đủ được gọi là kiểm thử toàn diện (kiểm thử “vét cạn”). Vì vậy, cần kiểm thử một chương trình với một tập con nhỏ của miền giá trị đầu vào đặt ra một giới hạn cơ bản trên hiệu quả của việc kiểm thử. Mặt khác, cho dù một chương trình thỏa mãn một tập kiểm thử thì chúng ta cũng không thể kết luận rằng chương trình là hoàn toàn đúng đắn. Khi chúng ta chọn một tập con của miền giá trị đầu vào, chúng ta sẽ phải đối phó với vấn đề kiểm chứng tính đúng đắn của các giá trị đầu ra chương trình với các giá trị đầu vào riêng biệt. Cơ chế đánh giá tính đúng đắn của giá trị đầu ra chương trình được gọi là oracle (phán xét kiểm thử). Quyết định tính đúng đắn của một giá trị đầu ra của chương trình là một công việc không tầm thường. Một chương trình được xem xét là không thể kiểm thử được (nontestable) khi nó gặp phải hai vấn đề sau: o Không tồn tại một phán xét kiểm thử. o Quá khó để đưa ra quyết định đây có phải đầu ra đúng đắn. Nếu không có cơ chế để đánh giá tính đúng đắn của một đầu ra chương trình hoặc nó tốn quá nhiều thời gian để đánh giá đầu ra, thì sẽ không đạt được kết quả mong muốn của việc thực hiện kiểm thử. 2.2. Các kỹ thuật kiểm thử phần mềm Trong kiểm thử phần mềm, chúng ta thường dùng hai kỹ thuật chính là kiểm thử tĩnh (static testing) và kiểm thử động (dynamic testing). Kiểm thử động bao gồm các kỹ thuật: kiểm thử hộp đen (black box testing) và kiểm thử hộp trắng (white box testing). Kỹ thuật kiểm thử hộp đen là một kỹ thuật quan trọng trong hoạt động kiểm thử phần mềm, khái niệm “hộp đen” ở đây là chỉ việc kiểm thử viên không biết chương 15 trình bên trong được cài đặt như thế nào, họ chỉ biết rằng nó phải làm gì, và làm như thế nào để thỏa mãn các yêu cầu đặc tả - đã được cụ thể hóa thành các ca kiểm thử [9]. Một số phương pháp được áp dụng trong kỹ thuật kiểm thử hộp đen: kỹ thuật phân lớp tương đương (Equivalence partitioning), kỹ thuật phân tích giá trị biên (Boundary value analysis), kỹ thuật dùng bảng quyết định (Decision table), kỹ thuật dùng bảng chuyển trạng thái (State transition) và kỹ thuật kiểm thử ca sử dụng (Use case testing). Kỹ thuật kiểm thử hộp trắng là một kỹ thuật được áp dụng khi ta đã biết chương trình bên trong được lập trình như thế nào, cấu trúc chương trình, các dòng điều khiển, và dòng dữ liệu chạy ra sao. Kỹ thuật này thường tốn thời gian, công sức để thực hiện, nên thường chỉ áp dụng ở mức độ kiểm thử đơn vị - kiểm tra từng lớp, từng bộ phận mà không thực hiện ở các mức độ cao hơn. Các kỹ thuật kiểm thử hộp trắng là: kiểm thử luồng điều khiển, kiểm thử dòng dữ liệu và kiểm thử miền. Tuy có rất nhiều phương pháp kiểm thử phần mềm, nhưng trong nội dung của luận văn này, chúng ta đi sâu vào việc kết hợp kiểm chứng mô hình, kỹ thuật phân lớp tương đương và kỹ thuật kiểm thử đột biến. Vì vậy, luận văn sẽ trình bày rõ hơn về hai kỹ thuật phân lớp tương đương và kỹ thuật kiểm thử đột biến. 2.2.1. Kỹ thuật phân lớp tương đương Kỹ thuật phân lớp tương đương được áp dụng khi miền dữ liệu đầu vào quá lớn để có thể kiểm tra từng giá trị đầu vào. Miền giá trị đầu vào sẽ được chia thành một số hữu hạn các miền nhỏ hơn có tính chất giống nhau. Mỗi miền nhỏ hơn này sẽ được gọi là một phân lớp tương đương, các giá trị đầu vào trong một lớp tương đương sẽ cho cùng một kết quả đầu ra. Việc phân lớp tương đương sẽ làm giảm số lượng các ca kiểm thử, các bộ giá trị đầu vào. Số lượng bộ giá trị đầu vào giảm xuống còn bằng số lượng các miền nhỏ. Theo [7], ưu điểm của phương pháp phân hoạch tương đương là: Chỉ cần một số lượng nhỏ ca kiểm thử để có thể bao phủ cả một miền giá trị đầu vào lớn. Khả năng tìm ra lỗi trên cả miền bao phủ là cao hơn so với phương pháp lựa chọn miền giá trị đầu vào, và ca kiểm thử ngẫu nhiên. Phương pháp này áp dụng được cho cả miền giá trị đầu vào và miền giá trị đầu ra. 2.2.2. Phương pháp kiểm thử đột biến (mutation testing) Kiểm thử đột biến là một cách để đánh giá và cải tiến chất lượng của một bộ ca kiểm thử bằng việc kiểm tra nếu các ca kiểm thử của nó có thể phát hiện ra một số lỗi đã được chèn vào trong chương trình. Các lỗi thường được đưa vào chương trình bằng việc thay đổi cú pháp của mã nguồn theo các mẫu của lỗi lập trình thông thường. Những độ lệch (deviation) trong mã lệnh được gọi là các đột biến (mutants). Các phiên bản khác nhau của chương trình từ các lỗi này được gọi là các đột biến. Thường thì mỗi đột biến chỉ bao gồm một sự biến đổi. Ví dụ về các phép biến đổi thông thường 16 bao gồm việc đổi tên biến, thay thế các toán tử bằng các toán tử tương đương, thay đổi trong toán tử Boolean và biểu thức đại số. Ở đây, ta chỉ xem xét các phép biến đổi về cú pháp. Theo [1], số lượng và loại phép đột biến phụ thuộc vào ngôn ngữ lập trình và đã được xác định gọi là toán tử đột biến (mutation operators). Một toán tử đột biến là một luật được viết lại để định nghĩa cách các thuật ngữ cụ thể trong ngôn ngữ lập trình được thay thế bằng các đột biến. Với việc thay thế một toán tử đột biến vào trong chương trình gốc thì sẽ tạo ra một đột biến mới. Sau khi, tập các đột biến được sinh ra, các ca kiểm thử được chạy trên chương trình gốc và trên mỗi biến thể. Nếu ca kiểm thử có thể phát hiện được một đột biến trong chương trinh gốc, ví dụ như là ca kiểm thử vượt qua được trong chương trình gốc nhưng trượt trong một đột biến, thì chúng ta nói rằng ca kiểm thử này đã “loại bỏ” (kill) được một đột biến. Mục tiêu là phát triển một bộ các ca kiểm thử có thể loại bỏ được tất cả các đột biến. Theo [9], tỷ lệ đột biến (Mutation score) của một tập kiểm thử là tỷ lệ phần trăm số các đột biến bị loại bỏ bởi tập các ca kiểm thử. 1 proctype tritype (int a; int b; int c) { 2 do 3 :: (a <= c-b) -> printf (" This is not a triangle\n"); 4 :: (a <= b-c) -> printf (" This is not a triangle\n"); 5 :: (b <= a-c) -> printf (" This is not a triangle\n"); 6 :: (a == b && b == c) -> printf (" This is a equilateral\n"); 7 :: (a == b) -> printf (" This is a isosceles\n"); 8 :: (b == c) -> printf (" This is a isosceles\n"); 9 :: (c == a) -> printf (" This is a isosceles\n"); 10 ::else -> printf (" This is a scalene\n"); 11 od 12 } 13 active proctype main() 14 { 15 run tritype (3, 5, 7); 16 } Hình 2.2. Chương trình kiểm tra ba cạnh của tam giác Hình 2.2 là đoạn mã bằng ngôn ngữ PROMELA (ngôn ngữ của công cụ SPIN) kiểm tra ba cạnh của tam giác và trả về kết quả là loại tam giác. Ví dụ về toán tử đột biến có thể viết lại là mỗi dấu “==” sẽ được thay thế bằng dấu “>=”. Chúng ta có năm biến thể, tương đương với năm phép biến đổi trong chương trình. Ta có một tập các ca kiểm thử của chương trình là: TC1: <(1, 2, 2), isosceles> TC2: <(2, 1, 2), isosceles> TC3: <(2, 2, 1), isosceles> TC4: <(3, 3, 3), equilateral> TC5: <(1, 3, 5), not a triangle> 17 TC6: <(1, 5, 3), not a triangle> TC7: <(5, 3, 1), not a triangle> TC8: <(3, 4, 5), scalene> Ta có các phép biến đổi của chương trình như sau: Mutant 1: biến đổi dòng 6 thành :: (a >= b && equilateral\n"); b == c) -> printf (" This is a c) -> printf (" This is a Mutant 2: biến đổi dòng 6 thành :: (a == b && equilateral\n"); b >= Mutant 3: biến đổi dòng 7 thành :: (a >= b) -> printf (" This is a isosceles\n"); Mutant 4: biến đổi dòng 8 thành :: (b >= c) -> printf (" This is a isosceles\n"); Mutant 5: biến đổi dòng 9 thành :: (a >= c) -> printf (" This is a isosceles\n"); Nếu ta chạy lại chương trình sau khi đã biến đổi cùng với bộ ca kiểm thử, chúng ta sẽ thu được kết quả sau: Mutant 1 và Mutant 2: tất cả các ca kiểm thử đều thỏa mãn. Nói cách khác là Mutant 1 và Mutant 2 không bị “kill”. Mutant 3: chương trình bị lỗi ở TC4 và TC7. Mutant 4: chương trình bị lỗi ở TC4, TC6 và TC7. Mutant 5: chương trình bị lỗi ở TC4 và TC7. Nếu tính toán tỷ lệ đột biến, chúng ta sẽ thấy rằng với năm đột biến thì chỉ ba trong năm đột biến được phát hiện ra, và tỷ lệ là 60%. Vì thế ta cần thêm các ca kiểm thử để phát hiện ra đột biến Mutant 1 và Mutant 2. TC9: (<3, 2, 2>, isosceles) TC10: (<3, 3, 2>, isosceles) Lúc này thì bộ ca kiểm thử mới phát hiện được hết các đột biến, và tỷ lệ đột biến bây giờ là 100%. Theo [9], kỹ thuật kiểm thử đột biến được thực hiện qua các bước sau: Bước 1: Bắt đầu với một chương trình P, và một tập các ca kiểm thử T cho trước được cho là chính xác. Bước 2: Thực hiện các ca kiểm thử trong tập T trên chương trình P. Nếu một ca kiểm thử bị lỗi, có nghĩa là đầu ra của chương trình không đúng, 18 chương trình P cần phải thay đổi và kiểm thử lại. Nếu không có lỗi xảy ra, ta tiếp tục thực hiện bước 3. Bước 3: Tạo một bộ các đột biến {Pi}, mỗi đột biến là một thay đổi nhỏ trong cú pháp của chương trình P. Bước 4: Thực hiện các ca kiểm thử trong T trên mỗi đột biến Pi. Nếu đầu ra của đột biến Pi khác với đầu ra của chương trình gốc P, thì đột biến Pi được xem là không chính xác và bị loại bỏ bởi ca kiểm thử. Nếu Pi có kết quả đầu ra chính xác như kết quả của chương trình gốc P khi kiểm thử trong T thì một trong các trường hợp sau là đúng: o P và Pi là tương đương. Có nghĩa là hành vi của chúng không khác nhau bởi bất kỳ tập các ca kiểm thử nào. Lưu ý là rất khó để đánh giá được là P và Pi tương đương trong thực tế. o Pi có thể bị loại bỏ. Có nghĩa là, các ca kiểm thử đã không loại bỏ được đột biến Pi. Trong trường hợp này, các ca kiểm thử mới sẽ được tạo ra. Bước 5: Tính toán tỷ lệ đột biến của tập các ca kiểm thử T. Tỷ lệ đột biến = , trong đó D là các đột biến đã bị loại bỏ, N là tổng số đột biến, E là số đột biến tương đương. Bước 6: Nếu tỷ lệ đột biến ở bước 5 là không cao, thì cần phải thiết kế các ca kiểm thử mới phân biệt Pi với P, thêm các ca kiểm thử mới vào tập T, vào quay lại bước 2. Nếu tỷ lệ đột biến ở mức độ tương đương với kỳ vọng, thì chấp nhận tập T như là một độ đo tốt cho tính đúng đắn của chương trình P với tập các đột biến Pi,và ngừng thiết kế các ca kiểm thử mới. Theo [9], kiểm thử đột biến đưa ra hai giả định quan trọng: Giả thuyết các lập trình viên có trình độ (Competent Programmer Hypothesis): giả sử rằng các lập trình viên đều có trình độ, họ không tạo ra các chương trình một cách ngẫu nhiên. Chúng ta có thể giả sử rằng một lập trình viên sẽ viết ra các chương trình đúng đắn với một vài lỗi nhỏ. Các lỗi nhỏ này được xem như là một sự sai lệch nhỏ so với chương trình gốc. Các lỗi này thường được gọi là các toán tử đột biến, gây ra những sai lệch nhỏ một cách có hệ thống trong chương trình. Hiệu ứng cặp đôi (Coupling Effect): Giả định này được đưa ra vào năm 1978 bởi nhà khoa học deMillo và đồng sự. Giả định này nói rằng các lỗi phức tạp là những cặp lỗi đơn giản và nếu mà một bộ kiểm thử phát hiện ra tất cả các lỗi đơn giản trong chương trình thì sẽ phát hiện ra các lỗi phức tạp. Kiểm thử đột biến giúp cho các kiểm thử viên có thể tự tin về chương trình của mình. Nhưng số lượng các đột biến được sinh ra, và các ca kiểm thử để loại bỏ được nó là rất lớn. Vì vậy, chúng ta cần có chiến lược để có thể áp dụng kỹ thuật kiểm thử đột biến một cách hiệu quả. 19 Chương 3. Kiểm chứng mô hình Chương 3 trình bày các khái niệm về kiểm chứng mô hình, quy trình thực hiện việc kiểm chứng mô hình, các ưu nhược điểm, thuộc tính của mô hình và các công cụ để kiểm chứng. 3.1. Khái niệm kiểm chứng mô hình Trước khi nói về kiểm chứng mô hình, thì chúng ta cần nhắc đến khái niệm về các phương pháp hình thức (formal methods). Theo [3], các phương pháp hình thức được coi như là việc áp dụng các kiến thức toán học ứng dụng vào việc mô hình hoá và phân tích các hệ thống thông tin. Các phương pháp hình thức là một trong những kỹ thuật thẩm định các hệ thống thông tin được đánh giá cao. Ngày nay, các phương pháp hình thức, và kiểm chứng hình thức đã được áp dụng trong các viện nghiên cứu và giảng dạy trong các trường đại học. Kỹ thuật kiểm chứng dựa vào mô hình là căn cứ vào mô hình mô tả các hành vi có thể của hệ thống bằng các công thức toán học chính xác và không nhập nhằng. Các mô hình hệ thống được đi kèm theo bởi các thuật toán dò tìm tất cả các trạng thái của mô hình hệ thống một cách tự động. Điều này cung cấp các nền tảng cho một loạt các kỹ thuật thẩm định từ thăm dò vét cạn (kiểm chứng mô hình) tới kiểm tra bằng thực nghiệm trên mô hình (mô phỏng) hoặc trên thực tế (kiểm thử). Kiểm chứng mô hình là một kỹ thuật trong kiểm chứng hình thức (Formal Verification). Nó nằm trong mối tương quan giữa đặc tả hình thức (Formal Specification) và sự tổng hợp hình thức (Formal Synthesis). Hình 3.1 Mối liên hệ giữa kiểm chứng hình thức, kiểm chứng mô hình và khái niệm hình thức Kiểm chứng mô hình (Model checking) là một kỹ thuật automat dùng để kiểm chứng các hệ phản vệ (re-active systems) có hữu hạn trạng thái, ví dụ như là các thiết