Luận văn: Nghiên cứu phương pháp xây dựng mô hình tự động - Đại học Quốc Gia Hà Nội

Luận văn nghiên cứu & xây dựng mô hình tự động. Tìm hiểu các phương pháp, quy trình triển khai mô hình tự động hóa hiệu quả. Ứng dụng thực tế và đánh giá kết quả.

• Tác giả: Lê Bá Cường
• Người hướng dẫn: TS. Phạm Ngọc Hùng
• Trường học: Đại học Quốc gia Hà Nội Trường Đại học Công nghệ
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Nghiên cứu phương pháp xây dựng mô hình tự động
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2011
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• DANH MỤC HÌNH VẼ
• DANH MỤC THUẬT TOÁN
• 1. Chương 1: Giới thiệu
• 2. Chương 2: Các phương pháp hình thức cho đặc tả phần mềm
• 2.1. Hệ thống chuyển trạng thái được gán nhãn
• 2.2. Phép ghép nối song song
• 2.3. Hệ chuyển trạng thái được gán nhãn an toàn, thuộc tính an toàn, tính thỏa mãn
• 2.4. Thành phần phần mềm
• 2.5. Ôtômát hữu hạn trạng thái
• 3. Chương 3: Các phương pháp sinh tự động mô hình thành phần phần mềm
• 3.1. Phương pháp học sử dụng giải thuật L*
• 3.1.1. Phương pháp xây dựng mô hình sử dụng thuật toán L*
• 3.2. Giải thuật Vasilevskii-Chow
• 3.3. Phương pháp xây dựng mô hình sử dụng thuật toán Thompson
• 3.3.1. Sinh dẫn xuất
• 3.3.2. Xây dựng mô hình
• 3.3.3. Tối ưu hóa mô hình
• 3.3.4. Độ phức tạp tính toán
• 4. Chương 4: Thực nghiệm
• 4.1. Công cụ xây dựng mô hình thành phần phần mềm
• 4.2. Ý nghĩa công cụ xây dựng mô hình
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Về Mô Hình Tự Động Nghiên Cứu Ứng Dụng 50 60 ký tự

Công nghệ phần mềm hướng thành phần đang ngày càng chứng minh được hiệu quả trong việc phát triển phần mềm, giúp giảm thiểu thời gian, công sức và nâng cao chất lượng. Việc tái sử dụng và tích hợp các thành phần phần mềm giúp xây dựng và phát triển phần mềm một cách nhanh chóng. Các ứng dụng được tạo ra bằng cách tích hợp các thành phần độc lập, tương tác với nhau. Các thành phần này có thể do nhà phát triển phần mềm hoặc bên thứ ba xây dựng. Một trong những vấn đề quan trọng nhất là đảm bảo rằng các thành phần phần mềm có thể phối hợp với nhau để đạt được mục tiêu chung của hệ thống. Các phương pháp kiểm thử và kiểm chứng mô hình là những giải pháp phổ biến hiện nay. Trong công nghiệp, các phương pháp kiểm thử thường được áp dụng rộng rãi để đảm bảo tính đúng đắn của phần mềm. Tuy nhiên, việc sinh ca kiểm thử thủ công thường tốn nhiều công sức và tính bao phủ không cao. Kiểm thử tự động là một giải pháp tiềm năng. Các phương pháp kiểm chứng mô hình hứa hẹn sẽ là cách tiếp cận hiệu quả để chứng minh tính đúng đắn của phần mềm. Để áp dụng các phương pháp này, cần xây dựng mô hình mô tả chính xác hành vi của hệ thống. Các nghiên cứu hiện nay về kiểm chứng mô hình và kiểm thử tự động thường giả định rằng mô hình hệ thống đã có sẵn và đúng đắn. Tuy nhiên, việc xây dựng mô hình hệ thống là một công việc khó khăn và dễ mắc lỗi. Thậm chí khi mô hình đã có và đúng, nó có thể không còn đúng khi phần mềm được phát triển thêm các hành vi mới. Một khó khăn khác là khi các thành phần phần mềm được phát triển bởi bên thứ ba, vì khi đó không có mã nguồn và tài liệu đầy đủ, hoặc tài liệu khó hiểu. Do đó, bài toán xây dựng mô hình mô tả chính xác hành vi của hệ thống có ý nghĩa to lớn trong việc kiểm chứng mô hình và kiểm thử tự động, cũng như có giá trị thực tiễn cao và được nhiều người quan tâm. Đề tài “Nghiên cứu phương pháp xây dựng mô hình tự động” được lựa chọn nhằm nghiên cứu phương pháp xây dựng mô hình tự động mô tả chính xác hành vi của hệ thống, làm cơ sở cho việc áp dụng các kỹ thuật kiểm chứng mô hình và kiểm thử tự động, góp phần nâng cao chất lượng phần mềm. Luận văn này trình bày các khái niệm cơ bản, các phương pháp hình thức cho đặc tả phần mềm, các khái niệm về thành phần phần mềm và đặc tả thành phần phần mềm, máy hữu hạn trạng thái, hệ chuyển trạng thái được gán nhãn, ôtômát hữu hạn trạng thái và các khái niệm liên quan. Hai giải pháp cho việc xây dựng mô hình thành phần phần mềm cũng được đề xuất: xây dựng mô hình sử dụng thuật toán học L* và xây dựng mô hình sử dụng thuật toán Thompson [11].

