chương 1 và 2, trong phần này tác giả sẽ đánh giá và đưa ra các giải pháp để mở rộng JPF với Z3. Sau khi đã có giải pháp sẽ 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ả. Các nghiên cứu liên quan Phần này tác giả sẽ trình bày một số nghiên cứu khác liên quan đến luận văn, đó là các công cụ Pex, AgitarOne, Cute trong việc tự động kiểm thử chương trình. 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, những hạn chế và hướng phát triển tiếp theo.
TIEU LUAN MOI download : skknchat@gmail.com 3 CHƢƠNG 1- JPF VÀ THỰC THI TƢỢNG TRƢNG Trong chương này sẽ bao gồm 2 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 [6]. 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 1-1 mô tả mô hình hoạt động của JPF. Hình 1-1: Mô hình hoạt động của JPF [6] 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 TIEU LUAN MOI download : skknchat@gmail.com 4 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.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 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. 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 1-2: TIEU LUAN MOI download : skknchat@gmail.com 5 Hình 1-2: Sơ đồ trạng thái trong quá trình kiểm thử 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 đậm 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 1-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. TIEU LUAN MOI download : skknchat@gmail.com 6 Hình 1-3: Kiến trúc mức cao [6] 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 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ơ TIEU LUAN MOI download : skknchat@gmail.com 7 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.
Hình 1-4: Mẫu Listener [6] 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 1-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. 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.BFSHeuristic), và sử dụng các API của nó để lấy các thông tin cài đặt cụ thể. TIEU LUAN MOI download : skknchat@gmail.com 8 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) .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 thư 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 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 định 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 1. 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 đó.
TIEU LUAN MOI download : skknchat@gmail.2 Thực thi tượng trưng để sinh dữ liệu kiểm thử 1.1 Thực thi tƣợng trƣng là gì? 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ể [8, 16]. Để 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: Đổi giá trị giữa 2 biến Đường đi cụ thể Việc thực thi cụ thể (sử dụng các giá trị cụ thể của 2 biến x, y) được mô tả như trên, khi đó với mỗi giá trị cụ thể của x và y ta sẽ có đường đi cụ thể. Hình 1- 5 sẽ biểu diễn quá trình thực thi tượng trưng TIEU LUAN MOI download : skknchat@gmail.com 10 Hình 1-5: Ví dụ về thực thi tƣợng trƣng Ở 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 đường đi có thể có của chương trình, và cho ra điều kiện đường đi (PC).
PC là một biểu thức boolean với các biến là các giá trị tượng trưng đầu vào, đây chính là các ràng buộc để đầu vào phải thỏa mãn theo một nhánh cụ thể [15, 16]. Ở ví dụ trên ta sẽ có 2 PC đó là: X > Y Y ≤ X và X > Y Y > X. Ư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.