Đặt vấn đề Trong ba thập kỷ vừa qua, công nghệ phần mềm dựa trên thành phần (Component-Based Software Engineering - CBSE) nổi lên như một cách tiếp cận quan trọng trong công nghệ phần mềm vì các đặc tính cả về nghiệp vụ và kỹ thuật của nó như: tăng hiệu quả, giảm chi phí, rút ngắn thời gian đưa sản phẩm ra thị trường, tăng khả năng bảo trì, v. Từ đó, việc đảm bảo chất lượng cho các phần mềm dựa trên thành phần (Component-Based Software - CBS) đóng vai trò sống còn trong vòng đời phát triển của chúng do yêu cầu ngày càng tăng về chất lượng. Với các sản phẩm phần mềm quan trọng có yêu cầu chất lượng cao như các phần mềm điều khiển ô tô, tàu hỏa, máy bay, v., các phần mềm này được yêu cầu thỏa mãn một số thuộc tính (thuộc tính được nghiên cứu trong luận án này là thuộc tính an toàn) cho trước, kiểm chứng là bắt buộc để đảm bảo thuộc tính đã cho không bị vi phạm trong toàn bộ thời gian hoạt động của chúng. Có hai hướng tiếp cận chính nhằm giải quyết vấn đề này gồm: hướng tiếp cận chứng minh định lý (theorem proving) là hướng tiếp cận bán tự động, đòi hỏi có sự tham gia của các chuyên gia trong quá trình kiểm chứng [31, 35, 53, 60, 61, 95], cần nhiều công sức và chi phí [9] và hướng tiếp cận kiểm chứng mô hình (model checking) là hướng tiếp cận hoàn toàn tự động [12].
Trong hai hướng tiếp cận này, hướng tiếp cận kiểm chứng mô hình [24, 25, 27, 54, 90] nhận được sự quan tâm đặc biệt trong cộng đồng nghiên cứu và trong công nghiệp phần mềm vì tính tự động hoàn toàn của nó. Kiểm chứng mô hình là hướng tiếp cận vét cạn thông qua việc duyệt qua toàn bộ không gian trạng thái của phần mềm để kiểm tra xem phần mềm có vi phạm thuộc tính 1 đã cho hay không. Nếu không có sự vi phạm nào, hệ thống ban đầu thỏa mãn thuộc tính đã cho. Ngược lại, một minh chứng về sự vi phạm sẽ được trả lại.
Vì đặc tính vét cạn không gian trạng thái của hệ thống cần kiểm chứng, hướng tiếp cận này gặp vấn đề về sự bùng nổ không gian trạng thái đối với các hệ thống lớn [24, 26, 90]. Để tận dụng được những ưu điểm của kiểm chứng mô hình và giải quyết vấn đề về bùng nổ không gian trạng thái, phương pháp kiểm chứng giả định - đảm bảo (Assume-Guarantee Verification - AGV) đã được đề xuất [23, 44, 52, 81, 88]. Kiểm chứng giả định-đảm bảo là phương pháp kiểm chứng dựa trên chiến lược chia để trị. Trong đó, hệ thống phần mềm lớn được chia thành các thành phần nhỏ hơn để kiểm chứng.
Từ đó, quá trình kiểm chứng kết luận rằng hệ thống tổng thể có thỏa mãn thuộc tính đã cho hay không mà không phải ghép nối toàn bộ các thành phần lại với nhau. Trong phương pháp kiểm chứng giả định - đảm bảo, có hai phương pháp lập luận: giả định - đảm bảo quay vòng (Circular Assume - Guarantee Reasoning - CIRC-AG) [3, 64, 75, 77, 78, 84] và giả định - đảm bảo không quay vòng (Non- Circular Assume - Guarantee Reasoning - NC-AG) [5, 21, 23, 41, 44, 68, 76, 96]. Trong luận án này, thuật ngữ “kiểm chứng giả định - đảm bảo quay vòng” và “kiểm chứng giả định - đảm bảo không quay vòng” được sử dụng lần lượt để chỉ “phương pháp kiểm chứng sử dụng lập luận quay vòng” và “phương pháp kiểm chứng sử dụng lập luận không quay vòng”. Sau này, phương pháp kiểm chứng giả định - đảm bảo không quay vòng được mở rộng, áp dụng cho các hệ thống được đặc tả bằng nhiều phương pháp khác nhau như: hệ chuyển trạng thái được gán nhãn (Labelled Transition Systems - LTS) [18, 22, 29, 41, 45, 46, 55, 56, 57, 58, 86], hệ thống có ràng buộc thời gian (timed systems) [68, 69], hệ thống chuyển trạng thái được đặc tả bằng lôgic mệnh đề [21, 48, 94], hệ thống chuyển trạng thái tượng trưng (symbolic transition systems) [6, 49, 82, 83], các hệ thống có yếu tố xác suất (probalistic systems) [16, 20, 37, 62], v.
Bài toán quan trọng nhất trong phương pháp kiểm chứng giả định - đảm bảo là làm sao để sinh được giả định. Để giải quyết vấn đề này, các phương pháp hiện nay đều dựa vào các thuật toán học ngôn ngữ chính quy thông qua sự tương tác của hai thực thể Learner và T eacher. Tùy vào loại hệ thống (có hoặc không có ràng buộc thời gian) và tùy vào phương pháp đặc tả được sử dụng (đặc tả bằng hệ chuyển trạng thái được gán nhãn, lôgic mệnh đề, và ô-tô-mát ghi sự kiện, v.), thuật toán sinh giả định sẽ được lựa chọn tương ứng (L∗ [8, 91], và 2 CDNF (Conjunction of Disjunctive Normal Form) [15, 21], T L∗ [68, 69], v. Mặc dù tồn tại nhiều phương pháp kiểm chứng giả định - đảm bảo, các phương pháp này đều có những ưu và nhược điểm nhất định.
Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các vấn đề còn tồn tại được trình bày trong Hình 1. Trong luận án này, phần mềm được đặc tả bằng các dạng đặc tả khác nhau như LTS, lôgic mệnh đề, và ô-tô-mát ghi sự kiện và thuộc tính được kiểm chứng là thuộc tính an toàn. Kiểm chứng M’ Tăng tốc độ hiệu quả? kiểm chứng? Mô hình phần mềm tiến hóa · Yes + giả định A · No + phản ví dụ cex Mô hình phần mềm Bùng nổ Kiểm chứng M với các không gian trạng thái? LTS Lôgic mệnh đề ERA loại đặc tả khác nhau? Hình 1.1: Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các vấn đề còn tồn tại. Phương pháp kiểm chứng giả định - đảm bảo cho hệ thống chuyển trạng thái được gán nhãn là phương pháp phổ biến nhất trong cộng đồng nghiên cứu cũng như trong việc áp dụng trong công nghiệp.
Trong phương pháp này, các luật kiểm chứng giả định - đảm bảo cho thấy rằng bản chất của bài toán kiểm chứng là bài toán bao của các ngôn ngữ và độ phức tạp của quá trình kiểm chứng tỉ lệ thuận với số trạng thái của giả định được sinh ra [100]. Theo đó, chi phí của quá trình kiểm chứng (chi phí được đề cập trong luận án này là chi phí về thời gian), đặc biệt trong ngữ cảnh tiến hóa (từ phần mềm M thành M 0 ), có thể nhỏ hơn nếu sử dụng giả định có số trạng thái và ngôn ngữ nhỏ hơn. Để sinh giả định cho bài toán kiểm chứng giả định - đảm bảo cho các hệ thống được đặc tả bằng LTS, Giannakopoulou và cộng sự là nhóm tác giả đầu tiên chỉ ra sự tồn tại của giả định yếu nhất (giả định có ngôn ngữ lớn nhất) trong kiểm chứng giả định - đảm bảo [41, 87]. Tiếp đó, Cobleigh và cộng sự đề xuất sử dụng thuật toán L∗ [8, 91] sinh giả định cho bài toán kiểm chứng giả định - đảm bảo [29].
Sau Cobleigh, có nhiều nghiên cứu mở rộng, cải tiến, tối ưu 3 cũng như áp dụng kết quả của Cobleigh cho nhiều ngữ cảnh khác của việc kiểm chứng phần mềm [10, 39, 87, 22, 28, 93, 17, 18, 19, 46, 38, 101, 86, 55, 57, 58]. Mặc dù vậy, vẫn chưa có nghiên cứu nào đề xuất phương pháp sinh giả định nhỏ nhất và mạnh nhất để giảm chi phí kiểm chứng phần mềm trong ngữ cảnh tiến hóa (tăng hiệu quả, tốc độ kiểm chứng M 0 ). Phương pháp kiểm chứng giả định - đảm bảo sử dụng đặc tả bằng LTS là phương pháp phổ biến và thường được áp dụng cho các hệ thống được đặc tả ở mức cao, như mức thiết kế, dưới dạng các hệ thống chuyển trạng thái. Tuy nhiên, độ phức tạp của nó vẫn rất cao.
Vì vậy, trường hợp hệ thống được đặc tả ở mức thấp hơn dưới dạng lôgic mệnh đề, một số nghiên cứu khác đã sử dụng phương pháp kiểm chứng được đề xuất bởi Chen và cộng sự để giảm độ phức tạp của quá trình kiểm chứng [21, 48]. Các thuật toán kiểm chứng giả định - đảm bảo sử dụng đặc tả bằng lôgic mệnh đề có những ưu điểm vượt trội so với các thuật toán sử dụng đặc tả bằng ô-tô-mát. Thứ nhất, về khả năng biểu diễn, đặc tả bằng lôgic mệnh đề tương đương với đặc tả bằng ô-tô-mát không đơn định và nó có thể biểu diễn súc tích hơn nhiều lần so với đặc tả bằng ô-tô-mát. Do đó, các thuật toán kiểm chứng sử dụng đặc tả bằng lôgic mệnh đề sinh các giả định có số trạng thái ít hơn nhiều lần các giả định sinh bởi các phương pháp sử dụng thuật toán L∗.
Thứ hai, xét về tốc độ thì thuật toán sinh giả định sử dụng đặc tả bằng lôgic mệnh đề sử dụng các thuật toán như CDNF [15], v. có tốc độ tốt hơn các thuật toán kiểm chứng sử dụng thuật toán L∗ [21]. Năm 2007, Sinha và cộng sự đã đề xuất sử dụng bộ giải nhằm kiểm tra tính thỏa mãn của hàm lôgic (SAT solver) cho bài toán kiểm chứng giả định - đảm bảo với các hệ thống được đặc tả bằng lôgic mệnh đề [94]. Năm 2010, Chen và cộng sự đã đề xuất áp dụng thuật toán CDNF được đề xuất bởi Bshouty [15] cho bài toán kiểm chứng giả định - đảm bảo cho hệ thống chuyển trạng thái được đặc tả bằng lôgic mệnh đề [21].
Sau Chen, năm 2016, He và cộng sự đã đề xuất một phương pháp sinh giả định có tốc độ nhanh và hiệu quả sử dụng thuật toán CDNF để sinh các giả định trong quá trình kiểm chứng giả định - đảm bảo cho hệ thống phần mềm được đặc tả bằng lôgic mệnh đề [48]. Sau đó, phương pháp này được áp dụng cho việc kiểm chứng hồi quy cho phần mềm tiến hóa. Tuy nhiên, trong ngữ cảnh tiến hóa phần mềm, thuật toán vẫn cần sinh lại giả định trong tất cả các trường hợp dù chỉ có sự thay đổi nhỏ trong các thành phần của phần mềm ban đầu. 4 Trong phát triển phần mềm nói chung, ngoài các phần mềm không có ràng buộc thời gian được đặc tả bằng LTS hoặc lôgic mệnh đề, v.v, các hệ thống có ràng buộc thời gian cũng nhận được sự quan tâm đặc biệt của cộng đồng nghiên cứu và trong công nghiệp.
Do đó, việc kiểm chứng các phần mềm này trở thành một xu hướng tất yếu do các đòi hỏi về chất lượng của các hệ thống thời gian thực ngày càng cao và trong nhiều lĩnh vực của đời sống xã hội như Internet vạn vật, khoa học vũ trụ, v. Một trong các phương pháp đặc tả các hệ thống có ràng buộc thời gian là sử dụng các ô-tô-mát ghi sự kiện (Event - Recording Automata - ERA) [4].