Một kỹ thuật kiểm chứng mô hình với Java path finder

Bài viết trình bày một kỹ thuật kiểm chứng mô hình với java path finder (JPF). Đây là một kỹ thuật kiểm chứng hỗ trợ các miền dữ liệu trừu tượng nhằm co lại miền dữ liệu lớn trong chương trình java, miền dữ liệu hữu hạn làm cho việc kiểm chứng trở nên dễ dàng hơn.
Nội dung trích xuất từ tài liệu:
Một kỹ thuật kiểm chứng mô hình với Java path finderTẠP CHÍ KHOA HỌC − SỐ 14/2017 5 MỘT KỸ KỸ THUẬ THUẬT KIỂ KIỂM CHỨ CHỨNG MÔ HÌNH VỚI JAVA PATH FINDER Nguyễn Đức Giang1(1), Lưu Thị Bích Hương2, Trần Bá Hùng1, Trần Thị Thu Ngân3 1 Viện Công nghệ Thông tin, Viện Hàn lâm Khoa học và Công nghệ Việt Nam 2 Trường Đại học Sư phạm Hà Nội 2 3 Trường Đại học Ngoại thương Tóm tắtắt: Trong bài báo này, chúng tôi trình bày một kỹ thuật kiểm chứng mô hình với java path finder (JPF). Đây là một kỹ thuật kiểm chứng hỗ trợ các miền dữ liệu trừu tượng nhằm co lại miền dữ liệu lớn trong chương trình java, miền dữ liệu hữu hạn làm cho việc kiểm chứng trở nên dễ dàng hơn. Kỹ thuật này sử dụng dữ liệu trừu tượng để tính toán một cách xấp xỉ của chương trình ban đầu, nếu một tính chất an toàn là đúng trong miền trừu tượng thì cũng đúng trong chương trình ban đầu. Bài báo cũng đưa ra cách tiếp cận tăng cường JPF với một trình thông dịch trừu tượng và cơ chế phù hợp với trạng thái trừu tượng, từ đó, người dùng có thể chọn các trừu tượng để sử dụng cho một ứng dụng cụ thể. Để cụ thể hóa kỹ thuật này, cần phân tích các chương trình đa luồng trong java, nơi mà vết thời gian không thể tiết kiệm bộ nhớ bằng việc sử dụng JPF. Từ khóa: khóa Kiểm chứng mô hình, tìm kiếm đường dẫn Java, diễn giải trừu tượng, không gian trạng thái ngang1. GIỚI THIỆU Trong ngành công nghệ phần mềm, ngoài việc cung cấp các ý tưởng hay ứng dụngcông nghệ thông tin (CNTT) trong đời sống kinh tế xã hội hiện đại thì việc kiểm chứng vàphân tích một cách kỹ lưỡng nhằm đảm bảo chất lượng cũng như giảm thiểu rủi ro thiệt hạicho sản phẩm ứng dụng trước khi đưa ra ngoài thị trường là cần thiết. Hiện nay các phươngpháp kiểm chứng hình thức được áp dụng khá phổ biến. Kỹ thuật đặc tả trạng thái không gian như việc kiểm tra mô hình là phương pháp phổbiến để kiểm chứng mô hình và tìm lỗi chương trình. Kiểm tra mô hình là một phươngpháp phân tích rất hữu ích, đặc biệt cho việc phân tích các chương trình đa luồng. Công cụsử dụng để kiểm tra các tính chất vi phạm (lỗi) của chương trình đa luồng với kỹ thuậtkiểm chứng mô hình là java path finder (JPF), với mục tiêu là bytecode java.(1) Nhận bài ngày 11.02.2017; chỉnh sửa, gửi phản biện và duyệt đăng ngày 20.3.2017 Liên hệ tác giả: Nguyễn Đức Giang; Email: ndgiang@ioit.ac.vn6 TRƯỜNG ĐẠI HỌC THỦ ĐÔ H NỘI JPF là một máy ảo Java đặc biệt có hỗ trợ quay lui, kết hợp trạng thái, không bất địnhtrong cả dữ liệu và các quyết định lập kế hoạch. JPF xây dựng không gian trạng tháichương trình on-the-fly trong việc thực hiện các chương trình trong máy ảo. Sự chuyểntiếp trong không gian trạng thái là một chuỗi các hướng dẫn bytecode thực hiện bởi mộtchủ đề duy nhất, nơi mà các đường dẫn đầu tiên trong chuỗi đại diện cho một sự lựa chọnkhông xác định tương ứng với một quy tắc. Tại mỗi ranh giới chuyển tiếp, JPF ghi nhớ mỗitrạng thái JVM hiện tại (chương trình trạng thái) trong một hình thức tuần tự cho các mụcđích của quay lui và trạng thái tương ứng. Các trạng thái JVM hoàn chỉnh bao gồm tất cảcác đối tượng heap, ngăn xếp của tất cả các chủ đề và tất cả dữ liệu tĩnh. Những thay đổicủa trạng thái JVM được thực hiện bên trong thông dịch các lệnh bytecode, đây là mộtphần của JPF. JPF chứa một thông dịch cụ thể, trong đó mô hình chung cho tất cả các lệnh bytecodeJava và lưu giữ giá trị cụ thể của các biến chương trình. JPF thực thi cụ thể chỉ thị trongdòng chảy không gian trạng thái. Hạn chế chính của JPF đối với tính hữu dụng thực tế lànếu thực hiện một dòng chảy đầy đủ thì rất dễ bị nổ trạng thái. Mặc dù JPF hỗ trợ nhiều tốiưu, bao gồm giảm thứ tự từng phần và giảm đối xứng, việc kiểm tra tất cả các chủ đề vớiviệc thực hiện cụ thể tốn nhiều thời gian và đòi hỏi nhiều bộ nhớ chương trình. Một giảipháp có thể sử dụng dữ liệu trừu tượng để làm giảm các miền lớn của các biến chươngtrình, lựa chọn miền nhỏ hơn và việc kiểm chứng chương trình thuận lợi thông qua dòngchảy không gian trạng thái khả thi hơn. Hãy xem xét ví dụ trong Hình 6. Đây là một biến thể đơn giản cổ điển - vấn đề ngườidùng với một đối tượng chia sẻ của lớp dữ liệu. Các tính chất an toàn quan tâm ở đây là sựvắng mặt của các kiểu dữ liệu. JPF sẽ đưa ra những hành vi chương trình cho tất cả các giátrị có thể có của các biến còn lại, nghĩa là tất cả các giá trị số nguyên từ 0 đến 1000000, vàkhông gian trạng thái chương trình sẽ do đó sẽ rất lớn. Người ta có thể sử dụng các dấuhiệu trừu tượng trên các biến còn lại để thay thế miền lớn của kiểu dữ liệu int trong Javavới một nhỏ miền hữu hạn {POS, ZERO, NEG}, mà chỉ mã hóa các dấu hiệu của biến cònlại, trong khi trừu tượng đi những giá trị thực tế. Tất cả các trạng thái chương trình có sựkhác biệt về giá trị của các biến sẽ được thu gọn để ba trạng thái khác nhau với các giá trịtrừu tượng tương ứng. Do đó, không gian trạng thái đưa ra bởi JPF với một khái niệm trừutượng như vậy sẽ nhỏ hơn nhiều, làm giảm thời gian cần thiết để xác minh các tính chất antoàn nhất định, trong khi tất cả các hành vi của chương trình sẽ được phân tích. Trong các phần tiếp theo của bài báo, chúng tôi trình bày nền tảng của JPF. Phần bacủa bài báo là kết quả sử dụng truy vết thực thi và kiểm chứng mô hình trong JAVA. Phầncuối cùng là kết luận của bài báo.TẠP CHÍ KHOA HỌC − SỐ 14/2017 72. NỀ ...