Chương 3: Sinh ca kiểm thử tham số hóa với JPF

Chương 3: Sinh ca kiểm thử tham số hóa với JPF

3.1. Kiến trúc của JPF

Có thể sử dụng JPF một cách linh hoạt dưới dạng giao diện dòng lệnh hoặc tích hợp vào trong các môi trường phát triển ứng dụng Java như Netbean, Eclipse. JPF là một ứng dụng Java mã nguồn mở cho phép ta cấu hình để sử dụng nó theo các cách khác nhau và mở rộng nó.

Máy ảo JPF được cài đặt tuân theo các đặc tả về máy ảo Java nhưng không giống như các máy ảo Java chuẩn khác máy ảo JPF có khả năng lưu trữ trạng thái (state storing), ghi nhớ trạng thái (state matching) và quay lui trong quá trình thực thi chương trình.

Quay lui (backtracking) có nghĩa là JPF có thể phục hồi lại trạng thái thực thi lúc trước để xem có còn những sự lựa chọn thực thi khác.

Ghi nhớ trạng thái (state matching) có nghĩa là đánh dấu các trạng thái đã thám hiểm mà không còn cần thiết nữa giúp JPF tránh được những sự thực thi không cần thiết. Trạng thái thực thi của một chương trình bao gồm heap và ngăn xếp tiến trình. Trong khi thực thi JPF kiểm tra mọi trạng thái mới có phải là các trạng thái đã được ghi nhớ. Nếu các trạng thái đã được ghi nhớ JPF sẽ không tiếp tục đi theo đường đi thực thi hiện hành và quay lui tới trạng thái gần nhất mà chưa được thám hiểm.

Với những chương trình lớn và phức tạp thì không gian trạng thái trong quá trình thực thi chương trình là rất lớn. Việc lưu trữ và thám hiểm tất cả các trạng thái không phải lúc nào cũng đạt được. JPF sử dụng các kỹ thuật khác nhau để giải quyết vấn đề này đó là các chiến lược tìm kiếm, các kỹ thuật để giảm thiểu số trạng thái chương trình và việc lưu trữ các trạng thái. Có các chiến lược tìm kiếm khác nhau được sử dụng như tìm kiếm theo chiều sâu (Depth-First Search), theo chiều rộng (Breadth-First Search), tìm kiếm kinh nghiệm.

Hình 12: Kiến trúc JPF

+ JPF được thiết kế gồm hai thành phần chính đó là đối tượng máy ảo (VM) và đối tượng tìm kiếm (Search Object).

VM là một bộ sinh trạng thái bằng việc thực thi các chỉ thị bytecode. Đối tượng VM có các phương thức chính đó là :

• 
  forward():sinh ra một trạng thái mới
  
• 
  backtrack():phục hồi lại trạng thái ngay trước đó
  
• 
  restore(): phục hồi lại một trạng thái tùy ý
  

+ Các tính năng mở rộng:

Search Listener và VM Listener: Chúng được sử dụng để quan sát việc thực thi bên trong JPF mà không cần cài đặt lại các lớp của VM và Search.

Search Listener được đăng ký tới các sự kiện của đối tượng Search:

public interface SearchListener {

  // got the next state

  void stateBacktracked (Search search);

// JPF encountered a property violation

  void propertyViolated (Search search);

//a search loop was started

// the search loop was finished

}

và VM Listener được đặng ký tới các sự kiện của đối tượng VM trong quá trình thực thi một chương trình. VMListener được sử dụng để quản lý việc thực thi các chỉ thị bytecode:

   void instructionExecuted (JVM vm);

  void threadStarted (JVM vm);

 void threadTerminated (JVM vm);

   void classLoaded (JVM vm);

   void objectCreated (JVM vm);

   void objectReleased (JVM vm);

   void gcBegin (JVM vm);

   void gcEnd (JVM vm);

   void exceptionThrown (JVM vm);

   void nextChoice (JVM vm);

...

}

Model Java Interface (MJI): Nếu JNI là giao diện cho phép các ứng dụng Java chạy trong máy ảo Java của môi trường thực thi giao tiếp với các thư viện và ứng dụng viết trong các ngôn ngữ khác như C, C++, Assembly của hệ điều hành bên dưới thì MJI là giao diện cho phép các ứng dụng Java chạy trong máy ảo JPF giao tiếp với máy ảo của môi trường thực thi bên dưới. Nói cách khác, MJI cho phép chuyển hướng việc thực thi một chương trình Java bên trong máy ảo JPF sang máy ảo của môi trường thực thi bên dưới (host JVM) mà JPF đang được chạy trên đó.

Hình 13: Bộ sinh lựa chọn trong JPF

Bộ tạo chỉ thị (Bytecode Factory): Trong JPF có các lớp biểu thị cho tất cả các chỉ thị bytecode được cài đặt để thông dịch các chỉ thị bytecode đó sử dụng thư viện bcel[30]. InstructionFactory là giao diện cho phép tạo các đối tượng Instruction bao gói việc thực thi các chỉ thị bytecode. Khi một chỉ thị bytecode trong tập tin .class được tải vào trong máy ảo JPF để xử lý thì một đối tượng Instruction sẽ được tạo ra. Nói cách khác, khi một tập tin .class được đọc một mảng các đối tượng Instruction sẽ được tạo ra. Các đối tượng Instruction có phương thức execute() để thực hiện việc thực thi chỉ thị bytecode tương ứng. Chế độ thực thi mặc định trong JPF là chế độ thực thi cụ thể. Với giao diện InstructionFactory, ta có khả năng ghi đè các lớp chỉ thị mà cài đặt việc thông dịch các chỉ thị bytecode để thay đổi chế độ thực thi trong JPF.