1.1. Tầm Quan Trọng Của Mô Hình Tự Động Hóa Trong Phát Triển Phần Mềm

Trong bối cảnh công nghệ phần mềm hiện đại, mô hình tự động đóng vai trò then chốt. Nó cho phép các nhà phát triển giảm thiểu công sức thủ công, tập trung vào các khía cạnh sáng tạo và chiến lược hơn của dự án. Tự động hóa mô hình không chỉ rút ngắn thời gian phát triển mà còn giảm thiểu rủi ro sai sót, đồng thời cải thiện khả năng tái sử dụng các thành phần. Như tác giả Lê Bá Cường đã nhấn mạnh, công nghệ phần mềm hướng thành phần, trong đó mô hình tự động đóng vai trò trung tâm, đang ngày càng trở nên quan trọng để đảm bảo sự cộng tác hiệu quả giữa các thành phần phần mềm. Áp dụng các phương pháp kiểm thử và kiểm chứng mô hình, đặc biệt là khi kết hợp với mô hình tự động, hứa hẹn nâng cao đáng kể chất lượng và độ tin cậy của phần mềm.

1.2. Các Phương Pháp Nghiên Cứu Mô Hình Tự Động Được Áp Dụng

Luận văn tập trung vào hai phương pháp chính để nghiên cứu mô hình tự động: thuật toán học L* và thuật toán Thompson. Thuật toán L*, được phát triển bởi Angluin [6] và cải tiến bởi Rivest và Schapire [13], là một phương pháp học lặp đi lặp lại để xây dựng mô hình ứng viên tương ứng với thành phần phần mềm. Thuật toán Thompson, dựa trên công trình của Thompson [11], xây dựng ôtômát hữu hạn như một mô hình mô tả chính xác hành vi của thành phần phần mềm. Các phương pháp này cung cấp các cách tiếp cận khác nhau để giải quyết bài toán xây dựng mô hình tự động, từ đó cho phép các nhà phát triển lựa chọn phương pháp phù hợp nhất với yêu cầu cụ thể của dự án.

II. Các Thách Thức Khi Xây Dựng Mô Hình Tự Động Chính Xác 55 ký tự

Việc xây dựng mô hình tự động chính xác cho các thành phần phần mềm, đặc biệt là khi chúng được phát triển bởi bên thứ ba, đặt ra nhiều thách thức đáng kể. Một trong những thách thức lớn nhất là thiếu thông tin chi tiết về mã nguồn và tài liệu. Ngay cả khi có tài liệu, nó có thể khó hiểu hoặc không đầy đủ. Việc xây dựng mô hình chính xác đòi hỏi phải hiểu rõ hành vi của thành phần phần mềm, nhưng điều này khó thực hiện khi thành phần được coi là một "hộp đen". Thêm vào đó, mô hình có thể trở nên lỗi thời khi phần mềm được tiến hóa với các hành vi mới. Việc duy trì mô hình cập nhật và chính xác đòi hỏi các phương pháp tự động hóa mô hình linh hoạt và có khả năng thích ứng với các thay đổi trong hành vi của phần mềm. Các phương pháp kiểm thử và kiểm chứng mô hình thường giả định rằng mô hình đã có sẵn và chính xác, nhưng thực tế, việc đảm bảo tính chính xác của mô hình là một thách thức lớn.

2.1. Vấn Đề Hộp Đen Trong Mô Hình Hóa Tự Động Thành Phần

