Luận án tiến sĩ công nghệ thông tin mô hình hóa và đặc tả hình thức các giao diện thành phần có chứa chất lượng dịch vụ và tính tương tranh

Luận án tiến sĩ công nghệ thông tin tập trung mô hình hóa và đặc tả hình thức giao diện thành phần, tích hợp chất lượng dịch vụ và tính tương tranh.

• Người hướng dẫn: TS. Đặng Văn Hưng
• Trường học: Đại học Công nghệ, Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ Phần mềm
• Đề tài: Mô Hình Hóa Và Đặc Tả Hình Thức Giao Diện Thành Phần Với Chất Lượng Dịch Vụ Và Tính Tương Tranh
• Loại tài liệu: luận án
• Địa điểm: Hà Nội

Tóm tắt

I. Mô Hình Hóa

Mô hình hóa là quá trình xây dựng các mô hình toán học hoặc logic để biểu diễn các hệ thống phức tạp. Trong luận án, mô hình hóa được áp dụng để đặc tả các hệ thống phần mềm dựa trên thành phần có tính tương tranh và ràng buộc thời gian. Phương pháp này sử dụng lý thuyết Vết thời gian để mở rộng khả năng đặc tả các ràng buộc thời gian trên các hệ thống tương tranh. Mô hình hóa giao diện và mô hình hóa tương tranh là hai khía cạnh chính được nghiên cứu, giúp tăng cường khả năng kiểm chứng và đảm bảo chất lượng hệ thống.

1.1. Mô Hình Hóa Giao Diện

Mô hình hóa giao diện tập trung vào việc đặc tả các giao diện thành phần trong hệ thống. Luận án sử dụng ô-tô-mát giao diện tương tranh thời gian (TCIA) để biểu diễn các thành phần. Các giao diện này được thiết kế để đảm bảo tính tương thích và khả năng ghép nối giữa các thành phần. Phương pháp này giúp tăng cường khả năng kiểm chứng và đảm bảo chất lượng dịch vụ của hệ thống.

1.2. Mô Hình Hóa Tương Tranh

Mô hình hóa tương tranh nghiên cứu cách các thành phần trong hệ thống hoạt động song song. Luận án sử dụng lý thuyết Vết thời gian để đặc tả các hành vi tương tranh có ràng buộc thời gian. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

II. Đặc Tả Hình Thức

Đặc tả hình thức là quá trình sử dụng các phương pháp toán học để mô tả chính xác các yêu cầu và hành vi của hệ thống. Trong luận án, đặc tả hình thức được áp dụng để đặc tả các giao diện thành phần và các ràng buộc thời gian. Phương pháp này sử dụng lôgic thời gian thực tuyến tính (TLTL) để biểu diễn các thuộc tính của hệ thống. Đặc tả chất lượng dịch vụ và đặc tả tương tranh là hai khía cạnh chính được nghiên cứu, giúp đảm bảo tính chính xác và độ tin cậy của hệ thống.

2.1. Đặc Tả Chất Lượng Dịch Vụ

Đặc tả chất lượng dịch vụ tập trung vào việc đảm bảo các yêu cầu về thời gian và tài nguyên của hệ thống. Luận án sử dụng lý thuyết Vết thời gian để đặc tả các ràng buộc thời gian cứng và mềm. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện trong khoảng thời gian cho phép, tăng cường chất lượng dịch vụ.

2.2. Đặc Tả Tương Tranh

Đặc tả tương tranh nghiên cứu cách các thành phần trong hệ thống hoạt động song song. Luận án sử dụng ô-tô-mát khoảng bất đồng bộ (ADA) để biểu diễn các hành vi tương tranh có ràng buộc thời gian. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

III. Giao Diện Thành Phần

Giao diện thành phần là các điểm tương tác giữa các thành phần trong hệ thống. Trong luận án, giao diện thành phần được nghiên cứu để đảm bảo tính tương thích và khả năng ghép nối giữa các thành phần. Phương pháp này sử dụng ô-tô-mát giao diện tương tranh thời gian (TCIA) để biểu diễn các giao diện. Thành phần giao diện và giao diện tương tranh là hai khía cạnh chính được nghiên cứu, giúp tăng cường khả năng kiểm chứng và đảm bảo chất lượng hệ thống.

3.1. Thành Phần Giao Diện

Thành phần giao diện nghiên cứu cách các thành phần trong hệ thống tương tác với nhau. Luận án sử dụng lý thuyết Vết thời gian để đặc tả các giao diện thành phần. Phương pháp này giúp đảm bảo rằng các thành phần có thể hoạt động một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

3.2. Giao Diện Tương Tranh

