Chương 1 GIỚI THIỆU 1. Đặt vẫn đề Phát triển phần mềm dựa trên công nghệ hướng thành phần (Component- based Software Development - CBSD) đang được quan tâm như là cách tiếp cận chủ yếu để xây dựng các phần mềm hiện nay. Phần mềm dựa trên thành phần được xây dựng bằng cách ghép nối các thành phần đã có sẵn. Các thành phần này hoặc do công ty tự phát triển trước đó hoặc được cung cấp bởi bên thứ ba.
Với cách tiếp cận này, chúng ta có thể giảm đáng kể chi phí và thời gian phat triển trong khi vẫn đảm bảo được chất lượng của phần mềm. Tuy nhiên, một trong những hạn chế lớn nhất của công nghệ hướng thành phần là làm thế nào để đảm bảo rằng các thành phần sau khi ghép nối với nhau có thể cộng tác để đạt được mục tiêu của hệ thống - việc đảm bao cơ chế “plug-and-play”. Dac biệt, đối với những ứng dụng yêu cầu chất lượng cao như các hệ thống điều khiển tên lửa, máy bay, an ninh quốc phòng, v. thì việc dam bảo tính đúng đắn của thiết kế trước khi thực hiện các pha tiếp theo là bắt buộc.
Hiện tại, các công nghệ hỗ trợ phát triển hướng thành phần chỉ cho phép kiểm tra khả năng ghép nối giữa các thành phần chứ không có cơ chế đảm bảo tính cộng tác của chúng. Kết quả, các sản phẩm phần mềm hiện nay có chất lượng thấp, không đáp ứng yêu cầu. Để giải quyết các nhược điểm của CBSD, hiện nay cùng với chứng minh định lý (theorem proving) [36], kiểm chứng mô hình (model checking) [23, 73] được biết đến như một giải pháp phổ biến để giải quyết vấn đề này. Để áp dụng các phương pháp kiểm chứng mô hình, ta cần phải xây dựng các mô hình đặc tả hành vi của hệ thống cần kiểm chứng [27, 26, 88].
Những mô hình này thường được biểu diễn bằng các máy hữu hạn trạng thái đơn định. Các nghiên cứu hiện tai hầu hết giả sử các mô hình này đã có và đúng đắn [54, 52, 51]. Tuy nhiên, giả thiết này rất khó đáp ứng trong thực tế vì việc xây dựng mô hình cho các phần mềm là một công việc khó khăn và tiềm an nhiều lỗi. Trong thực tế, các thiết kế biểu diễn bằng UML 2.0 rất phổ biến ở các công ty.
Nếu như chúng ta có cơ chế chuyển đổi dang đặc tả UML 2.0 sang các máy hữu hạn trạng thái đơn định thì khả năng ứng dụng sẽ tốt hơn. Làm thế nào để kiểm chứng tính đúng đắn của biểu đồ tuần tự nói riêng và các thiết kế nói chung là vấn đề mở và chưa có lời giải thỏa đáng. Giả sử chúng ta đã có các mô hình của các thành phần mô tả chính xác hành vi của chúng. Để áp dụng các phương pháp kiểm chứng mô hình, chúng ta phải chép nối các mô hình này để thu được một mô hình ghép nối duy nhất của hệ thống.
Mô hình sau khi được ghép nối kết hợp với đặc tả thuộc tính cần kiểm tra là dữ liệu vào đối với các công cụ kiểm chứng. Tuy nhiên, số lượng trạng thái của mô hình ghép nối thường rất lớn nên vấn đề bùng nổ không gian trạng thái có thể xảy ra khi kiểm chứng các phần mềm có kích thước lớn. Khó khăn trong việc xây dựng mô hình và vấn đề bùng nổ không gian trạng thái được xem là nguyên nhân chủ yếu cho việc khó áp dụng các phương pháp kiểm chứng mô hình trong thực tế. Kiểm chứng từng phần (modular verification) [30, 62, 65] là giải pháp hứa hẹn nhằm xử lý sự bùng nổ không gian trạng thái đối với kiểm chứng mô hình.
Trong cách tiếp cận này, thay vì kiểm chứng trên toàn bộ mô hình ghép nối, chúng ta chỉ cần kiểm chứng trên từng mô hình của mỗi thành phần riêng biệt. Khi tất cả các thành phần đã được kiểm chứng, chúng ta có thể kết luận phần mềm thỏa mãn thuộc tính cần kiểm chứng mà không cần ghép nối các mô hình của các thành phần với nhau. Kiểm chứng giả định - đảm bảo (Assume — Guarentee Verification) [25, 33] và sau đó được cải tiến trong [52| là hiện thực hóa của tư tưởng kiểm chứng từng phần. Trong phương pháp này, để kiểm chứng các hệ thống con một cách riêng biệt, chúng ta cần các giả định (assumptions) về môi trường mà mỗi hệ thống con sẽ được thực hiện ứng với thuộc tính cần kiểm chứng [24].
Tuy nhiên, độ phức tap của việc sinh giả định còn cao. Hơn nữa, các phương pháp này chỉ mới giải quyết được các hệ thống đơn giản gồm hai thành phần. Các phần mềm thực tế thường có nhiều hơn hai thành phần và ý tưởng của các phương pháp này khó tổng quát hóa cho trường hợp này. Mặc dù đã có nhiều nghiên cứu quan tâm giải quyết vấn đề đặc tả và kiểm chứng tính đúng đắn của thiết kế phần mềm dựa trên thành phần, các vấn đề sau vẫn còn là các bài toán mở và chưa có giải pháp thỏa đáng.
e Chưa có giải pháp để xây dựng mô hình đặc tả hình thức hành vi của từng thành phần phần mềm nói riêng và hệ thống dựa trên thành phần nói chung. Cần đề xuất một giải pháp đầy đủ từ đầu đến cuối cho bài toán kiểm chứng mô hình phần mềm dựa trên thành phần, từ bước sinh đặc tả hình thức đến áp dụng công cụ kiểm chứng để nhận được kết quả về tính đúng đắn của thiết kế. Mặc dù đã có nhiều phương pháp và công cụ kiểm chứng mô hình phần mềm khác nhau với yêu cầu đầu vào là các đặc tả hình thức phù hợp tương ứng, bản thân việc sinh các đặc tả hình thức đúng đắn, tiêu chuẩn hóa, từ các tài liệu thiết kế phần mềm là một thách thức cần giải quyết. Hạn chế này là nguyên nhân chính dẫn đến việc khó áp dụng các phương pháp kiểm chứng mô hình trong thực tế.
e Biểu đồ tuần tự UML là một tài liệu thiết kế phần mềm tiêu chuẩn. Đã có các nghiên cứu về kiểm chứng tính đúng đắn của biểu đồ tuần tự UML, nhưng không tách biệt quá trình sinh mô hình với bước kiểm chứng mô hình. Việc tự động sinh mô hình từ biểu đồ tuần tự UML và cho phép sự dụng lại mô hình một cách hợp lý là rất cần thiết. e Với sự tăng nhanh về kích thước cũng như sự phức tạp của phần mềm, việc kiểm chứng và đảm bảo tính đúng đắn của phần mềm ngày càng trở nên quan trọng và ngày càng khó khăn hơn do các phần mềm ngày càng phức tạp.
Hiện tại, chưa có một giải pháp đủ tốt để giải quyết vấn đề này. e Chưa có một công cụ đủ tốt tích hợp các giải pháp trên trong một công cụ kiểm chứng nhằm tự động hóa quá trình đặc tả và kiểm chứng cho thành phần phần mềm dựa trên biểu đồ tuần tự. Mục tiêu của luận án để giải quyết các vấn đề nêu trên. Kiểm chứng mô hình cho phần mềm dựa trên thành phần là một giải pháp đảm bảo chất lượng phần mềm ngay từ bước thiết kế.
Thách thức của kiểm chứng mô hình là cần có các đặc tả hình thức tiêu chuẩn, đúng đắn và công cụ phù hợp. Đã có nhiều nghiên cứu về phương pháp kiểm chứng mô hình phần mềm và một số bộ công cụ kiểm chứng khác nhau đã được phát triển. Để áp dụng kiểm chứng mô hình trong thực tiễn, cần lựa chọn giải pháp, sinh mô hình đặc tả đúng, phù hợp với phương pháp kiểm chứng và yêu cầu của bộ công cụ kiểm chứng được lựa chọn. Một cách lý tưởng, phương pháp đề xuất cần xây dựng mô hình cho mỗi thành phần phần mềm bằng cách phân tích tất cả các biểu đồ UML đặc tả các khung nhìn khác nhau về thành phần này.
Tuy nhiên, do hạn chế về thời gian nên phạm vi nghiên cứu của luận án này là các thiết kế của các thành phần phần mềm được biểu diễn dưới dang các biểu đồ tuần tự UML bởi đây là biểu đồ có hành vi chi tiết nhất trong các biểu đồ UML, một loại tài liệu thiết kế phần mềm phổ biến và nghiên cứu xuyên suốt quy trình, đề xuất giải quyết các khó khăn thách thức gặp phải, hoàn thiện thuật toán nâng cao tính hiệu quả khi áp dụng thực tiễn để có thể nhận được kết quả kiểm chứng cuối cùng. Mục tiêu của luận án là đề xuất một số phương pháp hỗ trợ sinh tự động mô hình đặc tả hành vi của thiết kế phần mềm dưới dạng biểu đồ tuần tự UML và kết hợp phương pháp kiểm chứng giả định - đảm bảo kiểm chứng tính đúng đắn của các thiết kế này một cách hiệu quả. Mặt khác, luận án đề xuất phương pháp sinh mô hình và kiểm chứng tính đúng đắn của các biểu đồ tuần tự UML sử dụng ôtômát vào/ra và công cụ kiểm chứng SPIN. Để giải quyết một số hạn chế trong kiểm chứng giả định - đảm bảo, luận án đề xuất một phương pháp để tạo ra các giả định nhỏ nhất cục bộ cho phương pháp kiểm chứng giả định - đảm bảo và hai cải tiến nhằm giảm độ phức tạp trong việc sinh giả định.
Luận án hướng đến một giải pháp đầy đủ cho việc kiểm chứng tính đúng đắn của các thiết kế có khả năng ứng dụng trong thực tế. Đối tượng nghiên cứu của luận án là thiết kế của các hệ thống phần mềm dựa trên thành phần. Các phần mềm này được phát triển bằng cách ghép nối các thành phần sẵn có với chất lượng cao. Đây là giải pháp phổ biến nhất hiện nay để phát triển các ứng dụng vì nó giảm thiểu thời gian cũng như chi phí phát triển trong khi vẫn đảm bảo được chất lượng phần mềm.
Tuy nhiên, chúng ta chưa có cơ chế đảm bảo tính cộng tác giữa các thành phần. Hệ quả là các thành phần không thể cộng tác được với nhau sau khi được ghép nối. Một cách lý tưởng, phương pháp đề xuất cần xây dựng mô hình cho mỗi thành phần phần mềm bằng cách phân tích tất cả các biểu đồ UML đặc tả các khung nhìn khác nhau về thành phần này. Tuy nhiên, do hạn chế về thời gian nên phạm vi nghiên cứu của luận án này là các thiết kế của các thành phần phần mềm được biểu diễn dưới dạng các biểu đồ tuần tự UML 2.0 bởi đây là biểu đồ có hành vi chỉ tiết nhất trong các biểu đồ UML.
Để đạt được mục tiêu nghiên cứu, luận án sẽ tiến hành khảo sát các giải pháp đã có. Từ đó, luận án sẽ xác định các hạn ché/van đề chưa giải quyết được và đề xuất phương pháp mới hoặc cải tiến các phương pháp hiện có.