Thành phần phần mềm thường được coi là 'hộp đen', nghĩa là chúng ta không thể biết được tất cả các trạng thái và hành vi bên trong nó. Việc thiếu thông tin này gây khó khăn lớn cho việc mô hình hóa tự động. Để vượt qua thách thức này, các phương pháp nghiên cứu mô hình tự động cần phải dựa vào các thử nghiệm và quan sát hành vi bên ngoài của thành phần. Các thuật toán như L* và Thompson được sử dụng để học và suy luận về hành vi của thành phần từ dữ liệu quan sát được, cho phép xây dựng mô hình tự động ngay cả khi thông tin chi tiết về thành phần bị hạn chế.

2.2. Khó Khăn Trong Việc Cập Nhật Mô Hình Tự Động Khi Phần Mềm Thay Đổi

Phần mềm liên tục phát triển và thay đổi. Khi các thành phần phần mềm được cập nhật hoặc thêm các hành vi mới, mô hình tự động cần phải được cập nhật để phản ánh những thay đổi này. Việc cập nhật thủ công mô hình có thể tốn thời gian và dễ mắc lỗi, vì vậy cần các phương pháp tự động hóa mô hình có khả năng phát hiện và thích ứng với các thay đổi. Các thuật toán học máy và phân tích hành vi có thể được sử dụng để tự động cập nhật mô hình khi có dữ liệu mới, đảm bảo rằng mô hình luôn chính xác và phù hợp với hành vi hiện tại của phần mềm.

2.3. Sự Phụ Thuộc Vào Tính Chính Xác Của Dữ Liệu Huấn Luyện Mô Hình Tự Động

Các thuật toán mô hình tự động học từ dữ liệu. Nếu dữ liệu huấn luyện không chính xác hoặc không đầy đủ, mô hình thu được có thể không phản ánh đúng hành vi của thành phần phần mềm. Đảm bảo tính chính xác và đầy đủ của dữ liệu huấn luyện là rất quan trọng để xây dựng mô hình tự động đáng tin cậy. Cần có các phương pháp để kiểm tra và làm sạch dữ liệu huấn luyện, cũng như để thu thập thêm dữ liệu khi cần thiết.

III. Phương Pháp L Nghiên Cứu Ứng Dụng Mô Hình Tự Động 57 ký tự

Giải thuật học L* học một ngôn ngữ không biết quy tắc để đưa ra một ôtômát hữu hạn đoán nhận nó. Ý tưởng chính của giải thuật này dựa trên định lý “Myhill – Nerode Theorem” [5] trong lý thuyết ngôn ngữ hình thức. Với mỗi tập có quy tắc U Σ*, tồn tại duy nhất một ôtômát tối tiểu mà tập các trạng thái của nó đẳng cấu với tập các lớp tương đương theo quan hệ sau: w ≈ w′ khi và chỉ khi u Σ*: wu U w′u U. Do đó, ý tưởng chính của L* là học các lớp tương đương. U là một ngôn ngữ không biết quy tắc trên bảng chữ cái Σ. Giải thuật * học L sẽ học để thu được một ôtômát hữu hạn đơn định (DFA) M như một ôtômát tối tiểu đoán nhận U, tức là L(M) = U. Để học được M, L* cần tương tác với một đối tượng giáo viên (Teacher), Teacher phải có khả năng trả lời hai loại câu hỏi như sau: Loại thứ nhất là câu hỏi truy vấn thành viên, với mỗi dẫn xuất Σ* thì U không? Teacher sẽ trả lời true nếu U, trái lại Teacher sẽ trả lời false. Loại thứ hai là câu hỏi kiểm tra ứng viên, với mỗi ứng viên DFA M thì M có phải là ôtômát đoán nhận U không (tức là L(M) = U?). Để làm được điều đó L* duy trì một bảng T mà mỗi bản ghi của nó lưu các chuỗi s Σ*, s có thuộc U hay không. Điều này được thực hiện bằng cách tạo các câu hỏi truy vấn thành viên gửi tới Teacher để cập nhật bảng T. Ở mỗi bước L* xây dựng một DFA M từ bảng T và yêu cầu Teacher trả lời câu hỏi kiểm tra ứng viên M có phải là ôtômát đoán nhận U hay không? Nếu Teacher trả lời true thì giải thuật sẽ dừng, trái lại L* sẽ sử dụng phản ví dụ được trả về bởi Teacher để cập nhật lại bảng T và tiếp tục lặp lại quá trình trên.