Giao diện tương tranh tập trung vào việc đảm bảo tính tương tranh giữa các thành phần trong hệ thống. Luận án sử dụng ô-tô-mát khoảng bất đồng bộ (ADA) để biểu diễn các giao diện tương tranh. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

IV. Chất Lượng Dịch Vụ

Chất lượng dịch vụ là một yếu tố quan trọng trong việc đảm bảo hiệu suất và độ tin cậy của hệ thống. Trong luận án, chất lượng dịch vụ được nghiên cứu thông qua các ràng buộc thời gian và tài nguyên. Phương pháp này sử dụng lý thuyết Vết thời gian để đặc tả các yêu cầu về thời gian. Chất lượng giao diện và tương tranh dịch vụ là hai khía cạnh chính được nghiên cứu, giúp đảm bảo rằng hệ thống đáp ứng các yêu cầu về chất lượng dịch vụ.

4.1. Chất Lượng Giao Diện

Chất lượng giao diện nghiên cứu cách các giao diện thành phần đảm bảo chất lượng dịch vụ. Luận án sử dụng ô-tô-mát giao diện tương tranh thời gian (TCIA) để biểu diễn các giao diện. Phương pháp này giúp đảm bảo rằng các giao diện đáp ứng các yêu cầu về thời gian và tài nguyên.

4.2. Tương Tranh Dịch Vụ

Tương tranh dịch vụ tập trung vào việc đảm bảo tính tương tranh giữa các dịch vụ trong hệ thống. Luận án sử dụng lý thuyết Vết thời gian để đặc tả các hành vi tương tranh. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

V. Tính Tương Tranh

Tính tương tranh là một thuộc tính quan trọng của các hệ thống phần mềm, cho phép các dịch vụ được thực hiện song song. Trong luận án, tính tương tranh được nghiên cứu thông qua các mô hình và phương pháp đặc tả hình thức. Phương pháp này sử dụng lý thuyết Vết thời gian để đặc tả các hành vi tương tranh có ràng buộc thời gian. Mô hình hóa tương tranh và đặc tả tương tranh là hai khía cạnh chính được nghiên cứu, giúp đảm bảo rằng hệ thống hoạt động một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

5.1. Mô Hình Hóa Tương Tranh

Mô hình hóa tương tranh nghiên cứu cách các thành phần trong hệ thống hoạt động song song. Luận án sử dụng lý thuyết Vết thời gian để đặc tả các hành vi tương tranh có ràng buộc thời gian. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

5.2. Đặc Tả Tương Tranh

Đặc tả tương tranh tập trung vào việc đảm bảo tính tương tranh giữa các thành phần trong hệ thống. Luận án sử dụng ô-tô-mát khoảng bất đồng bộ (ADA) để biểu diễn các hành vi tương tranh. Phương pháp này giúp đảm bảo rằng các dịch vụ của hệ thống được thực hiện một cách hiệu quả và đáp ứng các yêu cầu về thời gian.

Trích đoạn nội dung tài liệu

Đặt vấn đề Công nghệ phần mềm dựa trên thành phần là một trong những sáng kiến kỹ thuật quan trọng nhất trong công nghệ phần mềm vì nó được coi là một cách tiếp cận mở, hiệu quả trong việc giảm chi phí và thời gian phát triển phần mềm trong khi vẫn được đảm bảo được chất lượng của sản phẩm [59]. Với cách tiếp cận này, hệ thống được xây dựng bằng việc ghép nối các thành phần phần mềm có sẵn. Mỗi thành phần riêng lẻ là một gói phần mềm, một dịch vụ Web hoặc một mô-đun được đóng gói và chúng giao tiếp với nhau thông qua các giao diện. Tuy nhiên, phương pháp này vẫn còn một số vấn đề được đặt ra [59].

Thứ nhất là làm sao đảm bảo được các thành phần hoạt động được khi ghép nối với nhau? Thứ hai là làm thế nào để có thể mở rộng các thành phần từ thành phần có sẵn, và quan trọng nhất là làm thế nào để đảm bảo chất lượng hệ thống tức là hệ thống sau khi xây dựng phải thỏa mãn các ràng buộc được đưa ra trong quá trình đặc tả ban đầu? Để giải quyết các vấn đề trên, một trong các giải pháp thông dụng và hiệu quả được sử dụng là áp dụng các phương pháp hình thức. Đây là phương pháp sử dụng các mô hình toán học cho việc đặc tả, phát triển và kiểm chứng các hệ thống phần mềm và phần cứng [8, 22, 44, 57]. Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống có yêu cầu chất lượng cao, chẳng hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, hệ thống điều khiển cần gạt ga tàu,v. Trong các hệ thống này, vấn đề an toàn hay an ninh có vai trò quan trọng để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi.

