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. TIEU LUAN MOI download : skknchat@gmail.com 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.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á TIEU LUAN MOI download : skknchat@gmail.com 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. TIEU LUAN MOI download : skknchat@gmail.com 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.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.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. TIEU LUAN MOI download : skknchat@gmail.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.Random; public class Rand { public static void main (String[] args) { Random random = new Random(42); // (1) int a = random.println("a=" + a); int b = random.2: Sơ đồ trạng thái trong quá trình kiểm thử TIEU LUAN MOI download : skknchat@gmail.com 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 Kiến trúc mức cao của JPF Hình 2.3: Kiến trúc mức cao TIEU LUAN MOI download : skknchat@gmail.com 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).3 Khả năng mở rộng của JPF Hình 2.4: Mẫu Listener TIEU LUAN MOI download : skknchat@gmail.com 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.