3.1. Cơ Chế Hoạt Động Của Thuật Toán L Trong Mô Hình Hóa Tự Động

Thuật toán L* hoạt động bằng cách tương tác với một "giáo viên" để học về ngôn ngữ của thành phần phần mềm. Thuật toán duy trì một bảng quan sát để ghi lại các chuỗi có thuộc ngôn ngữ của thành phần hay không. Bằng cách đặt câu hỏi truy vấn thành viên và câu hỏi kiểm tra ứng viên, L* dần dần xây dựng một ôtômát hữu hạn đơn định (DFA) mô tả ngôn ngữ của thành phần. Thuật toán sử dụng các phản ví dụ để tinh chỉnh mô hình, đảm bảo rằng nó chính xác và đầy đủ.

3.2. Ưu Điểm Và Nhược Điểm Của Phương Pháp L Trong Nghiên Cứu Mô Hình Tự Động

Ưu điểm chính của phương pháp L* là khả năng học một ôtômát tối tiểu đoán nhận ngôn ngữ của thành phần. Tuy nhiên, phương pháp này cũng có một số nhược điểm. Thứ nhất, nó đòi hỏi một "giáo viên" có khả năng trả lời các câu hỏi truy vấn và kiểm tra ứng viên, điều này có thể khó khăn trong thực tế. Thứ hai, độ phức tạp của thuật toán có thể cao, đặc biệt là khi kích thước của bảng chữ cái và số trạng thái của thành phần lớn.

IV. Giải Thuật Thompson Xây Dựng Mô Hình Tự Động Đơn Giản 59 ký tự

Trong phát triển phần mềm hướng thành phần, mỗi thành phần như một hộp đen và nó được biểu diễn bởi một máy hữu hạn trạng thái không xác định (QC, Σ, C, q0C) được định nghĩa trong Chương 2. Với máy hữu hạn trạng thái không xác định, chúng ta không thể biết được tất cả các trạng thái và hành vi của nó mà chỉ có thể tiến hành các thực hiện trên đó. Do đó, chúng ta có thể nhìn nhận nó như một bộ hai thành phần (Σ, T), với T Σ* là một tập đóng các chuỗi tiền tố trên bảng chữ cái Σ. Tập các chuỗi trong T tương ứng với các thực hiện được của thành phần phần mềm C. Với mỗi thành phần phần mềm C ta không biết trước được tất cả các trạng thái và hành vi của nó. Giả sử rằng mọi dẫn xuất của nó đều có độ dài không vượt quá một hằng số maxLength. Khi đó, chúng ta sẽ tìm tập các dẫn xuất của C có độ dài không vượt quá maxLength. Thuật toán sinh tập dẫn xuất sẽ mô tả quá trình sinh tập các dẫn xuất của một thành phần phần mềm C.

4.1. Quy Trình Xây Dựng Mô Hình Bằng Thuật Toán Thompson

Thuật toán Thompson xây dựng ôtômát hữu hạn từ một biểu thức chính quy. Trong bối cảnh mô hình tự động, thuật toán này được sử dụng để xây dựng ôtômát từ tập các dẫn xuất thực hiện được của thành phần phần mềm. Quy trình bao gồm việc xây dựng biểu thức chính quy tương đương với ngôn ngữ L (tập các dẫn xuất), sau đó áp dụng thuật toán Thompson để xây dựng ôtômát hữu hạn tương ứng.

4.2. Ưu Điểm Và Hạn Chế Của Thuật Toán Thompson Trong Tự Động Hóa Mô Hình

Thuật toán Thompson đơn giản và dễ cài đặt. Tuy nhiên, ôtômát thu được thường không đơn định và không tối tiểu. Điều này có nghĩa là nó có thể có nhiều trạng thái hơn cần thiết, dẫn đến hiệu suất kém hơn. Do đó, cần có các bước tối ưu hóa bổ sung để đơn định hóa và tối tiểu hóa ôtômát.

4.3. Các Bước Tối Ưu Hóa Mô Hình Tự Động Sau Khi Xây Dựng Bằng Thompson

Sau khi xây dựng ôtômát bằng thuật toán Thompson, cần thực hiện các bước tối ưu hóa để giảm kích thước và cải thiện hiệu suất của mô hình. Các bước này bao gồm loại bỏ các quy tắc rỗng, đơn định hóa ôtômát và tối tiểu hóa ôtômát. Thuật toán đơn định hóa chuyển đổi ôtômát không đơn định thành ôtômát đơn định. Thuật toán tối tiểu hóa giảm số lượng trạng thái trong ôtômát mà không thay đổi ngôn ngữ mà nó chấp nhận.