1 Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại giai đoạn phân tích thiết kế), nhưng cũng có thể được sử dụng cho các giai đoạn sau của quá trình xây dựng và phát triển hệ thống. Để một hệ thống có hiệu quả cao về chất lượng dịch vụ (chất lượng dịch vụ tốt), các phương thức cần được tiến hành song song để tăng khả năng và tốc độ tính toán (Vết Mazurkiewicz đã đặc tả được đặc tính này). Mặt khác, thực tế là chúng ta không nên gọi phương thức quá “dày”, nếu không có thể sẽ gây ra tình trạng dịch vụ không đáp ứng được. Một ví dụ nhỏ trên thực tế về vấn đề này mà chúng ta hay gặp phải là thao tác mở tệp tin (hoặc chương trình) trên máy tính (hệ điều hành windows).

Chúng ta nhấn đúp chuột để chạy một chương trình nào đó, nếu chưa thấy chương trình thực hiện, nhiều người sẽ lại nhấn đúp để mở lên và thao tác này được lặp lại nhiều lần cho tới khi trên màn hình hiển thị chương trình cần mở. Lúc này sẽ có nhiều bản sao của chương trình chạy lên (do nhấn nhiều lần) và người dùng lại phải đóng bớt đi (thường để lại một bản). Nguyên nhân của việc này là chương trình đó cần một khoảng thời gian để thực hiện nhưng người dùng không biết (không chờ) mà làm thao tác mở liên tục (gọi chương trình quá "dày"). Như vậy chúng ta cần có ràng buộc về thời gian cho mỗi phương thức thể hiện thời gian tối thiểu và tối đa phương thức cần để thực hiện và đáp ứng yêu cầu dịch vụ.

Do đó, thêm vào các ràng buộc thời gian cho vết Mazurkiewicz là hợp lý và phương pháp đặc tả hệ thống sử dụng vết Mazurkiewicz mở rộng về thời gian là có chứa chất lượng dịch vụ (về khía cạnh thời gian). Đối tượng nghiên cứu trong luận án là các hệ thống phần mềm dựa trên thành phần có tính tương tranh và có ràng buộc thời gian hay gọi một cách ngắn gọn là hệ tương tranh có ràng buộc (có yếu tố) thời gian nhằm tận dụng các thế mạnh của cách tiếp cận phát triển phần mềm dựa trên thành phần và các phương pháp hình thức trong phát triển phần mềm. Trong các hệ thống, tính tương tranh là một thuộc tính của hệ thống trong đó một số dịch vụ của hệ thống được cho phép truy cập một cách song song. Ràng buộc về thời gian trong luận án là các yêu cầu về thời gian thực thi của các hành động trong hệ thống, mỗi hành động sẽ được gắn với một khoảng thời gian cho việc thực thi của nó.

Như vậy, hệ tương tranh có ràng buộc thời gian trong luận án này là các hệ thống mà các hành động có thể thực hiện một cách song song, có sử dụng dịch vụ của nhau và thêm các ràng buộc về khoảng thời gian thực hiện của hành 2 động. Đây là một lớp bài toán nhỏ trong công nghệ phát triển phần mềm dựa trên thành phần nhưng lại có ứng dụng rất lớn và đòi hỏi độ tin cậy cao. Do đó, mục tiêu của luận án là phát triển một phương pháp hình thức để đặc tả và kiểm chứng các giao diện của các thành phần phần mềm có tính tương tranh và ràng buộc về thời gian. Sau đó, luận án áp dụng phương pháp được đề xuất vào việc đặc tả, phân tích và kiểm chứng các mô hình khác nhau của các hệ thống phần mềm dựa trên thành phần.

Hiện nay đã có một số các phương pháp đề xuất để giải quyết bài toán đặc tả và kiểm chứng hệ thống nhưng hiếm thấy phương pháp nào đặc tả đồng thời tính tương tranh và ràng buộc thời gian. Các phương pháp chung thường sử dụng các mô hình là các hệ dịch chuyển trạng thái hay các ô-tô-mát để đặc tả các hoạt động của một thành phần (hệ thống). Những phương pháp này đã có những kết quả tốt và được sử dụng rộng rãi nhưng không tập trung và hỗ trợ vào đặc tả thời gian cũng như tính tương tranh mà quan tâm tới việc làm thế nào để có thể mô hình được hệ thống như trong [56, 71, 72]. Một số phương pháp khác sử dụng các mô hình ngẫu nhiên [6], trong đó các nghiên cứu tập trung vào việc phát triển lý thuyết chuỗi Markov, chuỗi Markov thời gian và mô hình xác suất nhằm xử lý các hệ thống xác suất (bao gồm cả các ràng buộc thời gian và tương tranh).

