I. Giới thiệu
Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là một vấn đề quan trọng nhằm đảm bảo tính đúng đắn, giảm tỉ lệ lỗi, tìm khiếm khuyết của phần mềm trước khi đưa vào sử dụng. Vấn đề này không chỉ là yếu tố quyết định thành công của các công ty phần mềm mà còn góp phần quan trọng tới sự thành công của khách hàng. Đặc biệt, trong các phần mềm nhúng/điều khiển, lỗi trong phần mềm có thể gây ra thiệt hại nghiêm trọng. Một trong những phương pháp nhằm chứng minh tính đúng đắn của chương trình là kiểm chứng mô hình. Tuy nhiên, một trong những hạn chế lớn nhất của phương pháp này là vấn đề "bùng nổ không gian trạng thái". Phương pháp kiểm chứng giả định-đảm bảo được xem là giải pháp tiềm năng để giải quyết vấn đề này cho các hệ thống dựa trên thành phần. AGTool là một công cụ hỗ trợ kiểm chứng phần mềm, cho phép người dùng sinh ra một giả thiết kiểm chứng để kiểm tra một thành phần và cả hệ thống có thỏa mãn một thuộc tính hay không.
II. Kiến thức cơ bản
Chương này trình bày các khái niệm cơ bản về Labeled Transition System (LTS) và các phương pháp biểu diễn LTS. LTS được sử dụng để đặc tả hành vi của các thành phần và thuộc tính cần kiểm chứng. Phương pháp liệt kê (LF) và FSP (Finite State Processes) là hai phương pháp chính để biểu diễn LTS. FSP được sử dụng để xây dựng mô hình các tiến trình, có thể được phân tích và kiểm tra bởi công cụ LTSA. Sự tương đương giữa hai phương pháp này cho phép chuyển đổi qua lại giữa các dạng biểu diễn, từ đó tạo điều kiện thuận lợi cho việc kiểm chứng phần mềm.
2.1 Labeled Transition System LTS
LTS là một mô hình toán học dùng để mô tả hành vi của hệ thống. Một LTS được định nghĩa bởi một bộ bốn bao gồm tập trạng thái, bảng chữ cái hành động, trạng thái khởi đầu và hàm chuyển trạng thái. LTS cho phép mô tả các hành động có thể xảy ra trong hệ thống và cách mà hệ thống chuyển từ trạng thái này sang trạng thái khác. Việc sử dụng LTS trong kiểm chứng phần mềm giúp phát hiện lỗi và đảm bảo tính đúng đắn của hệ thống.
2.2 Các phương pháp biểu diễn LTS
Có hai phương pháp chính để biểu diễn LTS: phương pháp liệt kê (LF) và FSP. Phương pháp liệt kê mô tả LTS bằng cách liệt kê tất cả các hàm chuyển trạng thái cùng với trạng thái khởi tạo. Trong khi đó, FSP cung cấp một cách tiếp cận tổng quát hơn để mô hình hóa các tiến trình. Mặc dù FSP có thể khó hiểu hơn, nhưng nó cho phép xây dựng các mô hình phức tạp hơn và có thể được phân tích bằng các công cụ kiểm chứng phần mềm như LTSA.
III. Chuyển đổi giữa các dạng biểu diễn của LTS
Chương này trình bày các phương pháp chuyển đổi giữa hai dạng biểu diễn của LTS là LF và FSP. Việc chuyển đổi này không chỉ giúp cải thiện khả năng tương tác giữa các công cụ kiểm chứng mà còn tối ưu hóa quy trình kiểm chứng phần mềm. Luận văn đề xuất một thuật toán để chuyển từ LF sang FSP và ngược lại, nhằm nâng cao hiệu quả của AGTool trong việc kiểm chứng phần mềm. Những cải tiến này sẽ giúp AGTool trở thành một công cụ hiệu quả hơn trong thực tế.
3.1 Chuyển đổi FSP sang LF
Chuyển đổi từ FSP sang LF yêu cầu một quy trình phân tích và chuyển đổi các hành động và trạng thái trong mô hình FSP thành dạng biểu diễn liệt kê. Quá trình này cần đảm bảo rằng tất cả các hành động và trạng thái đều được mô tả chính xác trong LF, từ đó tạo ra một mô hình có thể được kiểm chứng bằng AGTool. Việc thực hiện chuyển đổi này giúp tăng cường khả năng tương tác giữa AGTool và các công cụ kiểm chứng khác.
3.2 Chuyển đổi LF sang FSP
Chuyển đổi từ LF sang FSP cũng cần một quy trình tương tự, trong đó các hàm chuyển trạng thái trong LF sẽ được chuyển đổi thành các tiến trình trong FSP. Điều này không chỉ giúp tối ưu hóa quy trình kiểm chứng mà còn mở rộng khả năng sử dụng của AGTool trong các ứng dụng thực tế. Việc chuyển đổi này cũng giúp giảm thiểu lỗi trong quá trình kiểm chứng và nâng cao chất lượng phần mềm.
IV. Đánh giá thực nghiệm
Chương này trình bày kết quả thực nghiệm từ việc áp dụng các phương pháp chuyển đổi giữa LF và FSP trong AGTool. Các kết quả cho thấy rằng việc chuyển đổi này không chỉ cải thiện khả năng tương tác của AGTool mà còn nâng cao hiệu quả kiểm chứng phần mềm. Thực nghiệm cho thấy rằng AGTool có thể xử lý các mô hình phức tạp hơn và giảm thiểu thời gian kiểm chứng. Những cải tiến này mở ra hướng đi mới cho việc phát triển các công cụ kiểm chứng phần mềm trong tương lai.
V. Kết luận
Luận văn đã trình bày một cách chi tiết về khả năng chuyển đổi giữa các đặc tả hình thức trong kiểm chứng phần mềm. Các phương pháp chuyển đổi giữa LF và FSP đã được đề xuất và thực nghiệm cho thấy tính khả thi và hiệu quả của chúng. Những cải tiến này không chỉ giúp AGTool trở thành một công cụ mạnh mẽ hơn mà còn góp phần nâng cao chất lượng phần mềm trong ngành công nghiệp. Hướng phát triển trong tương lai sẽ tập trung vào việc tối ưu hóa các thuật toán chuyển đổi và mở rộng khả năng tương tác của AGTool với các công cụ kiểm chứng khác.