V. Thực Nghiệm Với GenModelTool Ứng Dụng Mô Hình Tự Động 54 ký tự

Để kiểm chứng và minh họa các phương pháp đã đề xuất, GenModelTool đã được phát triển, sử dụng thuật toán Thompson. Đầu vào của công cụ này là một bảng chữ cái gồm tập tất cả các hành động quan sát được trên thành phần phần mềm và tập các dẫn xuất là chuỗi các hành động có thể thực hiện được trên thành phần đó. GenModelTool sẽ trả về một ôtômát hữu hạn đoán nhận tập dẫn xuất trên. Công cụ được xây dựng bằng ngôn ngữ java với đầu vào được lưu trên file input. Dòng đầu tiên lưu bảng chữ cái là một tập tất cả các hành động có thể quan sát được trên thành phần phần mềm C. Các dòng tiếp theo mỗi dòng ghi một dẫn xuất là một chuỗi các hành động có thể thực hiện được trên C từ trạng thái khởi tạo. Sau khi mở tệp input.txt, dữ liệu đầu vào được hiển thị trên tab input. Lựa chọn chức năng Generate, chương trình sẽ gọi hàm makeDFA để xây dựng ôtômát hữu hạn đoán nhận tập dẫn xuất đầu vào. Khi đó, đầu ra của công cụ trên được biểu diễn trên tab output. Lựa chọn chức năng lưu tệp, chương trình sẽ lưu ôtômát hữu hạn thu được ở trên dưới một tệp output.

5.1. Kiến Trúc Và Chức Năng Của Công Cụ GenModelTool

GenModelTool là một công cụ được phát triển để tự động xây dựng mô hình thành phần phần mềm dựa trên thuật toán Thompson. Công cụ này nhận đầu vào là bảng chữ cái và tập các dẫn xuất thực hiện được của thành phần, sau đó tạo ra một ôtômát hữu hạn đoán nhận tập dẫn xuất đó. GenModelTool được xây dựng bằng ngôn ngữ Java và có giao diện người dùng đơn giản để dễ dàng sử dụng.

5.2. Ứng Dụng GenModelTool Để Xây Dựng Mô Hình Tự Động Cho Thành Phần Sender

GenModelTool được sử dụng để xây dựng mô hình cho một thành phần Sender với bảng chữ cái {in, send, ack} và tập các dẫn xuất {in, in send, in send ack}. Công cụ đã tạo ra một ôtômát hữu hạn đoán nhận tập dẫn xuất này, minh họa khả năng của nó trong việc tự động mô hình hóa hành vi của thành phần phần mềm.

5.3. Ý Nghĩa Của GenModelTool Trong Phát Triển Phần Mềm Hướng Thành Phần

GenModelTool có ý nghĩa quan trọng trong việc mô hình hóa tự động thành phần phần mềm, cung cấp cơ sở cho việc áp dụng các kỹ thuật kiểm chứng mô hình và kiểm thử tự động. Công cụ này giúp nâng cao chất lượng phần mềm và cung cấp đầu vào cho các công cụ khác như AGTool, hỗ trợ cho việc sinh giả định và kiểm chứng đảm bảo giả định.

VI. Kết Luận Và Hướng Phát Triển Mô Hình Tự Động 52 ký tự

Các phương pháp và công cụ được trình bày trong luận văn này cung cấp các giải pháp cho bài toán xây dựng mô hình tự động thành phần phần mềm. Thuật toán L* là một giải pháp toàn diện, nhưng đòi hỏi một "giáo viên" và có độ phức tạp cao. Thuật toán Thompson đơn giản và dễ cài đặt, nhưng cần các bước tối ưu hóa bổ sung. GenModelTool là một công cụ thực tế cho phép tự động mô hình hóa thành phần phần mềm dựa trên thuật toán Thompson. Trong tương lai, cần tập trung vào việc cải thiện các thuật toán mô hình tự động, đặc biệt là trong việc đối phó với các thành phần phức tạp và các thay đổi trong hành vi của phần mềm.

6.1. Tổng Kết Các Phương Pháp Nghiên Cứu Mô Hình Tự Động Trong Luận Văn

