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. | TẠ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 ngang 1. 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ụng cô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ại cho 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ương phá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ương phá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ỹ