Đây là một kiểu hệ thống có nhiều ứng dụng lớn, tuy nhiên mục tiêu của luận án không tập trung vào các hệ thống này. Để đặc tả các hệ tương tranh, công cụ được sử dụng phổ biến là lý thuyết Vết Mazurkiewicz [30, 55]. Các khái niệm về Vết Mazurkiewicz (gọi tắt là Vết) đã được giới thiệu để mô tả hành vi không liên tục của hệ thống song song thông qua các quan sát liên tục của nó. Vết biểu diễn quá trình đồng thời theo cùng một cách như các chuỗi biểu diễn một cách tuần tự.

Lý thuyết về Vết được sử dụng như một công cụ để suy luận về quy trình không liên tục; là một vấn đề của thực tế sử dụng lý thuyết này người ta có thể có được một tính toán của các tiến trình tương tranh tương tự như những cái có sẵn cho hệ thống tuần tự. Trong lý thuyết này, các khái niệm cơ bản được đề xuất là quan hệ phụ thuộc-độc lập, ngôn ngữ Vết, ô-tô-mát đoán nhận ngôn ngữ Vết cũng như lôgic thời gian tuyến tính biểu diễn Vết được đặc biệt quan tâm và có nhiều nghiên cứu hỗ trợ, mở rộng như trong [14, 31, 50, 68]. Điều này khẳng định lý thuyết Vết là công cụ có hiệu quả trong đặc tả các hệ tương tranh bởi tính đơn giản, 3 tiện dụng của phương pháp. Tuy nhiên công cụ này có hạn chế là không hỗ trợ đặc tả các ràng buộc thời gian.

Đây là một kiểu ràng buộc được yêu cầu trong nhiều ứng dụng quan trọng và phổ biến. Những hệ có ràng buộc này được gọi là các hệ thời gian thực hoặc đơn giản hơn là các hệ thống có ràng buộc thời gian. Do đó, nghiên cứu về đặc tả các hệ có các ràng buộc thời gian được nhiều nhà nghiên cứu quan tâm xem xét và đề xuất các phương pháp đặc tả và kiểm chứng. Hầu hết các đề xuất này đều dựa trên lý thuyết về các ô-tô-mát thời gian (TA - Timed Automata) [4, 11].

Lý thuyết này được coi là công cụ không thể thiếu khi nghiên cứu về các hệ thống thời gian thực. Ứng dụng ô-tô-mát thời gian, người phát triển hệ thống sẽ mô tả mỗi thành phần bằng một ô-tô-mát và hệ thống sẽ là một mạng các ô-tô-mát được ghép nối với nhau theo một cách thức phù hợp. Các kết quả về lý thuyết cũng như các thuật toán chứng minh đã được nghiên cứu và giới thiệu. Tuy nhiên, phương pháp này và các mở rộng như trong [46, 35] lại rất khó khăn trong việc mô tả các ràng buộc về tính tương tranh.

Chi tiết về lý thuyết Vết và ô-tô-mát thời gian sẽ được giới thiệu trong chương 2. Đây là hai lý thuyết nền tảng trong nghiên cứu của luận án này. Một số nghiên cứu khác đã sử dụng khái niệm Vết thời gian (timed traces) để mô tả hành vi hệ thống như trong [12, 73] và một số nghiên cứu liên quan. Trong các nghiên cứu này, Vết thời gian được định nghĩa nhằm giải các bài toán về kiểm chứng mô hình (Model checking) như việc sử dụng Vết thời gian được định nghĩa trên tập các đồng hồ của ô-tô-mát thời gian nhằm giải bài toán về giảm bùng nổ không gian trạng thái vùng trong ô-tô-mát thời gian hoặc giải các bài toán kiểm chứng cho mô hình mạch bất đồng bộ.

Các nghiên cứu này khác với nghiên cứu trong luận án về mục tiêu. Trong luận án, mục đích các nghiên cứu là đề xuất phương pháp đặc tả các giao diện của các thành phần. Tuy nhiên, điều dễ thấy là các nghiên cứu này và nghiên cứu trong luận án có thể hỗ trợ nhau nhằm phát huy hết lợi ích mà lý thuyết Vết mang lại. Gần đây, trong [27], các tác giả đã đề xuất một phương pháp đặc tả và kiểm chứng các giao diện thời gian thực.

Trong nghiên cứu này, hệ thống được hình thành bởi ghép nối các giao diện thời gian thực với nhau, mỗi giao diện biểu diễn một thành phần hệ thống. Giao diện thời gian thực là giao diện với ràng buộc thời gian liên quan giữa thời điểm đầu ra với thời điểm đầu vào. Tại một thời điểm trong quá trình thực hiện, một hành vi của giao diện theo một hợp đồng được thực hiện với môi trường về chức năng của nó cũng như thời gian 4 thực hiện để đảm bảo thực hiện hợp đồng.