Luận văn đã trình bày hai phương pháp chính để nghiên cứu mô hình tự động: thuật toán L* và thuật toán Thompson. Thuật toán L* là một phương pháp học toàn diện, trong khi thuật toán Thompson là một phương pháp đơn giản và dễ cài đặt. Cả hai phương pháp đều có những ưu điểm và hạn chế riêng, và sự lựa chọn phương pháp phù hợp phụ thuộc vào yêu cầu cụ thể của dự án.

6.2. Hướng Phát Triển Tiềm Năng Cho Mô Hình Tự Động Hóa Trong Tương Lai

Trong tương lai, có nhiều hướng phát triển tiềm năng cho mô hình tự động hóa. Một hướng là cải thiện các thuật toán hiện có, đặc biệt là trong việc đối phó với các thành phần phức tạp và các thay đổi trong hành vi của phần mềm. Một hướng khác là khám phá các phương pháp mới, chẳng hạn như sử dụng học sâu để tự động học mô hình từ dữ liệu lớn. Cuối cùng, cần tập trung vào việc tích hợp mô hình tự động vào quy trình phát triển phần mềm để tự động hóa các tác vụ như kiểm thử và kiểm chứng.

6.3. Tầm Quan Trọng Của Mô Hình Tự Động Trong Phát Triển Phần Mềm Hiện Đại

Mô hình tự động đóng vai trò ngày càng quan trọng trong phát triển phần mềm hiện đại. Nó giúp tự động hóa các tác vụ tốn thời gian và dễ mắc lỗi, cho phép các nhà phát triển tập trung vào các khía cạnh sáng tạo và chiến lược hơn của dự án. Bằng cách sử dụng mô hình tự động, các nhà phát triển có thể xây dựng phần mềm chất lượng cao hơn trong thời gian ngắn hơn.

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

Chương 1 giới thiệu về đề tài. Chương này trình bày các ngữ cảnh, những lý do chọn đề tài, mục tiêu của đề tài và cấu trúc của luận văn. Chương 2 trình bày các khái niệm cơ bản phục vụ cho đề tài. Chương này mô tả các phương pháp hình thức cho đặc tả phần mềm, các khái niệm về thành phần phần mềm và đặc tả thành phần phần mềm, máy hữu hạn trạng thái, hệ chuyển trạng thái được gán nhãn, ôtômát hữu hạn trạng thái và các khái niệm liên quan.

Chương 3 nghiên cứu phương pháp xây dựng tự động mô hình mô tả chính xác hành vi của một thành phần phần mềm. Trong chương này, chúng tôi đề xuất hai giải pháp cho việc xây dựng mô hình thành phần phần mềm. Giải pháp thứ nhất là xây dựng mô hình sử dụng thuật toán học L*. Đây là phương pháp học lặp đi lặp lại để xây dựng mô hình ứng viên tương ứng với thành phần phần mềm C.

Ở mỗi bước lặp, chúng ta sẽ kiểm tra tính tương thích giữa mô hình ứng viên với thành phần C và cập nhật lại mô hình ứng viên nếu không tương thích. Giải pháp thứ hai là xây dựng mô hình sử dụng thuật toán Thompson [11]. Phương pháp này xây dựng ôtômát hữu hạn như một mô hình mô tả chính xác hành vi của thành phần phần mềm C tương đương với biểu thức chính quy sinh tập dẫn xuất trên C. Chương 4 giới thiệu về kết quả thực nghiệm.

Chương này trình bày những kết quả đạt được, công cụ sinh mô hình của một thành phần phần mềm và áp dụng cho một số ví dụ cụ thể. Cuối cùng là phần kết luận, định hướng mở rộng và tài liệu tham khảo. TIEU LUAN MOI download : [e-mail] 3 Chương 2: Các phương pháp hình thức cho đặc tả phần mềm 2.1 Hệ thống chuyển trạng thái được gán nhãn Mỗi thành phần phần mềm được đặc tả bởi một mô hình tương ứng mô tả hành vi của thành phần đó. Mô hình của thành phần phần mềm có thể được biểu diễn bởi một hệ chuyển trạng thái được gán nhãn [10], đó là một đồ thị có hướng với các nhãn trên các cạnh của nó.

