SINH DỮ LIỆU THỬ CHO ỨNG DỤNG LUSTRE/SCADE SỬ DỤNG ĐIỀU KIỆN KÍCH HOẠT

Abstract

Kiểm thử là một trong những hoạt động quan trọng trong tiến trình phát triển phần mềm. Phần mềm phát triển ngày càng phức tạp, yêu cầu chất lượng ngày càng cao hơn, vai trò kiểm thử càng quan trọng hơn, đặc biệt là trong phát triển phần mềm cho các hệ thống phản ứng. Hệ thống phản ứng được phát triển phổ biến trong các lĩnh vực như hàng không, năng lượng, hạt nhân… Những hệ thống này thường yêu cầu rất cao về chất lượng và đòi hỏi các hoạt động kiểm thử nghiêm ngặt trước khi chúng được triển khai sử dụng. Lustre/SCADE là ngôn ngữ được sử dụng rộng rãi để phát triển phần mềm cho các hệ thống phản ứng, một lĩnh vực mà chất lượng phần mềm được yêu cầu hết sức nghiêm ngặt, gần như là không được phép xảy ra bất cứ một lỗi nhỏ nào. Điều này đòi hỏi việc kiểm thử phải được tiến hành thường xuyên và liên tục khi có bất cứ sự thay đổi nào trên ứng dụng. Bên cạnh đó, đối với những ứng dụng trong lĩnh vực này, việc kiểm thử thủ công sẽ rất khó thực hiện và không mang lại hiệu quả, do đó yêu cầu cần phải tự động hóa hoạt động kiểm thử cho các ứng dụng Lustre/SCADE. Trong bài báo này, chúng tôi tập trung nghiên cứu việc kiểm thử tự động cho các ứng dụng Lustre/SCADE. Chúng tôi đề xuất kỹ thuật sử dụng các điều kiện kích hoạt trên mạng lưới toán tử (operator network) để sinh ra các dữ liệu thử một cách tự động. Trong đó, kỹ thuật kiểm chứng mô hình (model checking) được sử dụng trong việc sinh tự động các dữ liệu thử này. Cuối cùng, chúng tôi thử nghiệm giải pháp này trên một chương trình Lustre/SCADE trong hệ thống điều khiển nhiệt độ môi trường.