Nghiên cứu phương pháp sinh dữ liệu kiểm thử phần mềm dựa trên kỹ thuật kiểm chứng mô hình

  • Số trang: 53 |
  • Loại file: PDF |
  • Lượt xem: 21 |
  • Lượt tải: 0
nhattuvisu

Đã đăng 26946 tài liệu

Mô tả:

2 GIA HÀ NỘI ĐẠI HỌC QUỐC TRƢỜNG ĐẠI HỌC CÔNG NGHỆ PHAN VĂN TIẾN NGHIÊN CỨU PHƢƠNG PHÁP SINH DỮ LIỆU KIỂM THỬ PHẦN MỀM DỰA TRÊN KỸ THUẬT KIỂM CHỨNG MÔ HÌNH NGÀNH: CÔNG NGHỆ THÔNG TIN CHUYÊN NGÀNH: CÔNG NGHỆ PHẦN MỀM MÃ SỐ: 60 48 10 LUẬN VĂN THẠC SĨ NGƢỜI HƢỚNG DẪN KHOA HỌC: TS. NGUYỄN TRƢỜNG THẮNG LỜI CẢM ƠN Hà Nội - 2011 3 LỜI CẢM ƠN Trƣớc tiên tôi xin gửi lời cảm ơn chân thành và sâu sắc nhất tới TS. Nguyễn Trƣờng Thắng - Viện công nghệ thông tin - Viện khoa học công nghệ Việt Nam. Thầy đã tận tình chỉ bảo, giúp đỡ và truyền đạt cho tôi rất nhiều kiến thức và kinh nghiệm quý báu trong thời gian qua. Tôi xin cảm ơn các thầy giáo, cô giáo trong khoa Công Nghệ Thông Tin, các thầy các cô luôn giành cho tôi những kiến thức, tình cảm và những lời khuyên quý báu. Cuối cùng tôi xin cảm ơn các bạn bè, đồng nghiệp và nhất là các thành viên trong gia đình đã tạo mọi điều kiện tốt nhất, động viên, cổ vũ tôi trong suốt quá trình học tập và nghiên cứu để hoàn thành tốt luận văn tốt nghiệp này. Tác giả 4 LỜI CAM ĐOAN Tôi xin cam đoan rằng đây là công trình nghiên cứu của tôi trong đó có sự giúp đỡ của thầy hƣớng dẫn. Các nội dung nghiên cứu và kết quả trong đề tài này là hoàn toàn trung thực. Trong luận văn, tôi có tham khảo đến một số tài liệu của một số tác giả đã đƣợc liệt kê tại phần tài liệu tham khảo ở cuối luận văn. Hà Nội, ngày……tháng……năm…… Tác giả Phan Văn Tiến 5 MỤC LỤC MỞ ĐẦU ......................................................................................................................................... 8 CHƢƠNG 1- CƠ SỞ LÝ LUẬN ............................................................................................ 10 1.1 Tổng quan kiểm định phần mềm .................................................................................... 10 1.2 Các nhóm kiểm định phần mềm ..................................................................................... 10 CHƢƠNG 22.1 JAVA PATH FINDER VÀ THỰC THI TƢỢNG TRƢNG ............................ 12 Giới thiệu về JPF............................................................................................................. 12 2.1.1 JPF có thể kiểm tra những chƣơng trình gì? ............................................................ 13 2.1.2 Kiến trúc mức cao của JPF ...................................................................................... 14 2.1.3 Khả năng mở rộng của JPF ...................................................................................... 15 2.1.4 Một số mở rộng của JPF .......................................................................................... 16 2.2 Thực thi tƣợng trƣng để sinh dữ liệu kiểm thử ............................................................... 17 2.2.1 Thực thi tƣợng trƣng là gì? ...................................................................................... 17 2.2.2 Thực thi tƣợng trƣng với JPF .................................................................................. 18 2.2.3 Hƣớng dẫn thực thi tƣợng trƣng với JPF ................................................................. 19 2.2.4 Hạn chế .................................................................................................................... 29 CHƢƠNG 3- MICROSOFT Z3.............................................................................................. 31 3.1 SMT là gì ........................................................................................................................ 31 3.2 Z3 là gì ............................................................................................................................ 31 3.3 Tại sao lại là Z3? ............................................................................................................. 32 3.4 Kiến trúc của Z3.............................................................................................................. 32 3.5 Định dạng đầu vào .......................................................................................................... 33 3.6 Định dạng SMT-LIB ....................................................................................................... 34 3.6.1 3.7 Các chức năng chính của SMT-LIB. ....................................................................... 34 Các quan hệ, phƣơng thức, và hằng số. .......................................................................... 35 3.7.1 Tất cả các phƣơng thức là tuyệt đối ( total) ............................................................. 35 3.7.2 Uninterpreted function và hằng số........................................................................... 36 3.7.3 Phƣơng thức đệ quy ................................................................................................. 36 3.8 Số học.............................................................................................................................. 37 3.8.1 Sô học tuyến tính thực ............................................................................................. 37 3.8.2 Số hoc tuyến tính nguyên ........................................................................................ 37 3.8.3 Trộn giữa số nguyên và số thực. .............................................................................. 38 3.8.4 Số học phi tuyến tính ............................................................................................... 38 6 3.9 Kiểu dữ liệu..................................................................................................................... 39 3.9.1 Kiểu bản ghi............................................................................................................. 39 3.9.2 Kiểu liệt kê ( enumeration) ...................................................................................... 39 3.9.3 Kiểu dữ liệu đệ qui. ................................................................................................. 39 3.10 Ví dụ về Z3 .................................................................................................................. 40 3.11 Một vài ứng dụng của Z3 ............................................................................................ 40 CHƢƠNG 4- TÍCH HỢP Z3 VỚI JPF ................................................................................... 42 4.1 Nghiên cứu đánh giá các giải pháp ................................................................................. 42 4.2 Kiến trúc hệ thống ........................................................................................................... 42 4.3 Chuyển đổi dữ liệu .......................................................................................................... 43 4.4 Thiết kế và cài đặt ........................................................................................................... 47 4.5 Kết quả và đánh giá......................................................................................................... 48 KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN CỦA ĐỀ TÀI ............................................................. 53 TÀI LIỆU THAM KHẢO ............................................................................................................. 54 7 DANH MỤC CÁC HÌNH Hình 2.1: Mô hình hoạt động của JPF ............................................................................... 12 Hình 2.2: Sơ đồ trạng thái trong quá trình kiểm thử .......................................................... 13 Hình 2.3: Kiến trúc mức cao .............................................................................................. 14 Hình 2.4: Mẫu Listener ....................................................................................................... 15 Hình 2.5: Ví dụ về thực thi tƣợng trƣng ............................................................................ 18 Hình 2.6: Đầu ra trên Eclipse cho MyClass1 ..................................................................... 21 Hình 2.7: Đầu ra của MyClass2 trên Eclipse ..................................................................... 22 Hình 2.8: Đầu ra của MyClass2sau khi đã lọc kết quả trên Eclipse................................... 24 Hình 2.9: Đầu ra của MyDriver trên Eclipse ...................................................................... 25 Hình 2. 10: Đầu ra của MyClassFP trên Eclipse ............................................................... 27 Hình 3.1: Kiến trúc của Z3 ................................................................................................. 33 Hình 4.1: Kiến trúc hệ thống .............................................................................................. 43 Hình 4.2: Sơ đồ mức gói..................................................................................................... 47 Hình 4.3: Sơ đồ lớp tổng quát ............................................................................................ 48 Hình 4.4: Kết quả với Choco - số học tuyến tính ............................................................... 49 Hình 4. 5: Kết quả với z3 - số học tuyến tính. .................................................................... 50 Hình 4. 6: Kết quả với Choco – số học phi tuyến tính ....................................................... 51 Hình 4. 7: Kết quả với Z3 – số học phi tuyến tính ............................................................. 52 8 MỞ ĐẦU Trong những năm gần đây, việc phát triển phần mềm ngày càng đƣợc chuyên nghiệp hóa. Các phần mềm đƣợc phát triển ngày càng có quy mô lớn. Yêu cầu đảm bảo chất lƣợng phần mềm là một trong những mục tiêu quan trong nhất, đặc biệt trong một số lĩnh vực nhƣ y khoa, ngân hàng, hàng không… Việc kiểm thử, kiểm chứng phần mềm một cách thủ công chỉ đảm bảo đƣợc phần nào chất lƣợng của phần mềm. Vì vậy rất nhiều các tổ chức, công ty đã nghiên cứu và phát triển các lý thuyết cũng nhƣ công cụ để kiểm chứng, kiểm thử phần mềm một cách tự động. Xuất phát từ nhu cầu thực tế trên, tác giả đã nghiên cứu một số lý thuyết, công cụ trong việc kiểm chứng và kiểm thử phần mềm. Một lý thuyết nền tảng rất quan trọng đó là lý thuyết về tính thỏa đƣợc, viết tắt là SMT (Satisfiability Modulo Theories). Lý thuyết về tính thỏa đƣợc đã đƣợc ứng dụng để giải quyết nhiều bài toán trong công nghệ phần mềm nhƣ:     Kiểm chứng chƣơng trình Khám phá chƣơng trình Mô hình hóa phần mềm Sinh các ca kiểm thử Hiện nay Microsoft Z3 là một công cụ tìm lời giải cho SMT đang đƣợc áp dụng trong nhiều dự án của Microsoft nhƣ: Pex, Spec#, SLAM/SDV, Yogi. Z3 đƣợc đánh già là công cụ tìm lời giải mạnh nhất hiện nay. Tuy nhiên Z3 chỉ đƣợc áp dụng cho các ngôn ngữ của Microsoft. Vì vậy tác giả đặt ra vấn đề: Liệu có thể sử dụng Z3 để kiểm chứng cho các chƣơng trình viết bằng ngôn ngữ khác nhƣ Java? Trong quá trình nghiên cứu về kiểm chứng chƣơng trình tác giả cũng có tìm hiểu về JavaPathFinder (JPF). JPF là một dự án mã nguồn mở đƣợc phát triển trên ngôn ngữ Java. Hiện nay có một mở rộng của JPF trong việc sinh tự động dữ liệu đầu vào để kiểm thử chƣơng trình. Tuy nhiên còn rất nhiều hạn chế, vì vậy tác giả đã nghĩ đến việc làm sao để tích hợp đƣợc Z3 với JPF để có thể sinh tự động dữ liệu kiểm thử chƣơng trình. Nếu việc tích hợp thành công thì sẽ dẫn tới việc giải quyết đƣợc lớp bài toán rộng hơn. Điều này là rất có ý nghĩa đối với thực tế. Mục tiêu đề tài: Mục tiêu của đề tài là nghiên cứu nắm bắt rõ về Z3 và JPF. Sau đó bƣớc đầu tích hợp thành công Z3 và JPF để có thể sinh tự động dữ liệu kiểm thử chƣơng trình Java cho các bài toán mà hiện nay JPF không thể thực hiện đƣợc. (ví dụ: sinh tự động dữ liệu cho số học phi tuyến tính). 9 CẤU TRÚC CỦA LUẬN VĂN Luận văn bao gồm các phần sau: Mở đầu: Giới thiệu về đề tài, tính cấp thiết cũng nhƣ mục tiêu của đề tài Chƣơng 1: Cơ sở lý luận Chƣơng 2: JPF và Thực thi tƣợng trƣng Nội dung: Giới thiêu JPF là gì? Kiến trúc của JPF, cách mở rộng, phát triển trên JPF. Ngoài ra còn một phần rất quan trọng đó là giới thiệu về thực thi tƣợng trƣng để sinh dữ liệu kiểm thử cho chƣơng trình trong JPF. Mở rộng này sẽ cho phép sinh tự động dữ liệu kiểm thử chƣơng trình Java. Chƣơng 3: Microsoft Z3 Nội dung: Giới thiệu về lý thuyết tính thỏa đƣợc SMT, Z3, các lý thuyết đƣợc hỗ trợ trên Z3, các API của Z3 để tích hợp với JPF, các ứng dụng của Z3. Chƣơng 4: Tích hợp JPF với Z3 Nội dung: Nghiên cứu, đánh giá các giải pháp. Sau khi đã có giải pháp tiến hành thiết kế kiến trúc hệ thống, sau đó chi tiết hóa sang mức gói, mức lớp cuối cùng là cài đặt và đánh giá kết quả. Kết luận và hƣớng phát triển của luận văn Trình bày kết quả sau khi nghiên cứu, triển khai và hƣớng phát triển tiếp theo. 10 CHƢƠNG 1- CƠ SỞ LÝ LUẬN 1.1 Tổng quan kiểm định phần mềm Nhƣ chúng ta đã biết, việc kiểm thử phần mềm là một khâu không thể thiếu trong các bƣớc phát triển phần mềm, đặc biệt các phần mềm lớn, nhiều module do nhiều ngƣời phát triển, dễ sinh ra các lỗi tiềm ẩn mà nhà phát triển không thể lƣờng trƣớc. Trong lĩnh vực kiểm định chất lƣợng phần mềm hiện nay trên thế giới, hiện có nhiều kỹ thuật nhƣng tựu chung có thể phân theo ba nhóm chính: Phân tích mã nguồn tĩnh (static code analysis), kiểm thử dữ liệu động (dynamic data testing) và kỹ thuật hình thức dựa trên mô hình (model-based verification). Hai nhóm đầu tập trung vào việc nâng cao chất lƣợng phần mềm tại mức mã nguồn, trong khi nhóm cuối cùng xử lý phần mềm tại mức trừu tƣợng cao hơn – mô hình. 1.2 Các nhóm kiểm định phần mềm Phân tích mã nguồn tĩnh là kỹ thuật phát hiện lỗi chƣơng trình mà không yêu cầu chạy chƣơng trình đó. Không giống nhƣ kỹ thuật kiểm thử dữ liệu động đòi hỏi phải chạy chƣơng trình với dữ liệu đầu vào thật, kỹ thuật phân tích mã nguồn tĩnh chỉ xem xét mã nguồn của chƣơng trình. Kỹ thuật kiểm thử phần mềm dựa trên mô hình: khác với hai nhóm ở trên ở điểm đối tƣợng đƣợc kiểm thử là các mô hình đƣợc trừu tƣợng hóa từ hệ thống đƣợc xem xét. Quá trình trừu tƣợng hóa là việc lƣợc bỏ những chi tiết của hệ thống trong khi chỉ giữ lại những thông tin/khía cạnh quan trọng cần đƣợc lƣu tâm. Kỹ thuật trừu tƣợng hóa đơn giản hóa hệ thống đƣợc xem xét và do đó giảm không gian tìm kiếm và thời gian phân tích chƣơng trình đi nhiều lần so với lúc thực hiện công việc phân tích đó trên mã nguồn. Khi xây dựng xong phần mềm, chúng ta phải sử dụng các testcase (trƣờng hợp kiểm thử) cho việc kiểm thử. Chất lƣợng của việc kiểm thử phụ thuộc rất lớn vào tập hợp các testcase mà chúng ta sử dụng. Hai tiêu chí chính của việc đánh giá chất lƣợng kiểm thử đó là hiệu quả cho chất lƣợng phần mềm đƣợc kiểm thử là độ phủ dòng chảy (control flow coverage) và độ phủ dữ liệu (data coverage). Tiêu chí thứ nhất tập trung vào việc kiểm thử tất cả các điểm điều khiển trên chƣơng trình (ví dụ: các nhánh rẽ khả đạt trong cấu trúc chƣơng trình – reachable control points). Trong khi tiêu chí thứ hai tập trung vào tập dữ liệu kiểm thử ứng với mỗi điểm điều khiển trong cấu trúc chƣơng trình. Bằng kỹ thuật phân tích chƣơng trình dựa trên mô hình sau khi trừu tƣợng hóa mã nguồn của chƣơng trình đƣợc kiểm thử, việc phân tích cấu trúc logic của chƣơng trình và tập dữ liệu ứng với mỗi điểm điều khiển trong chƣơng trình sẽ dễ dàng hơn. Qua đó, quá 11 trình sinh ra tập các testcase sẽ nhanh chóng và chính xác, đảm bảo các tiêu chí control flow và data coverage tốt hơn nhiều so với cách tiếp cận ở mức mã nguồn truyền thống. Hơn nữa, nếu quá trình này đƣợc thực hiện một cách tự động sẽ giảm thiểu nhiều công sức cho các chuyên gia kiểm thử chƣơng trình. Với cách tiếp cận nhƣ vậy, phần mềm có thể đƣợc kiểm thử một cách tự động bằng máy, đem lại kết quả chuẩn hơn, xét đƣợc nhiều trƣờng hợp hơn, đặt biệt là các lỗi logic, tiết kiệm chi phí sản xuất. Đánh giá tập dữ liệu kiểm thử: Ngoại trừ những chƣơng trình đơn giản, sẽ là không thực tế nếu kiểm chứng phần mềm trên tập tất cả dữ liệu đầu vào có thể. Ngay cả khi chỉ tính tổ hợp của các dữ liệu đầu vào hoặc tổ hợp của các hàm, số lƣợng đầu vào và số lƣợng các trạng thái cũng là quá lớn. Khi hệ thống có bộ nhớ lớn, các dữ liệu đầu vào, đầu ra sẽ đƣợc log lại để theo dõi trạng thái. Trong khi không có một công cụ để tạo ra một thiết kế phần mềm chuẩn, hoàn chỉnh và chắc chắn thì việc kiểm thử là một khâu không thể thiếu để có thể đánh giá đƣợc chất lƣợng phần mềm. Vì thế ngƣời ta phải tìm cách chọn đƣợc một tập dữ liệu nhỏ mà có thể kiểm thử mang lại đƣợc độ tin cậy cao với mỗi hệ thống. Độ phủ hay mức độ đầy đủ bằng trực quan đánh giá đƣợc phạm vi hay mức độ kiểm thử. Nếu kiểm thử không đầy đủ đƣợc hết mọi khía cạnh của phần mềm đồng nghĩa với việc chúng ta bỏ sót nhiều lỗi. Các tấn suất của các trƣờng hợp cũng không giống nhau. Khái niệm ca kiểm thử đơn giản là kiểm chứng các trạng thái đƣa ra thể hiện cho hoạt động của hệ thống. Chúng ta có thể tạo ra ca kiểm thử đề đạt đƣợc trạng thái có thể bằng cách đƣa vào các biến đặc biệt, trạng thái để điều khiển hệ thống. 12 CHƢƠNG 2- JAVA PATH FINDER VÀ THỰC THI TƯỢNG TRƯNG Trong chƣơng này sẽ bao gồm hai phần chính. Phần 1 giới thiệu về JPF, một dự án mã nguồn mở đƣợc viết bằng ngôn ngữ java để kiểm chứng mô hình. Phần 2 giới thiệu một mở rộng của JPF đó là thực thi tƣợng trƣng trong việc sinh tự động dữ liệu để kiểm thử chƣơng trình Java. 2.1 Giới thiệu về JPF JPF là một bộ kiểm tra mô hình phần mềm trạng thái tƣờng minh cho Java [5]. Hiểu một cách cơ bản JPF là một máy ảo thực thi chƣơng trình Java không chỉ một lần (giống nhƣ các máy ảo thông thƣờng), mà thực thi trong tất cả các nhánh, các đƣờng đi có thể. JPF sẽ kiểm tra các vi phạm thuộc tính nhƣ khóa chết hoặc các ngoại lệ không thể bắt đƣợc xuyên xuốt các đƣờng thực thi tiềm năng. Hình 2-1 mô tả mô hình hoạt động của JPF. Hình 2.1: Mô hình hoạt động của JPF Về lý thuyết điều này là rất khả thi, tuy nhiên với việc tăng kích cỡ của ứng dụng, phần mềm kiểm chứng mô hình phải đối mặt với nhiều thách thức. JPF cũng không là ngoại lệ. Câu trả lời của chúng ta đó là tăng sự linh hoạt của JPF để thích nghi với một ứng dụng cụ thể. Chúng ta có thể coi JPF nhƣ là một Framework và từ đó phát triển mở rộng để có thể giải quyết đƣợc bài toán cụ thể mà chúng ta muốn. 13 2.1.1 JPF có thể kiểm tra những chƣơng trình gì? JPF có thể kiểm tra tất cả các chƣơng trình Java. JPF có thể tìm ra các khóa chết hoặc ngoại lệ. Ngoài ra chúng ta có thể tự phát triển mở rộng để kiểm tra các thuộc tính khác. Để hiểu rõ hơn về JPF chúng ta có thể xét ví dụ sau: Tạo một lớp là Rand.java nhƣ bên dƣới, sau đó chúng ta sẽ dùng JPF để kiểm tra xem có lỗi không. import java.util.Random; public class Rand { public static void main (String[] args) { Random random = new Random(42); int a = random.nextInt(2); System.out.println("a=" + a); // (1) // (2) int b = random.nextInt(3); // (3) System.out.println(" b=" + b); int c = a/(b+a -2); System.out.println(" // (4) c=" + c); } } Hình 2.2: Sơ đồ trạng thái trong quá trình kiểm thử 14 Hoạt động của lớp trên đó là khởi tạo 2 biến a và b một cách ngẫu nhiên trong các khoang tƣơng ứng la [0,2] và [0,3]. Sau đó có một biến c có giá trị đƣợc xác định bằng công thức c = a/(b+a-2). Nếu ta chạy chƣơng trình java này thông thƣờng thì có thể thấy kết quả là: a = 1, b =0, và c = -1. Nhƣ vậy chƣơng trình là không có lỗi. Tuy nhiên nếu ta sử dụng JPF để kiểm tra chƣơng trình trên thì sẽ thấy nhƣ hình vẽ bên dƣới: Nhìn hình vẽ trên ta có thể thấy nếu chạy chƣơng trình java bình thƣờng thì ta chỉ có thể nhân đƣợc 1 trong 6 kết quả trên, do vậy khả năng lớn là không phát hiện đƣợc ra lỗi ( Đƣờng bôi đỏ là ví dụ). Tuy nhiên JPF sẽ tìm ra tất cả các đƣờng đi của chƣơng trình sau đó kiểm tra chúng. Ta sẽ thấy có 2 trƣờng hợp lỗi gây ra bởi phép chia cho 0. 2.1.2 Kiến trúc mức cao của JPF Hình 2.3: Kiến trúc mức cao 15 Hình 2-3 biểu diễn sơ đồ kiến trúc mức cao của JPF. JPF đƣợc thiết kế thành 2 thành phần chính đó là: JVM, và Search. JVM là một bộ sinh trạng thái cụ thể Java. Bằng việc thực hiện các chỉ thị Java bytecode. Search chịu trách nhiệm lựa chọn trạng thái mà JVM nên xử lý, hoặc hƣớng JVM sinh trạng thái tiếp theo, hoặc yêu cầu JVM quay trở lại một trạng thái trƣớc đó. Nói một các khác Search có thể coi nhƣ các driver cho các đối tƣợng JVM. Search cũng cấu hình và đánh giá các đối tƣợng thuộc tính. Các cài đặt chính của Search bao gồm tìm kiếm theo độ sâu (DFSearch) và HeuristicSearch. Một cài đặt Search sẽ cung cấp một phƣơng thức Search đơn giản bao gồm một vòng lặp chính sẽ duyệt qua tất cả các không gian trạng thái liên quan cho đến khi nó duyệt xong tất cả hoặc tìm ra một vi phạm thuộc tính (property violation). 2.1.3 Khả năng mở rộng của JPF Hình 2.4: Mẫu Listener 16 JPF có thể đƣợc coi nhƣ là một Framework mà tại đó bất kỳ nhà phát triển nào đều có thể mở rộng để phục vụ cho một mục đích cụ thể. JPF cung cấp một cơ chế mở rộng để cho phép thêm vào các chức năng mới mà không phải thay đổi trực tiếp cài đặt của Search hoặc VM. Yêu cầu về khả năng mở rộng có thể đạt đƣợc bằng cách sử dụng mẫu Listerner trên hình 2-4. Các thể hiện sẽ tự đăng ký hoặc đăng ký với đối tƣợng Search/VM, nhận thông báo khi một đối tƣợng (Subject) tƣơng ứng thực thi một hoạt động nhất định, và sau đó có thể tƣơng tác với đối tƣợng để truy vấn các thông tin bổ sung hoặc điểu khiển hành vi của đối tƣợng. Việc thay đổi các khía cạnh của đổi tƣợng đƣợc ánh xạ vào các phƣơng thức Observer riêng biệt, các thể hiện của đối tƣợng sẽ đƣợc truyền đi nhƣ tham số. Đối tƣợng Subject sẽ theo dõi các listener đã đăng ký theo Multicaster. Có 3 mức khác nhau để có thể lấy đƣợc thông tin của đối tƣợng Subject bằng cách cài đặt listener.  Generic – listener cƣ trú bên ngoài các gói JPF và chỉ sử dụng các thông tin đã đƣợc công khai (public) theo gov.nasa.jpf.Search / VM.  Search-specific – listener cƣ trú bên ngoài gói JPF nhƣng sẽ đƣa các tham số thông báo của đối tƣợng Subject vào các cài đặt cụ thể (ví dụ: gov.nasa.jpf.search.heuristic.BFSHeuristic), và sử dụng các API của nó để lấy các thông tin cài đặt cụ thể.  Internal - listener cƣ trú trong các gói cài đặt Subject riêng biêt và truy cập các thông tin riêng của gói ( private) . 2.1.4 Một số mở rộng của JPF Với kiến trúc mở rộng linh hoạt, hiện nay đã có một số mở rộng đƣợc phát triển cho JPF UI - User Interface Model Checking Đây là mở rộng cho việc kiểm tra mô hình một lớp đặc biệt của các ứng dụng Java đó là các chƣơng trình Swing và AWT. Mở rộng này đƣợc cài đăt nhƣ một nhƣ viện chuẩn đƣợc mô hình hóa MJI (MJI Là viết tắt của: Model Java Interface) nhằm thay thế các chức năng của Swing và AWT để mà các ứng dụng giao diện sử dụng chuẩn của Java có thể đƣợc kiểm thử với các đầu vào khác nhau. symbc - Symbolic Test Data Generation Mở rộng này sử dụng BytecodeFactory để ghi đè lõi (core) JPF bytecodes nhằm sinh ra các ca kiểm thử riêng biệt. Nói tóm lại nó hoạt động bằng cách sử dụng các thuộc 17 tính/ trƣờng của JPF để thu thập các điều kiện đƣờng đi PC, sau đó đƣợc đƣa các PC vào một hệ thống tìm lời giải theo đinh dạng của hệ thống đó để đƣa ra dữ liệu kiểm thử. Mở rộng này sẽ đƣợc trình bày chi tiết hơn ở phần 2.2. cv - Compositional Verification Framework Mở rộng này là một thuật toán học máy đƣợc sử dụng cho các lập luận thừa nhận/ đảm bảo, nhằm mục đích phân chia hệ thống thành các thành phần con và sau đó kiểm chứng từng thành phần đó một cách riêng rẽ. Mục đích chính của mở rộng này là cải tiến khả năng của JPF, nó có thể đƣợc sử dụng để sinh ra môi trƣờng giả định cho kiểm chứng mô hình UML, để xác định các trình tự sự kiện đúng. numeric - Numeric Property Verification Mở rộng này đƣợc sử dụng để kiểm chứng các thuộc tính của số học. Ban đầu mở rộng đƣợc sử dụng nhƣ nhƣ một tập các lớp chỉ thị số học để phát hiện tràn bộ nhớ, sau đó đƣợc mở rộng để kiểm chứng việc truyền giá trị không chính xác, so sánh dấu phẩy động chính xác (floating point comparison). statechart - UML State Chart Model Checking Mục đích của mở rông này là kiểm tra lƣợc đồ chuyển trạng thái UML. Trong mở rộng này mỗi một biểu đồ chuyển trạng thái sẽ đƣợc biểu diễn tƣơng ứng với một lớp Java (hoặc nhiều lớp). Sau đó quá trình kiểm tra sẽ là kiểm tra các lớp java đó. 2.2 Thực thi tượng trưng để sinh dữ liệu kiểm thử 2.2.1 Thực thi tƣợng trƣng là gì? Đổi giá trị giữa 2 biến Đƣờng đi cụ thể 18 Hình 2.5: Ví dụ về thực thi tƣợng trƣng Kỹ thuật thực thi tƣợng trƣng là kỹ thuật thực thi chƣơng trình bằng cách sử dụng các giá trị tƣợng trƣng, không phải sử dụng các giá trị cụ thể [2]. Để hiểu rõ thực thi tƣợng trƣng là gì, xét ví dụ chuyển đổi giứa 2 biến x và y: Ở ví dụ trên, nếu trong trƣờng hợp thực thi tƣợng trƣng, giá trị của x và y là các giá trị tƣợng trƣng X, Y chứ không phải là các giá trị cụ thế. Kết quả của quá trình thực thi tƣợng trƣng sẽ duyệt hết các dƣờng đi có thể có của chƣơng trình, và cho ra điều kiên đƣờng đi. Ƣu điểm của phƣơng pháp này là ta có thể thực thi tại bất kỳ điểm nào trong chƣơng trình và có thể trộn giữa đầu vào tƣợng trƣng với đầu vào cụ thể. Phƣơng pháp này sẽ cho ta các điều kiện đƣờng đi của chƣơng trình, và với việc sử dụng các công cụ tìm lời giải cho các điều kiện đƣờng đi (coi mỗi điều kiện đƣờng đi là một biểu thức) sẽ sinh ra dữ liệu kiểm thử cho chƣơng trình. Tuy nhiên phƣơng pháp này cũng có giới hạn đó là có thể bùng nổ các đƣờng đi trong việc thực thi tƣợng trƣng. 2.2.2 Thực thi tƣợng trƣng với JPF Thực thi tƣợng trƣng là một mở rộng của JPF. Mở rộng này của JPF sẽ thực thi tƣợng trƣng các chƣơng trình java. Một trong những ứng dụng chính của mở rộng này, đó là tự động sinh dữ liệu kiểm thử bao phủ toàn bộ chƣơng trình của mã nguồn. 19 Mở rộng này phối hợp thực thi tƣợng trƣng với kiểm chứng mô hình và các ràng buộc giải quyết để sinh dữ liệu kiểm thử. Trong công cụ này, các chƣơng trình đƣợc thực thi trên đầu vào tƣợng trƣng. Các giá trị của các biến đƣợc biểu diễn nhƣ và các biểu thức số và ràng buộc, chúng đƣợc sinh từ việc phân tích cấu trúc mã nguồn. Những ràng buộc sau đó đƣợc giải quyết để sinh ra các dữ liệu kiểm thử để đảm bảo đạt đƣợc phần mã nguồn đó. Tại thời điểm hiện tại JPF hỗ trợ các tham số nguyên và thực. Tuy nhiên vẫn còn một số trƣờng hợp cần giải quyết cho số thực. Hiện tại mở rộng này chỉ hỗ trợ các ràng buộc tuyến tính (số học tuyến tính), sô học phi tuyến là chƣa đƣợc hỗ trợ. Thông tin tƣợng trƣng đƣơc truyền theo các thuộc tính kết hợp với các biến và các toán tử. Thực thi tƣợng trƣng có thể bắt đầu từ bất kỳ điểm nào trong chƣơng trình và nó có thể thực thi tƣợng trƣng riêng biệt với nhau. 2.2.3 Hƣớng dẫn thực thi tƣợng trƣng với JPF Để thực hiên một phƣơng thức một cách tƣợng trƣng, ngƣời sử dụng cần đặc tả tham số phƣơng thức nào là tƣợng trƣng/cụ thể. Các tham biến toàn cục cũng có thể đƣợc đặc tả để thực thi tƣợng trƣng, theo các sự chú thích đặc biệt. Đây là một ví dụ để chạy một thực thi tƣợng trung. Ví dụ này cho phép thực thi tƣợng trƣng của phƣơng thức test trong lớp chính. +vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory +jpf.listener=gov.nasa.jpf.symbc.SymbolicListener +symbolic.method=test(sym#con) +search.multiple_errors=true +jpf.report.console.finished= ExSymExe 2.2.3.1 Một ví dụ đơn giản Sau đây là một ví dụ rất đơn giản của việc thực thi tƣợng trƣng với JPF. Chúng ta có thể sự dụng Eclipse hoặc thông qua giao diện dòng lệnh. Giả sự ta có phƣơng thức sau trong lớp bạn muốn sinh kiểm thử: public class MyClass1 { public int myMethod(int x, int y) { int z = x + y; if (z > 0) { z = 1; } else { z = z - x; 20 } z = 2 * z; return z; } } Chúng ta sẽ cần tạo một driver để gọi myMetho(int,int). Driver có thể là một lớp khác hoặc phƣơng thức main() của chính lớp này. Trong trƣờng hợp này ta sẽ viết driver trong phƣơng thức main() của lớp MyClass1. Trong ví dụ đơn giản này, driver chỉ cần gọi myMethod() với số và kiểu tham số đúng sau đó in ra điều kiện đƣờng đi (Path condition – PC). Điều lƣu ý là tham số chính xác không phải là vấn đề, vì chúng ta sẽ thực thi myMethod() một cách tƣợng trƣng, tất cả các giá trị cụ thể sẽ đƣợc thay thế bằng giá trị tƣợng trƣng. Chúng ta có thể xem các ca kiểm thử (test case) bằng cách in ra điều kiện đƣờng đi. Việc này thực hiện đƣợc bằng cách gọi phƣơng thức: gov.nasa.jpf.symbc.Debug.printPC(). Sau đây là mã nguồn đầy đủ: public class MyClass1 { public int myMethod(int x, int y) { int z = x + y; if (z > 0) { z = 1; } else { z = z - x; } z = 2 * z; return z; } // driver để kiểm thử public static void main(String[] args) { MyClass1 mc = new MyClass1(); int x = mc.myMethod(1, 2); Debug.printPC("MyClass1.myMethod Path Condition: "); } } 21 Khi đó nếu chạy bằng Eclipse sẽ cho kết quả sau: Hình 2.6: Đầu ra trên Eclipse cho MyClass1 Nhìn vào kết quả ở trên các PC sẽ chỉ ra các ca kiểm thử là Ca kiểm thử 1: y = -9999999, x = 10000000 Ca kiểm thử 2: y = -10000000, x = 10000000 Ca kiểm thử 1 tƣơng ứng với z > 0 của câu lệnh if của phƣơng thức myMethod. Ca kiểm thử 2 tƣơng ứng với nhánh z≤0. 2.2.3.2 Lọc các trƣờng hợp kiểm thử Chúng ta thay đổi MyClass1 thành MyClass 2 nhƣ sau. public class MyClass2 { private int myMethod2(int x, int y) { int z = x + y; if (z > 0) { z = 1; } if (x < 5) { z = -z; } return z;
- Xem thêm -