Mỗi nhãn trên cạnh biểu diễn cho một hành động có thể thực hiện được bởi hệ thống, mỗi đỉnh của đồ thị là một trạng thái của mô hình, biểu diễn cho trạng thái của hệ thống. Tập tất cả các nhãn được gọi là bảng chữ cái. Ta ký hiệu Act là tập tất cả các hành động quan sát được, là hành động không quan sát được trong môi trường của thành phần phần mềm, là trạng thái lỗi đặc biệt của hệ thống, ta ký hiệu LTS  = <{π}, Act, , π>.1: Hệ thống chuyển trạng thái được gán nhãn (Labeled Transition System – LTS) Một hệ chuyển trạng thái được gán nhãn [10] M là một bộ có thứ tự gồm bốn thành phần (Q, , , q0), trong đó:  Q là tập khác rỗng các trạng thái của M,  Act là tập các hành động quan sát được, gọi là bảng chữ cái của M,  Qx x Q là hàm chuyển trạng thái, và  q0 Q là trạng thái khởi tạo. Ta ký hiệu qi qj nếu có một hành động với nhãn là a chuyển hệ thống từ trạng thái qi sang trạng thái qj, khi đó (qi, a, qj).

Điều này có nghĩa là khi hệ thống đang ở trạng thái qi nó có thể thực hiện một hành động a và chuyển sang trạng thái qj. Tương tự, khi hệ thống đang ở trạng thái qj có thể thực hiện một hành động a′ và chuyển sang trạng thái qk. Như vậy, ta có TIEU LUAN MOI download : [e-mail] 4 ′ một chuỗi các hành động qi qj qk. Khi đó, chúng ta có thể ′ ký hiệu: qi qk.

Một cách tổng quát, nếu chúng ta có một chuỗi các hành động qi qk biểu diễn hệ thống thì khi nó ở trạng thái qi nó có thể thực hiện một chuỗi các hành động a1.an và kết thúc ở trạng thái qk. Xét một hệ chuyển trạng thái được gán nhãn P = (Q, , , q0) với q, q′ Q, , i ta có: 1.1: q0 in q1 ack send q2 Hình 2.1: Một hệ thống chuyển trạng thái được gán nhãn.1 là một ví dụ về hệ chuyển trạng thái được gán nhãn L = (Q, , , q0), trong đó:  Q = {q0, q1, q2} là tập các trạng thái của L,  = {in, send, ack} là tập các hành vi của L,  = { (q0, in, q1), (q1, send, q2), (q2, ack, q0)} là các quy tắc chuyển trạng thái, và  q0 là trạng thái khởi đầu. TIEU LUAN MOI download : [e-mail] 5 Định nghĩa 2.2: Kích thước của hệ chuyển trạng thái được gán nhãn Kích thước của hệ chuyển trạng thái được gán nhãn M = (Q, , , q0) là số trạng thái của M, ký hiệu là |M|, trong đó |M| = |Q|.3: Hệ chuyển trạng thái được gán nhãn đơn định và không đơn định Một hệ chuyển trạng thái được gán nhãn M = (Q, , , q0) là không đơn định nếu - chuyển dịch hoặc nếu (q, a, q ) và (q, a, q") thì q q". Trái lại, M là hệ chuyển trạng thái được gán nhãn đơn định.1: Cho 2 hệ chuyển trạng thái được gán nhãn M = (Q, , , q0) và M' = (Q', , , q0').

Ta nói M chuyển dịch thành M' với chuyển dịch a nếu và chỉ nếu (q0, a, q0') , , Q = Q' và .2: Một hệ thống chuyển trạng thái được gán nhãn đơn định và không đơn định a q1 q0 a b c q2 Hình 2.2 – a: Hệ chuyển trạng thái được gán nhãn không đơn định.2–a mô tả một hệ chuyển trạng thái được gán nhãn L = (Q, , , q0), trong đó: Q = {q0, q1, q2}, = {a, b, c}, q0 là trạng thái khởi đầu, và = {(q0, a, q1), (q0, a, q2), (q1, b, q2), (q2, c, q0)}. Khi hệ thống đang ở trạng thái q0, thực hiện một hành động a thì hệ thống có thể chuyển đến trạng thái q1 hoặc trạng thái q2. Như vậy, trạng thái kế tiếp của q0 khi thực hiện cùng một hành động a là không xác định duy nhất TIEU LUAN MOI download : [e-mail] 6 hay không tất định. Ta gọi đó là hệ chuyển trạng thái được gán nhãn không đơn định.2 – b: Hệ chuyển trạng thái được gán nhãn đơn định.

