I. Hướng dẫn kiểm thử đột biến Lustre cho hệ thống an toàn
Trong lĩnh vực phát triển phần mềm cho các hệ thống an toàn-critical (safety-critical systems), việc đảm bảo chất lượng và độ tin cậy là yêu cầu bắt buộc. Ngôn ngữ lập trình Lustre, một ngôn ngữ đồng bộ luồng dữ liệu, đã trở thành một công cụ quan trọng để thiết kế các hệ thống phản ứng phức tạp như hệ thống điều khiển máy bay, lò phản ứng hạt nhân, hay hệ thống phanh ABS trên ô tô. Với các hệ thống này, một sai sót nhỏ trong phần mềm có thể gây ra hậu quả thảm khốc, do đó, quy trình xác minh và thẩm định (V&V - verification and validation) phải được thực hiện một cách nghiêm ngặt. Kiểm thử đột biến (mutation testing) nổi lên như một kỹ thuật kiểm thử hộp trắng mạnh mẽ, có khả năng đánh giá sâu sắc chất lượng của một bộ dữ liệu thử. Kỹ thuật này không chỉ tìm lỗi mà còn đo lường khả năng phát hiện lỗi của các ca kiểm thử. Nguyên lý cơ bản của kiểm thử đột biến dựa trên hai giả thuyết chính: "lập trình viên giỏi" (competent programmer hypothesis) và "hiệu ứng liên kết" (coupling effect hypothesis). Giả thuyết đầu tiên cho rằng các lập trình viên thường chỉ mắc phải những lỗi nhỏ, đơn giản. Giả thuyết thứ hai khẳng định rằng một bộ kiểm thử có khả năng phát hiện các lỗi đơn giản cũng sẽ có khả năng cao phát hiện các lỗi phức tạp hơn. Quy trình phân tích đột biến (mutation analysis) bắt đầu bằng việc tạo ra các phiên bản lỗi của chương trình gốc, gọi là các "đột biến" (mutants), bằng cách áp dụng các thay đổi cú pháp nhỏ thông qua các toán tử đột biến (mutation operators). Mục tiêu sau đó là tạo bộ kiểm thử (test suite generation) có khả năng "diệt" (kill) càng nhiều đột biến càng tốt, tức là làm cho kết quả đầu ra của đột biến khác với chương trình gốc.
1.1. Vai trò của ngôn ngữ lập trình Lustre trong hệ thống phản ứng
Lustre là một ngôn ngữ khai báo, được thiết kế đặc biệt cho các chương trình đồng bộ (synchronous programs). Đặc tính này làm cho nó cực kỳ phù hợp để mô hình hóa và phát triển các hệ thống phản ứng (reactive systems) - những hệ thống liên tục tương tác với môi trường và phải đáp ứng các ràng buộc thời gian thực nghiêm ngặt. Một chương trình Lustre được cấu thành từ các "node", mỗi node định nghĩa các mối quan hệ giữa luồng dữ liệu đầu vào và đầu ra. Khác với các ngôn ngữ lập trình mệnh lệnh, thứ tự các câu lệnh trong một node Lustre không quan trọng. Điều này cho phép thực hiện các phương pháp xác minh hình thức (formal verification) một cách hiệu quả, giúp chứng minh tính đúng đắn của chương trình. Các hệ thống được xây dựng bằng Lustre, chẳng hạn như các mô hình SCADE, yêu cầu mức độ tin cậy cao nhất, do đó, hoạt động kiểm thử đóng một vai trò không thể thiếu trong chu trình phát triển.
1.2. Nguyên lý cơ bản của phương pháp phân tích đột biến
Phân tích đột biến hoạt động bằng cách chèn các lỗi giả định vào mã nguồn. Mỗi lỗi được chèn thông qua một toán tử đột biến, tạo ra một phiên bản chương trình mới chỉ khác chương trình gốc ở một điểm duy nhất. Ví dụ, một toán tử có thể thay thế phép cộng (+) bằng phép trừ (-) hoặc thay đổi một toán tử quan hệ (>) thành (<=). Sau khi tạo ra một tập hợp các đột biến, chúng được thực thi với cùng một bộ dữ liệu thử như chương trình gốc. Nếu một ca kiểm thử tạo ra kết quả khác biệt giữa chương trình gốc và một đột biến, đột biến đó được coi là "bị diệt". Chất lượng của bộ dữ liệu thử được đo bằng điểm đột biến (mutation score) – tỷ lệ phần trăm các đột biến không tương đương đã bị diệt. Một điểm đột biến cao cho thấy bộ kiểm thử có năng lực phát hiện lỗi tốt.
II. Thách thức sinh đột biến Lustre Chi phí và độ phức tạp
Mặc dù kiểm thử đột biến cho Lustre là một phương pháp hiệu quả, việc áp dụng nó trong thực tế, đặc biệt với các dự án quy mô công nghiệp, gặp phải nhiều rào cản đáng kể. Thách thức lớn nhất đến từ chi phí tính toán và nguồn lực. Việc sinh đột biến bằng phương pháp thủ công là một công việc tốn nhiều thời gian, công sức và dễ xảy ra sai sót. Đối với một chương trình Lustre dù có quy mô vừa phải, số lượng đột biến có thể được tạo ra là rất lớn. Luận văn của Tạ Thanh Hải chỉ ra rằng, "số lượng các đột biến tạo ra xấp xỉ bằng tích của số các tham chiếu dữ liệu và số các đối tượng dữ liệu". Điều này có nghĩa là khi độ phức tạp của chương trình tăng lên, số lượng đột biến sẽ tăng theo cấp số nhân, khiến cho việc quản lý, biên dịch và thực thi từng đột biến trở nên không khả thi. Hơn nữa, mỗi đột biến cần được thực thi với ít nhất một ca kiểm thử, làm tăng gánh nặng về thời gian xử lý. Vấn đề thứ hai là sự tồn tại của các đột biến tương đương (equivalent mutants). Đây là những đột biến, mặc dù có cú pháp khác với chương trình gốc, nhưng lại tạo ra kết quả đầu ra giống hệt với mọi đầu vào khả dĩ. Việc xác định các đột biến này là một bài toán khó, thường đòi hỏi sự can thiệp thủ công của chuyên gia. Nếu không loại bỏ các đột biến tương đương, điểm đột biến sẽ không bao giờ đạt 100%, gây ra sự mơ hồ trong việc đánh giá chất lượng thực sự của bộ kiểm thử. Những khó khăn này đòi hỏi một giải pháp tự động hóa để giảm bớt gánh nặng và làm cho mutation testing for Lustre trở nên thực tế hơn.
2.1. Chi phí tính toán trong việc tạo và thực thi đột biến thủ công
Chi phí trong kiểm thử đột biến tập trung vào ba giai đoạn chính: sinh đột biến, biên dịch đột biến, và thực thi các ca kiểm thử trên từng đột biến. Khi thực hiện thủ công, mỗi giai đoạn đều tiêu tốn tài nguyên đáng kể. Người kiểm thử phải rà soát mã nguồn, xác định các vị trí có thể áp dụng toán tử đột biến, sau đó tạo ra từng tệp mã nguồn mới cho mỗi đột biến. Tiếp theo, mỗi tệp này phải được biên dịch riêng lẻ. Cuối cùng, toàn bộ bộ kiểm thử phải được chạy trên hàng trăm, thậm chí hàng nghìn phiên bản đột biến. Quy trình này không chỉ làm chậm tiến độ dự án mà còn tiềm ẩn nguy cơ lỗi do con người. Việc tự động hóa quá trình này là yêu cầu cấp bách để có thể áp dụng kiểm thử đột biến Lustre ở quy mô lớn.
2.2. Vấn đề nan giải về đột biến tương đương trong phân tích đột biến
Một đột biến được gọi là tương đương nếu nó luôn tạo ra kết quả giống hệt chương trình gốc, bất kể dữ liệu đầu vào. Ví dụ, câu lệnh x = y + z trong một ngữ cảnh if (y==2 && z==2) có thể bị đột biến thành x = y * z. Trong trường hợp này, cả hai phiên bản đều cho ra x = 4, khiến chúng trở nên tương đương và không thể bị "diệt". Việc phát hiện tự động các đột biến này là một vấn đề không thể giải quyết triệt để (undecidable problem). Trong thực tế, các kiểm thử viên thường phải phân tích thủ công từng đột biến "sống sót" để xác định xem chúng có tương đương hay không. Công việc này cực kỳ tốn thời gian và làm giảm hiệu quả của toàn bộ quy trình phân tích đột biến.
III. Phương pháp xây dựng công cụ sinh đột biến Lustre tự động
Để giải quyết các thách thức về chi phí và độ phức tạp, luận văn của Tạ Thanh Hải đã đề xuất và xây dựng một công cụ sinh đột biến tự động cho chương trình Lustre, được đặt tên là MuLustre. Phương pháp tiếp cận của công cụ này tập trung vào việc tự động hóa hoàn toàn quy trình từ phân tích mã nguồn đến tạo ra các tệp đột biến, giúp loại bỏ các thao tác thủ công tốn kém. Nền tảng của công cụ là một bộ phân tích cú pháp mạnh mẽ, có khả năng đọc và hiểu cấu trúc của một chương trình Lustre. Quy trình hoạt động của MuLustre bắt đầu bằng việc tiếp nhận một chương trình Lustre gốc làm đầu vào. Chương trình này sau đó được đưa qua một bộ phân tích cú pháp (Lustre Parser). Bộ phân tích này, được xây dựng dựa trên các công cụ Lex và Yacc, có nhiệm vụ tách mã nguồn thành các thành phần cú pháp cơ bản (tokens) và xây dựng một cây cấu trúc trừu tượng (Abstract Syntax Tree - AST) đại diện cho chương trình. Cây AST này là một dạng biểu diễn trung gian, lưu trữ tất cả thông tin về biến, hằng số, toán tử và cấu trúc lệnh của chương trình. Một khi đã có cây AST, công cụ sẽ duyệt qua cây này và xác định tất cả các vị trí mà các toán tử đột biến cho Lustre có thể được áp dụng. Dựa trên bộ toán tử đã được định nghĩa, công cụ sẽ tự động thực hiện các thay đổi trên cây AST để tạo ra các phiên bản đột biến. Cuối cùng, từ mỗi cây AST đã bị biến đổi, công cụ sẽ sinh ra một tệp mã nguồn Lustre hoàn chỉnh, tương ứng với một đột biến.
3.1. Kiến trúc hệ thống và quy trình hoạt động của công cụ MuLustre
Kiến trúc của MuLustre được thiết kế theo mô-đun để đảm bảo tính linh hoạt và khả năng mở rộng. Thành phần cốt lõi là Bộ phân tích cú pháp (Lustre Parser). Thành phần này chịu trách nhiệm biến đổi mã nguồn văn bản thành một cấu trúc dữ liệu mà máy tính có thể xử lý. Sau khi phân tích, một dạng trung gian (cây AST) được tạo ra. Tiếp theo, mô-đun Sinh đột biến (Mutant Generator) sẽ hoạt động. Mô-đun này chứa logic để áp dụng các mutation operators for Lustre lên cây AST. Mỗi toán tử đột biến được áp dụng sẽ tạo ra một bản sao của cây AST với một thay đổi nhỏ. Quy trình này được lặp lại cho đến khi tất cả các toán tử và tất cả các vị trí hợp lệ đều đã được xử lý. Kết quả là một tập hợp lớn các chương trình đột biến, sẵn sàng cho giai đoạn thực thi và đánh giá.
3.2. Vai trò của bộ phân tích cú pháp Lustre Parser Lex Yacc
Để tự động hóa việc sinh đột biến, bước đầu tiên và quan trọng nhất là phải "hiểu" được mã nguồn. MuLustre sử dụng hai công cụ kinh điển trong xây dựng trình biên dịch là Lex và Yacc. Lex (Lexical Analyzer Generator) chịu trách nhiệm phân tích từ vựng, tức là đọc chuỗi ký tự đầu vào và nhóm chúng thành các đơn vị có ý nghĩa gọi là token (ví dụ: từ khóa node, let, toán tử +, tên biến). Yacc (Yet Another Compiler-Compiler) sau đó nhận các token này và thực hiện phân tích cú pháp. Dựa trên một bộ quy tắc văn phạm được định nghĩa trước cho ngôn ngữ lập trình Lustre, Yacc xây dựng cây phân tích cú pháp, đảm bảo rằng chương trình tuân thủ đúng cú pháp của ngôn ngữ. Việc sử dụng Lex và Yacc giúp tự động hóa quá trình phân tích một cách hiệu quả và chính xác.
IV. TOP các toán tử đột biến cho Lustre được công cụ áp dụng
Hiệu quả của một hệ thống kiểm thử đột biến phụ thuộc rất lớn vào chất lượng và sự đa dạng của bộ toán tử đột biến được sử dụng. Các toán tử này được thiết kế để mô phỏng các lỗi phổ biến mà lập trình viên thường mắc phải. Công cụ MuLustre được xây dựng dựa trên một bộ 7 toán tử đột biến cho Lustre (mutation operators for Lustre) đã được định nghĩa và phân loại cẩn thận, bao trùm các lỗi về biến, hằng số và các loại biểu thức khác nhau. Các toán tử này đảm bảo rằng các đột biến được tạo ra có ý nghĩa và đại diện cho các sai sót tiềm tàng trong logic của chương trình. Việc lựa chọn và áp dụng các toán tử này một cách có hệ thống là chìa khóa để tạo bộ kiểm thử chất lượng, giúp cải thiện độ tin cậy của các hệ thống an toàn-critical. Mỗi toán tử nhắm vào một loại lỗi cụ thể, từ việc thay thế đơn giản một biến cho đến thay đổi logic của các biểu thức quan hệ hay số học. Ví dụ, toán tử thay thế toán tử số học (ARO) có thể thay đổi một phép cộng thành phép nhân, mô phỏng lỗi tính toán. Tương tự, toán tử thay thế toán tử quan hệ (RRO) có thể thay đổi điều kiện x > y thành x <= y, mô phỏng lỗi trong logic điều khiển. Sự kết hợp của các toán tử này cho phép tạo ra một tập hợp đột biến đa dạng, thách thức bộ kiểm thử ở nhiều khía cạnh khác nhau.
4.1. Nhóm toán tử đột biến biến và hằng số VRO CRO
Nhóm toán tử này tập trung vào các lỗi liên quan đến việc sử dụng sai dữ liệu. Toán tử thay thế biến (VRO - Variable Replacement Operator) hoạt động bằng cách thay thế một biến này bằng một biến khác cùng kiểu trong chương trình. Lỗi này rất phổ biến, ví dụ như lập trình viên gõ nhầm tên biến. Toán tử thay thế hằng số (CRO - Constant Replacement Operator) cũng hoạt động tương tự, thay thế một hằng số này bằng một hằng số khác. Cả hai toán tử này giúp phát hiện các lỗi liên quan đến việc khởi tạo hoặc tham chiếu dữ liệu sai.
4.2. Nhóm toán tử đột biến biểu thức số học và quan hệ ARO RRO
Đây là nhóm toán tử quan trọng nhất, nhắm vào logic tính toán và điều khiển. Toán tử thay thế toán tử số học (ARO - Arithmetic Replacement Operator) thay thế một toán tử số học (+, -, *, /, mod, div) bằng một toán tử khác trong cùng nhóm. Toán tử thay thế toán tử quan hệ (RRO - Relational Replacement Operator) thay thế một toán tử quan hệ (=, <, <=, >, >=, <>) bằng một toán tử khác. Những đột biến này rất hiệu quả trong việc kiểm tra các điều kiện biên và các nhánh logic của chương trình.
4.3. Nhóm toán tử đột biến biểu thức luận lý và một ngôi LRO UOI UOD
Toán tử thay thế toán tử luận lý (LRO - Logical Replacement Operator) thay thế các toán tử như and, or, xor với nhau. Toán tử chèn toán tử một ngôi (UOI - Unary Operator Insertion), cụ thể là chèn toán tử not, nhằm kiểm tra các trường hợp phủ định logic. Ngược lại, Toán tử xóa toán tử một ngôi (UOD - Unary Operator Delete), ví dụ như xóa toán tử thời gian pre(), giúp phát hiện các lỗi liên quan đến trạng thái và bộ nhớ trong các chương trình đồng bộ.
V. Ứng dụng công cụ sinh đột biến và đánh giá kết quả thực tiễn
Mục tiêu cuối cùng của việc xây dựng một công cụ tự động là để áp dụng vào thực tế và đánh giá hiệu quả của nó. Công cụ MuLustre đã được thử nghiệm trên một số lượng lớn các chương trình Lustre để kiểm chứng khả năng sinh đột biến và tính khả thi của phương pháp. Kết quả thực nghiệm được trình bày trong luận văn cho thấy công cụ hoạt động hiệu quả, có khả năng phân tích và tạo ra hàng trăm, thậm chí hàng nghìn đột biến một cách nhanh chóng và chính xác. Quá trình thử nghiệm không chỉ xác nhận rằng việc tự động hóa là khả thi mà còn cung cấp những dữ liệu quý giá về hiệu suất của các toán tử đột biến cho Lustre. Ví dụ, kết quả cho thấy các toán tử như ARO (thay thế toán tử số học) và RRO (thay thế toán tử quan hệ) có khả năng sinh ra số lượng đột biến lớn nhất, phản ánh sự phổ biến của các biểu thức này trong các chương trình thực tế. Sau khi sinh đột biến, bước tiếp theo là đánh giá chất lượng của một bộ dữ liệu thử ngẫu nhiên bằng cách tính điểm đột biến (mutation score). Kết quả cho thấy, ngay cả với bộ thử được sinh ngẫu nhiên, một tỷ lệ đáng kể các đột biến đã bị "diệt", chứng tỏ tiềm năng của phương pháp. Phân tích các đột biến còn "sống sót" cung cấp thông tin chi tiết để cải thiện bộ kiểm thử, giúp người kiểm thử tập trung vào việc tạo bộ kiểm thử mới để diệt các đột biến "cứng đầu" hơn, từ đó nâng cao chất lượng tổng thể của quy trình xác minh và thẩm định (V&V).
5.1. Kết quả thử nghiệm sinh đột biến tự động trên các chương trình Lustre
Công cụ MuLustre được thử nghiệm với nhiều chương trình Lustre có độ phức tạp khác nhau. Bảng kết quả trong luận văn (Bảng 3.2 và 3.3) cho thấy số lượng đột biến được tạo ra tương ứng với từng toán tử. Chẳng hạn, một chương trình đơn giản có thể tạo ra vài chục đột biến, trong khi các chương trình lớn hơn có thể tạo ra hàng trăm đột biến. Quá trình này, nếu thực hiện thủ công, sẽ mất rất nhiều giờ, nhưng với công cụ tự động, nó chỉ mất vài giây hoặc vài phút. Điều này chứng minh rằng tự động hóa giúp giảm đáng kể thời gian và chi phí trong giai đoạn chuẩn bị cho mutation testing for Lustre.
5.2. Phân tích điểm đột biến và hiệu quả của bộ dữ liệu thử
Chỉ sinh đột biến là chưa đủ; mục tiêu là sử dụng chúng để đánh giá và cải thiện bộ kiểm thử. Trong thử nghiệm, một bộ dữ liệu thử được sinh ngẫu nhiên và chạy trên các đột biến đã tạo. Điểm đột biến sau đó được tính theo công thức MS = D / (M - E), trong đó D là số đột biến bị diệt, M là tổng số đột biến, và E là số đột biến tương đương. Kết quả thực nghiệm (Bảng 3.4) cho thấy các tỷ lệ đột biến khác nhau cho các chương trình khác nhau, cung cấp một thước đo định lượng về chất lượng của bộ thử. Một điểm số thấp chỉ ra rằng bộ thử cần được cải thiện, trong khi một điểm số cao mang lại sự tin tưởng hơn vào tính toàn diện của nó.
VI. Tương lai của công cụ sinh đột biến tự động cho Lustre
Việc xây dựng thành công công cụ MuLustre đã mở ra một hướng đi đầy hứa hẹn cho việc áp dụng kiểm thử đột biến trong các dự án phát triển bằng ngôn ngữ lập trình Lustre. Đây là một đóng góp quan trọng, giúp tự động hóa một khâu tốn kém trong quy trình xác minh và thẩm định (V&V), đặc biệt là đối với các hệ thống an toàn-critical. Công cụ này không chỉ giúp giảm chi phí và thời gian mà còn nâng cao độ tin cậy của phần mềm bằng cách cung cấp một phương pháp có hệ thống để đánh giá và cải thiện chất lượng bộ kiểm thử. Tương lai của các công cụ sinh đột biến tự động cho Lustre nằm ở việc tích hợp sâu hơn vào các quy trình phát triển phần mềm hiện đại (DevOps, CI/CD) và kết hợp với các kỹ thuật xác minh khác. Một hướng phát triển tiềm năng là tích hợp khả năng phát hiện đột biến tương đương một cách tự động, có thể bằng cách sử dụng các kỹ thuật tối ưu hóa trình biên dịch hoặc các bộ giải ràng buộc (constraint solvers). Một hướng khác là kết hợp phân tích đột biến với các phương pháp xác minh hình thức (formal verification). Ví dụ, các đột biến còn "sống sót" sau khi kiểm thử có thể trở thành mục tiêu cho các công cụ kiểm tra mô hình (model checking) để chứng minh chúng có tương đương hay không. Cuối cùng, việc mở rộng bộ toán tử đột biến cho Lustre để bao quát nhiều loại lỗi hơn, đặc biệt là các lỗi liên quan đến đặc tính thời gian thực và đồng bộ của chương trình đồng bộ, cũng là một lĩnh vực nghiên cứu quan trọng.
6.1. Đóng góp vào quy trình xác minh và thẩm định V V phần mềm
Công cụ sinh đột biến tự động như MuLustre góp phần hoàn thiện quy trình V&V bằng cách cung cấp một thước đo khách quan về chất lượng của bộ kiểm thử. Thay vì chỉ dựa vào các độ đo bao phủ mã nguồn truyền thống (như bao phủ dòng lệnh hay nhánh), điểm đột biến cung cấp một chỉ báo mạnh mẽ hơn về khả năng phát hiện lỗi. Việc tự động hóa giúp kỹ thuật này trở nên khả thi để áp dụng thường xuyên trong chu trình phát triển, cho phép phát hiện sớm các điểm yếu trong bộ kiểm thử và cải thiện chúng một cách kịp thời.
6.2. Hướng phát triển Tích hợp xác minh hình thức và tối ưu hóa
Trong tương lai, các công cụ này có thể được cải tiến để trở nên thông minh hơn. Một hướng đi là sử dụng thông tin từ phân tích đột biến để tự động tạo bộ kiểm thử mới nhằm diệt các đột biến còn sống. Kỹ thuật này, được gọi là sinh dữ liệu thử dựa trên đột biến (mutation-based test data generation), có thể sử dụng các thuật toán tối ưu hóa hoặc giải thuật di truyền. Hơn nữa, việc tích hợp với các công cụ xác minh hình thức sẽ tạo ra một quy trình V&V toàn diện, kết hợp sức mạnh của cả kiểm thử (testing) và chứng minh (proving) để đảm bảo mức độ an toàn cao nhất cho các hệ thống phần mềm quan trọng.
