Các nguyên lý và kỹ thuật kiểm chứng chất lượng phần mềm

- Huỳnh Quyết Thắng Hà Nội – 2011 Trần Việt Hưng Cao học CNTT 2009 iiLỜI CAM ĐOAN Tôi xin cam đoan luận văn "Các nguyên lý và kỹ thuật kiểm chứng chất lượng phần mềm" do bản thân thực hiện dưới sự hướng dẫn của PGS.TS Huỳnh Quyết Thắng - Viện CNTT&TT - Trường Đại học Bách khoa Hà Nội, là không sao chép nguyên văn của bất kỳ một luận văn nào đã được công bố.
- Phương pháp nghiên cứu CHƯƠNG I: TỔNG QUAN VỀ KIỂM THỬ PHẦN MỀM Kiểm thử phần mềm Các phương pháp kiểm thử phần mềm Các chiến lược kiểm thử phần mềm Các giai đoạn kiểm thử phần mềm Kiểm thử đơn vị Kiểm thử tích hợp Kiểm thử hợp thức hoá Kiểm thử chấp nhận Kiểm thử hồi quy Các vấn đề của kiểm thử phần mềm Các hạn chế của kiểm thử Các nguyên tắc kiểm thử Phân loại một số công cụ kiểm thử tự động Kiểm chứng phần mềm Phương pháp Giả lập và kiểm thử (Simulation and Testing Phương pháp Kiểm chứng suy dẫn thường (Deductive Verification Phương pháp Kiểm chứng mô hình (Model Checking Trần Việt Hưng Cao học CNTT 2009 iv1.6.4 Sự khác nhau giữa Kiểm chứng mô hình phần mềm và kiểm thử phần mềm..14 1.7 Các phương pháp đặc tả và thiết kế phần mềm Phương pháp hình thức (formal method Phương pháp bán hình thức (semi-formal method Kết luận CHƯƠNG II: KIỂM CHỨNG MÔ HÌNH Tổng quan về kiểm chứng mô hình Quy trình kiểm chứng mô hình Mô hình hoá hệ thống (System Modeling Đặc tả các đặc tính (Properties Specification Kiểm chứng (Verification Các khái niệm cơ bản Đồ thị trạng thái Phân đoạn đường đi Phân đoạn đường đi cực đại và phân đoạn đường đi khởi tạo Đường đi Dấu vết và phân đoạn dấu vết Tính chất thời gian tuyến tính Tính bất biến, tính an toàn và tính sống còn Tính bất biến Tính an toàn Tính sống còn Logic thời gian tuyến tính (LTL Cú pháp của LTL Ngữ nghĩa Ngữ nghĩa của LTL (diễn tả thông qua Words.
- 48 2.6.4 Sử dụng Maude để kiểm chứng mô hình Kiểm chứng mô hình LTL dựa ô-tô-mát.
- 49 2.6.4.2 Kiểm chứng mô hình LTL trong Maude.
- 50 2.6.4.3 Kiểm chứng mô hình LTL.
- 57 2.7 Kết luận CHƯƠNG III: ÁP DỤNG MAUDE CHECKER KIỂM CHỨNG MÔ HÌNH MÔ PHỎNG READING PRACTISE Phát biểu bài toán Phương pháp giải quyết bài toán Đề xuất quy trình kiểm chứng mô hình sử dụng MaudeChecker Kiểm chứng mô hình phần mềm Reading Practise Đặc tả thuộc tính cần kiểm chứng Thiết kế Hệ thống Mô hình hóa Hệ thống bằng ngôn ngữ Maude Tính sống còn.
- Quy trình kiểm chứng mô hình Hình 2.2.
- Mô tả biểu đồ và hệ thống chuyển dịch Hình 2.11.
- Quy trình kiểm chứng mô hình LTL dựa ô-tô-mát Hình 2.13.
- Đồ thị nhập của các mô đun kiểm chứng mô hình Hình 3.1.
- Biểu đồ mô tả trạng thái của Hệ thống Hình 3.2.Kết quả kiểm tra Thuộc tính sống còn Hệ thống có thể đạt đến trạng thái kết thúc Hình 3.3.
- Kết quả kiểm tra Thuộc tính sống còn Hệ thống đảm bảo không luôn ở trạng thái đợi Hình 3.4.
- Kết quả kiểm tra Thuộc tính an toàn Hệ thống đảm bảo không tồn tại hai trạng thái kết thúc.
- Công nghệ phần mềm là một phần không thể tách rời trong công nghệ thông tin.
- Phần mềm được coi là sản phẩm chính của công nghệ phần mềm.
- Quá trình phát triển phần mềm gồm nhiều giai đoạn: thu thập yêu cầu, phân tích, thiết kế, xây dựng, kiểm chứng, triển khai và bảo trì.
- Trong đó việc kiểm chứng phần mềm là hết sức quan trọng để đảm bảo chất lượng một phần mềm.
- Trong công nghệ phần mềm, kiểm chứng phần mềm luôn thu hút được mối quan tâm của rất nhiều các nhà nghiên cứu.
- Vấn đề đặt ra ở đây là làm thế nào để phát triển, ứng dụng các phương pháp nhằm tăng độ tin cậy trong việc thiết kế và xây dựng phần mềm và hơn nữa các phương pháp này cần phải được tiến hành một cách tự động.
- Các phương pháp này sẽ cải thiện chất lượng và hạ giá thành cho việc phát triển hệ thống.
- Các phương pháp kiểm chứng cơ sở cho các hệ thống phức tạp bao gồm: Giả lập, kiểm thử, kiểm chứng suy dẫn và kiểm chứng mô hình.
- Trong tất cả các phương pháp kể trên, kiểm chứng mô hình (Model Checking)[3] là phương pháp cung cấp một cách tiếp cận toàn diện và hữu hiệu nhất để phân tích hệ thống.
- Với yêu cầu tìm hiểu, đề xuất, tổng hợp các nguyên lý, kỹ thuật kiểm chứng chất lượng phần mềm trong xây dựng phần mềm đạt chất lượng cao, tác giả đã chọn đề tài cho luận văn là: “Các nguyên lý và kỹ thuật kiểm chứng chất lượng phần mềm”.
- Lịch sử nghiên cứu Với sự phát triển như vũ bão của công nghệ thông tin nói chung và phần mềm nói riêng, việc phát triển phần mềm ngày càng được hỗ trợ bởi nhiều công cụ tiên tiến.
- Tuy nhiên, với yêu cầu ngày càng cao về chất lượng và cũng vì độ phức tạp của phần mềm và những giới hạn về thời gian, chi phí, nên việc phát triển phần mềm vẫn gặp phải những khó khăn trong các khâu như là đặc tả yêu cầu phần mềm và các kỹ thuật đánh giá chất lượng phần mềm.
- Maude cũng đã có những ứng dụng to lớn vào việc phát triển các hệ thống phần mềm chất lượng cao trong nhiều lĩnh vực.
- Tiếp thu thành tựu của các nhà khoa học đi trước, được PGS.TS Huỳnh Quyết Thắng hướng dẫn, tác giả đã cố gắng thực hiện đề tài: "Các nguyên lý và kỹ thuật kiểm chứng chất lượng phần mềm".
- Mục đích, đối tượng và phạm vi nghiên cứu 3.1 Mục đích Tìm hiểu, đề xuất, tổng hợp các nguyên lý, kỹ thuật kiểm chứng phần mềm trong xây dựng phần mềm đạt chất lượng cao.
- Trong luận văn, đã áp dụng các lý thuyết của kiến trúc phần mềm, đặc tả yêu cầu và kiểm chứng mô hình của phương pháp hình thức để kiểm chứng mô hình cho phần mềm Reading Practise.
- 3.2 Đối tượng Luận văn tìm hiểu các lý thuyết liên quan đến đánh giá chất lượng phần mềm, kiểm chứng phần mềm, kiểm chứng mô hình.
- công nghệ, giải pháp, công cụ của Maude[5] vào kiểm chứng mô hình cho ứng dụng phần mềm cụ thể.
- Do giới hạn nên luận văn chỉ mới ứng dụng kiểm chứng mô hình cho phần mềm Reading Practise.
- 3.3 Phạm vi nghiên cứu Cơ sở lý thuyết về các nguyên lý và kỹ thuật kiểm chứng chất lượng phần mềm vào việc phát triển phần mềm nói chung.
- Với ngôn ngữ lập trình Maude, tập Trần Việt Hưng Cao học CNTT 2009 3trung vào tìm hiểu cơ bản về ngôn ngữ lập trình Maude, cách thức kiểm chứng mô hình trong Maude.
- Cuối cùng là đề xuất quy trình đặc tả và kiểm chứng mô hình sử dụng MaudeChecker kiểm chứng cho phần mềm Reading Practise 4.
- Tổng quan các nguyên lý và kỹ thuật kiểm chứng chất lượng phần mềm.
- Chi tiết kỹ thuật kiểm chứng mô hình, logic thời gian tuyến tính và ngôn ngữ lập trình Maude.
- Cụ thể hóa việc kiểm chứng chất lượng phần mềm sử dụng kỹ thuật kiểm chứng mô hình và công cụng MaudeChecker với phần mềm Reading Practise và đưa ra kết quả của chương trình.
- Đã xây dựng thành công mô hình kiểm chứng (viết bằng ngôn ngữ Maude, sử dụng công cụ MaudeChecker.
- Phương pháp nghiên cứu - Tìm hiểu lý thuyết và kỹ thuật về kiểm chứng chất lượng phần mềm thông qua các nguồn tài liệu.
- Trần Việt Hưng Cao học CNTT 2009 4CHƯƠNG I: TỔNG QUAN VỀ KIỂM THỬ PHẦN MỀM 1.1 Kiểm thử phần mềm Ngày nay, với sự phát triển mạnh mẽ của lĩnh vực công nghệ thông tin, phần mềm đã thực sự trở thành một bộ phận quan trọng không thể thiếu trong hầu hết các lĩnh vực.
- Và càng ngày càng có nhiều hệ thống được điều khiển bởi phần mềm.
- Do đó, việc xây dựng, bảo trì và đặc biệt là kiểm định chất lượng hệ thống phần mềm là yêu cầu cần thiết đối với nền kinh toàn cầu và của từng quốc gia.
- Trong bối cảnh hầu hết các ngành kinh tế quan trọng đều đang sử dụng rộng rãi các hệ thống phần mềm thì có thể thấy, những lỗi phần mềm có thể gây ra những hậu quả nghiêm trọng về tiền bạc, thời gian, thậm chí sinh mạng của con người.
- Chất lượng phần mềm là một trong những mục tiêu chung mà mọi đối tượng liên quan trong việc sử dụng (người dùng), quản lý và phát triển (người xây dựng, lập trình) đều đặt lên vị trí hàng đầu khi đưa ra một vấn đề phát triển phần mềm.
- Trong các mô hình phát triển dù với quy mô bé hay lớn, đơn giản hay phức tạp.
- vấn đề kiểm thử phần mềm luôn được đặt lên hàng đầu, có tầm quan trọng không kém so với các vị trí phân tích và phát triển, và được thực hiện song song, xuyên suốt quá trình phát triển một hệ thống phần mềm.
- Kiểm thử phần mềm có nhiều cách định nghĩa khác nhau.
- Tuy nhiên, chúng cùng bao trùm hai nội dung cơ bản là phát hiện lỗi và đánh giá chất lượng của phần mềm.
- Định nghĩa sau đây của Myers là đơn giản và có tính thực tế: “Kiểm thử là tiến trình thực thi chương trình với mục đích tìm thấy lỗi”.
- Theo định nghĩa của Myers, kiểm thử mà không phát hiện được lỗi được coi là không thành công.
- Trần Việt Hưng Cao học CNTT 2009 5Mục đích của việc kiểm thử phần mềm[2]: Theo Deutch: “Phát triển hệ thống phần mềm gồm rất nhiều hoạt động sản xuất, và nguy cơ có lỗi là rất lớn.
- Kiểm thử phần mềm nhằm đảm bảo chất lượng phần mềm.
- Theo Glen Myers: Kiểm thử là tiến trình thực thi chương trình để tìm ra lỗi.
- Một trường hợp kiểm thử là trường hợp có xác suất cao để tìm ra lỗi chưa biểu hiện.
- Kiểm thử thành công khi phát hiện lỗi.
- Những mục đích trên ngược với quan điểm thông thường là “kiểm thử thành công là kiểm thử không tìm ra lỗi nào”.
- Nếu kiểm thử không phát hiện ra lỗi thì ta sẽ nghĩ rằng cấu hình kiểm thử này chưa đúng và lỗi vẫn còn tiềm ẩn trong phần mềm.
- Vậy kiểm thử thành công là kiểm thử tìm ra lỗi.
- Chúng ta cần phải nhớ rằng: “Kiểm thử không thể chứng minh được việc không có khiếm khuyết, nó chỉ có thể chứng minh rằng khiếm khuyết phần mềm hiện hữu.” 1.2 Các phương pháp kiểm thử phần mềm Có 2 phương pháp kiểm thử chính là: Kiểm thử tĩnh và Kiểm thử động.
- Kiểm thử tĩnh – Static testing Là phương pháp thử phần mềm đòi hỏi phải duyệt lại các yêu cầu và các đặc tả bằng tay, thông qua việc sử dụng giấy, bút để kiểm tra logic, lần từng chi tiết mà không cần chạy chương trình.
- Kiểu kiểm thử này thường được sử dụng bởi chuyên viên thiết kế người mà viết mã lệnh một mình.
- Kiểm thử động – Dynamic testing Là phương pháp thử phần mềm thông qua việc dùng máy chạy chương trình để điều tra trạng thái tác động của chương trình.
- Đó là kiểm thử dựa trên các ca kiểm thử xác định bằng sự thực hiện của đối tượng kiểm thử hay chạy các chương trình.
- Kiểm thử động kiểm tra cách thức hoạt động động của mã lệnh, tức là kiểm tra sự phản ứng vật lý từ hệ thống tới các biến luôn thay đổi theo thời gian.
- Trong kiểm thử động, phần mềm phải thực sự được biên dịch và chạy.
- Kiểm thử động thực sự bao gồm làm việc với phần mềm, nhập các giá trị đầu vào và kiểm tra xem liệu đầu ra có như mong muốn hay không.
- Các phương pháp kiểm thử động gồm có kiểm thử Unit – Unit Tests, Kiểm thử tích hợp – Intergration Tests, Kiểm thử hệ thống – System Tests, và Kiểm thử chấp nhận sản phẩm – Acceptance Tests.
- 1.3 Các chiến lược kiểm thử phần mềm Một chiến lược kiểm thử là một kế hoạch định nghĩa mục tiêu các giai đoạn kiểm thử cũng như các kỹ thuật kiểm thử sử dụng.
- Chiến lược kiểm thử thường được quyết định dựa vào tiêu chuẩn về độ tin cậy của phần mềm và chi phí cho việc phát triển phần mềm.
- Ngoài ra, một chiến lược kiểm thử sẽ phụ thuộc kích thước của đối tượng được kiểm thử cũng như quan điểm về đối tượng được kiểm thử.
- Nếu chúng ta muốn kiểm thử một cách độc lập các thành phần/đơn vị cấu tạo nên phần mềm, chúng ta gọi là kiểm thử đơn vị.
- Nếu chúng ta muốn kiểm thử sự kết hợp các thành phần cấu tạo nên phần mềm, chúng ta gọi là kiểm thử tích hợp.
- Nếu chúng ta muốn bảo đảm rằng một phần mềm đang được phát triển một cách đúng đắn và các thành phần cấu tạo nên phần mềm cũng được phát triển một cách đúng đắn, chúng ta gọi là xác minh.
- Tuy nhiên, một phần mềm không chỉ đơn thuần là đáp ứng yêu cầu của nhà sản xuất, mà nó chỉ trở nên hữu ích nếu đáp ứng được nhu cầu của người sử dụng cuối cùng.
- Việc bảo đảm một phần mềm đáp ứng nhu cầu của người sử dụng được gọi là hợp thức hoá.
- Trần Việt Hưng Cao học CNTT 2009 71.4 Các giai đoạn kiểm thử phần mềm Kiểm thử phần mềm gồm có giai đoạn: Kiểm thử đơn vị, Kiểm thử tích hợp, Kiểm thử hợp thức hóa, Kiểm thử chấp nhận sản phẩm và Kiểm thử hồi quy.
- 1.4.1 Kiểm thử đơn vị Phần lớn các phương pháp thiết kế phần mềm đều dẫn đến chia phần mềm thành những mô-đun hay chương trình nhỏ có các dữ liệu vào và kết quả riêng.
- Chúng ta gọi các mô-đun hay chương trình đó là các đơn vị phần mềm.
- Trên các đơn vị này chúng ta sẽ tiến hành kiểm thử đơn vị.
- Một khi đơn vị phần mềm đã được mã hoá, nghĩa là lập trình và hồ sơ kiểm thử đơn vị tương ứng đã được hoàn thành thì kiểm thử đơn vị có thể được tiến hành.
- Kiểm thử đơn vị chủ yếu là thực hiện các trường hợp kiểm thử đã được mô tả trong hồ sơ kiểm thử đơn vị và điền các thông tin cần thiết vào các phiếu báo cáo kiểm thử.
- Nếu một lỗi hay sự không tương thích được phát hiện, cần phải chỉnh sửa lại đơn vị phần mềm.
- Sau đó, kiểm thử đơn vị được thực hiện lại.
- Kiểm thử đơn vị sẽ kết thúc khi mà tất cả các trường hợp kiểm thử được mô tả trong hồ sơ kiểm thử đơn vị đã được thực hiện thành công và kết quả được lưu lại trong hồ sơ.
- 1.4.2 Kiểm thử tích hợp Kiểm thử tích hợp được tiến hành một khi kiểm thử đơn vị các thành phần cần thiết cho kiểm thử tích hợp kết thúc và hồ sơ kiểm thử tích hợp đã được chuẩn bị sẵn sàng.
- Trong giai đoạn kiểm thử tích hợp, ý tưởng là các thành phần đã được kiểm thử đơn vị sẽ được tích hợp lại dần dần cho đến khi có được toàn bộ phần mềm.
- Phần mềm càng phức tạp thì đòi hỏi giai đoạn kiểm thử tích hợp phải trải qua các giai đoạn trung gian, là các giai đoạn mà các nhóm các thành phần sẽ được kiểm thử.
- Mục tiêu của giai đoạn kiểm thử tích hợp là kiểm tra sự giao tiếp và trao đổi dữ liệu giữa các thành phần phần mềm.
- Tích hợp từ trên xuống bằng cách kiểm thử tích hợp các thành phần chính trước, sau đó thêm vào các thành phần được gọi trực tiếp bởi các thành phần vừa kiểm thử.
- Tích hợp từ dưới lên bằng cách kiểm thử các thành phần không gọi các thành phần khác, sau đó thêm vào các thành phần gọi các thành phần vừa kiểm thử.
- 1.4.3 Kiểm thử hợp thức hoá Kiểm thử hợp thức hoá có thể bắt đầu ngay sau khi kiểm thử tích hợp kết thúc và hồ sơ kiểm thử hợp thức hoá đã sẵn sàng.
- Mục tiêu của kiểm thử hợp thức hoá là cần chỉ ra rằng phần mềm thực hiện đúng những gì mà người sử dụng mong đợi.
- Vì thế, ở giai đoạn này, kiểm thử được thực hiện dưới góc nhìn của người sử dụng, chứ không phải dưới góc nhìn của người phát triển như các giai đoạn kiểm thử đơn vị hay kiểm thử tích hợp.
- Vì kiểm thử được thực hiện dưới góc nhìn của người sử dụng nên giai đoạn này chỉ sử dụng các kỹ thuật kiểm thử chức năng, tức là các kỹ thuật kiểm thử hộp đen.
- Thông thường các tài liệu đặc tả sẽ được phân tích để xác định các yêu cầu chứa đựng các hành vi mong đợi của phần mềm.
- 1.4.4 Kiểm thử chấp nhận Được thực hiện khi tất cả các giai đoạn kiểm thử được hoàn tất nhằm để chứng minh phần mềm đã đủ sẵn sàng xuất xưởng.
- Các thủ tục kiểm thử hoặc chạy thử phải được người đặt hàng chấp nhận trước khi thực hiện để nghiệm thu.
- 1.4.5 Kiểm thử hồi quy Phần mềm là một trong những loại sản phẩm thay đổi rất nhanh.
- Người sử dụng luôn có yêu cầu cải tiến phần mềm và các chức năng mới

Xem thử không khả dụng, vui lòng xem tại trang nguồn
hoặc xem Tóm tắt