Hệ chuyển trạng thái được gán nhãn như trên hình 2.2–b là một hệ chuyển trạng thái được gán nhãn đơn định. Từ trạng thái qi bất kỳ nếu thực hiện một hành động aj nào đó thì hệ thống sẽ chuyển sang một trạng thái xác định duy nhất qk.4: Vết của một hệ chuyển trạng thái được gán nhãn M Một vết của một hệ chuyển trạng thái được gán nhãn M = (Q, , , q0) là một chuỗi hữu hạn các hành động a1a2 …an với a1 = q0, ai (i = 1,…,n). Như vậy vết của hệ chuyển trạng thái được gán nhãn M là một chuỗi các hành động quan sát được mà M có thể thực hiện từ trạng thái khởi tạo q0.3: Cho một hệ chuyển trạng thái được gán nhãn M = (Q, , , q0) như trên hình 2.3 in q0 q1 ack send q2 Hình 2.3: Hệ chuyển trạng thái được gán nhãn. TIEU LUAN MOI download : [e-mail] 7 Trong đó: Q = { q0, q1, q2}, = {in, send, ack}, q0 là trạng thái khởi đầu, và = {(q0, in, q1), (q1, send, q2), (q2, ack, q0)}.

Với hệ chuyển trạng thái M được mô tả trên hình 2.3, chuỗi các hành động in send ack là một dẫn xuất trên M. Từ trạng thái q0, thực hiện hành động in hệ thống chuyển sang trạng thái q1, tiếp tục thực hiện hành động send hệ thống chuyển sang trạng thái q2, cuối cùng thực hiện hành động ack hệ thống trở về trạng thái q0. Tương tự trên một chuỗi in send ack in send cũng là một dẫn xuất trên M. Xét một chuỗi hành động in send in send ack trên M.

Ta thấy từ trạng thái khởi tạo q0 thực hiện hành động in hệ thống chuyển sang trạng thái q1, tiếp tục thực hiện hành động send hệ thống chuyển sang trạng thái q2, từ trạng thái q2 hệ thống không thể thực hiện được hành động in. Do đó chuỗi hành động trên không phải là một dẫn xuất trên M.2: Với Σ Act ta ký hiệu ↑Σ là một dẫn xuất thu được bằng cách loại bỏ khỏi tất cả các hành động a mà a  Σ. Tập tất cả các vết của M được gọi là ngôn ngữ của M, ký hiệu L(M).an là một vết hữu hạn trên hệ chuyển trạng thái được gán nhãn M. Ta ký hiệu hệ chuyển trạng thái được gán nhãn Mσ = (Q, , , q0) với Q = {q0, q1,., qn} và = { (qi-1, ai, qi)} với i=1,.

Ta nói rằng một hành động a được chấp nhận từ một trạng thái s Q nếu tồn tại s Q sao cho (s, a, s ). Tương tự vậy ta nói rằng một vết a1a2 …an được chấp nhận từ trạng thái s Q nếu tồn tại một dãy các trạng thái s0, s1, …, sn với s0 = q0 sao cho i= thì (si-1, ai, si) .2 Phép ghép nối song song Một toán tử ghép nối song song [10], ký hiệu || là một phép toán ghép nối hai thành phần phần mềm bằng cách đồng bộ các hành vi chung trên bảng chữ cái và đan xem các hành động còn lại. Giả sử có hai hệ chuyển trạng thái được gán nhãn là M1= (Q1, αM1, 1, q10) và M2= (Q2, αM2, 2, q20), phép ghép nối song song giữa M1 và M2, ký hiệu M1 || M2 được định nghĩa như sau: TIEU LUAN MOI download : [e-mail] 8 Nếu M1 =  hoặc M2 =  thì M1|| M2 = . Ngược lại, M1|| M2 = (Q, αM, , q0), trong đó: Q= Q1Q2, αM= αM1 αM2, q0 = (q10, q20) và hàm  được xác định như sau:  Với mọi (q1,a,q2) δ1 và (q1′, a, q2′) δ2 thì ( (q1, q1′), a, (q2, q2′) ) δ,  Với (q1,a,q2) δ1, a ∉ αM2 thì q′ Q2 ta có ( (q1,q′), a, (q2,q′) ) δ, và  Với (q1′, a, q2′) δ2, a ∉ αM1 thì q Q1 ta có ( (q, q1′), a, (q, q2′) ) δ.4: Mô hình ghép nối song song hai hệ chuyển trạng thái được gán nhãn Input và Output như trên hình 2.4 mô tả phép ghép nối song song hai hệ chuyển trạng thái được gán nhãn.

Trong đó, hai hành động send và ack là đồng bộ, các hành động còn lại đan xen nhau.