Luận văn thạc sĩ: Nghiên cứu phương pháp xây dựng mô hình tự động trong công nghệ phần mềm

Luận văn thạc sĩ VNU UET nghiên cứu phương pháp xây dựng mô hình tự động, cung cấp kiến thức và ứng dụng trong lĩnh vực công nghệ.

• 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
• 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 phần mềm
• 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
• 1.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.2. Phương pháp xây dựng mô hình sử dụng thuật toán L*
• 3.3. Giải thuật Vasilevskii-Chow
• 3.4. Phương pháp xây dựng mô hình sử dụng thuật toán Thompson
• 3.5. Sinh dẫn xuất
• 3.6. Xây dựng mô hình
• 3.7. Tối ưu hóa mô hình
• 3.8. Độ 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ề nghiên cứu phương pháp tự động xây dựng mô hình phần mềm

Nghiên cứu phương pháp tự động xây dựng mô hình phần mềm đang trở thành một lĩnh vực quan trọng trong công nghệ thông tin. Phương pháp này không chỉ giúp giảm thiểu thời gian phát triển mà còn nâng cao chất lượng phần mềm. Việc áp dụng các kỹ thuật tự động hóa trong xây dựng mô hình giúp đảm bảo rằng các thành phần phần mềm có thể tương tác hiệu quả với nhau.

1.1. Định nghĩa và vai trò của mô hình phần mềm

Mô hình phần mềm là một biểu diễn trừu tượng của hành vi và cấu trúc của phần mềm. Nó giúp các nhà phát triển hiểu rõ hơn về cách thức hoạt động của hệ thống và đảm bảo rằng các thành phần phần mềm có thể hoạt động cùng nhau.

1.2. Lợi ích của việc tự động hóa trong xây dựng mô hình

Tự động hóa quy trình xây dựng mô hình giúp tiết kiệm thời gian và công sức, đồng thời giảm thiểu lỗi do con người gây ra. Điều này cũng giúp tăng cường tính chính xác và độ tin cậy của mô hình phần mềm.

II. Các thách thức trong nghiên cứu phương pháp tự động xây dựng mô hình phần mềm

Mặc dù có nhiều lợi ích, việc tự động xây dựng mô hình phần mềm cũng gặp phải nhiều thách thức. Một trong những vấn đề lớn nhất là đảm bảo rằng mô hình được xây dựng chính xác và có thể phản ánh đúng hành vi của hệ thống thực tế.

2.1. Khó khăn trong việc xác định hành vi của hệ thống

Việc xác định hành vi của hệ thống là một thách thức lớn, đặc biệt khi các thành phần phần mềm được phát triển bởi nhiều bên khác nhau. Điều này có thể dẫn đến việc mô hình không chính xác hoặc không đầy đủ.

2.2. Vấn đề về tính tương thích giữa các thành phần

Một thách thức khác là đảm bảo rằng các thành phần phần mềm có thể tương tác với nhau một cách hiệu quả. Việc này đòi hỏi phải có các phương pháp kiểm thử và kiểm chứng mô hình hiệu quả.

III. Phương pháp tự động xây dựng mô hình phần mềm hiệu quả

Để giải quyết các thách thức trong việc xây dựng mô hình phần mềm, nhiều phương pháp tự động đã được phát triển. Những phương pháp này không chỉ giúp xây dựng mô hình mà còn đảm bảo tính chính xác và hiệu quả.

3.1. Phương pháp học sử dụng giải thuật L

Giải thuật L* là một phương pháp học tự động giúp xây dựng mô hình chính xác bằng cách lặp đi lặp lại quá trình kiểm tra và cập nhật mô hình ứng viên. Phương pháp này đã chứng minh được tính hiệu quả trong việc xây dựng mô hình phần mềm.

3.2. Phương pháp xây dựng mô hình sử dụng thuật toán Thompson

Thuật toán Thompson cho phép 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. Phương pháp này giúp tạo ra các mô hình chính xác từ các biểu thức chính quy.

IV. Ứng dụng thực tiễn của phương pháp tự động xây dựng mô hình phần mềm

Các phương pháp tự động xây dựng mô hình phần mềm đã được áp dụng rộng rãi trong nhiều lĩnh vực khác nhau. Những ứng dụng này không chỉ giúp nâng cao chất lượng phần mềm mà còn cải thiện quy trình phát triển phần mềm.

4.1. Ứng dụng trong kiểm thử phần mềm

Phương pháp tự động xây dựng mô hình đã được sử dụng để tạo ra các ca kiểm thử tự động, giúp giảm thiểu thời gian và công sức trong quá trình kiểm thử phần mềm.

4.2. Ứng dụng trong kiểm chứng mô hình

Kiểm chứng mô hình là một lĩnh vực quan trọng trong phát triển phần mềm. Các phương pháp tự động giúp đảm bảo rằng mô hình phần mềm đáp ứng các yêu cầu và tiêu chuẩn chất lượng.

V. Kết luận và tương lai của nghiên cứu phương pháp tự động xây dựng mô hình phần mềm

Nghiên cứu phương pháp tự động xây dựng mô hình phần mềm đang mở ra nhiều cơ hội mới cho ngành công nghệ thông tin. Tương lai của lĩnh vực này hứa hẹn sẽ có nhiều tiến bộ và cải tiến, giúp nâng cao chất lượng phần mềm và quy trình phát triển.

5.1. Định hướng nghiên cứu trong tương lai

Các nghiên cứu trong tương lai có thể tập trung vào việc phát triển các phương pháp tự động hóa mới, nhằm cải thiện tính chính xác và hiệu quả của mô hình phần mềm.

5.2. Tác động của công nghệ mới đến phương pháp xây dựng mô hình

Sự phát triển của công nghệ mới như trí tuệ nhân tạo và học máy có thể tạo ra những cơ hội mới cho việc tự động hóa quy trình xây dựng mô hình phần mềm, từ đó nâng cao chất lượng và hiệu quả.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh phát triển phần mềm hiện đại, công nghệ phần mềm hướng thành phần (Component-Based Software Engineering - CBSE) được xem là phương pháp hiệu quả nhằm giảm thiểu thời gian và công sức phát triển đồng thời nâng cao chất lượng sản phẩm. Theo ước tính, việc tái sử dụng và tích hợp các thành phần phần mềm độc lập giúp tăng tốc độ phát triển phần mềm lên đến 30-50%. Tuy nhiên, một trong những thách thức lớn nhất là đảm bảo các thành phần này có thể cộng tác hiệu quả để đạt được mục tiêu hệ thống. Vấn đề này càng trở nên phức tạp khi các thành phần được phát triển bởi bên thứ ba, không có mã nguồn hoặc tài liệu đầy đủ.

Mục tiêu nghiên cứu của luận văn là phát triển phương pháp xây dựng mô hình tự động mô tả chính xác hành vi của thành phần phần mềm, 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. Phạm vi nghiên cứu tập trung vào ngành Công nghệ phần mềm, với các phương pháp hình thức và thuật toán học máy hữu hạn trạng thái, áp dụng trong khoảng thời gian đến năm 2011 tại Việt Nam. Việc xây dựng mô hình chính xác không chỉ giúp nâng cao chất lượng phần mềm mà còn giảm thiểu chi phí kiểm thử và kiểm chứng, đồng thời tăng tính tin cậy của hệ thống.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Luận văn dựa trên các lý thuyết và mô hình sau:

• Hệ chuyển trạng thái được gán nhãn (Labeled Transition System - LTS): Mô hình biểu diễn hành vi của thành phần phần mềm dưới dạng đồ thị có hướng với các trạng thái và hành động quan sát được. LTS được định nghĩa bởi bộ bốn thành phần (Q, Act, δ, q0), trong đó Q là tập trạng thái, Act là bảng chữ cái các hành động, δ là hàm chuyển trạng thái, và q0 là trạng thái khởi tạo.

• Ôtômát hữu hạn trạng thái (Deterministic Finite Automata - DFA): Mô hình toán học dùng để nhận dạng ngôn ngữ chính quy, gồm tập trạng thái, bảng chữ cái, hàm chuyển trạng thái, trạng thái khởi tạo và tập trạng thái kết thúc. DFA được sử dụng để mô tả chính xác hành vi của thành phần phần mềm.

• Thuật toán học L* của Angluin: Thuật toán học lặp đi lặp lại để xây dựng mô hình DFA tối tiểu dựa trên các truy vấn thành viên và kiểm tra ứng viên, tương tác với một đối tượng giáo viên (Teacher) để xác định tính chính xác của mô hình.

• Thuật toán Thompson: Thuật toán xây dựng ôtômát hữu hạn không đơn định (NDFA) từ biểu thức chính quy, được sử dụng để sinh mô hình từ tập các dẫn xuất hành vi của thành phần phần mềm.

Các khái niệm chính bao gồm: hệ chuyển trạng thái đơn định và không đơn định, thuộc tính an toàn, phép ghép nối song song, máy hữu hạn trạng thái không xác định (UFSM), và các phép toán trên ngôn ngữ chính quy (hợp, nhân, lặp).

Phương pháp nghiên cứu

Nguồn dữ liệu chính là các thành phần phần mềm được xem như hộp đen, chỉ có thể quan sát các hành vi thông qua các chuỗi hành động thực hiện được. Phương pháp nghiên cứu gồm:

• Phương pháp học sử dụng thuật toán L*: Thuật toán này xây dựng mô hình DFA tối tiểu bằng cách tương tác với thành phần phần mềm qua các truy vấn thành viên (kiểm tra chuỗi hành động có phải thực hiện được hay không) và kiểm tra ứng viên mô hình. Giải thuật Vasilevskii-Chow được sử dụng để kiểm tra tính tương thích giữa mô hình ứng viên và thành phần phần mềm.

• Phương pháp xây dựng mô hình sử dụng thuật toán Thompson: Thu thập tập các dẫn xuất hành vi có độ dài hữu hạn từ thành phần phần mềm, xây dựng biểu thức chính quy tương ứng, sau đó sử dụng thuật toán Thompson để tạo ôtômát hữu hạn không đơn định mô tả hành vi.

Quá trình nghiên cứu được thực hiện theo timeline gồm: thu thập dữ liệu hành vi, xây dựng mô hình ứng viên, kiểm tra và tối ưu hóa mô hình, và cuối cùng là phát triển công cụ hỗ trợ tự động hóa quá trình này.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

1. Xây dựng mô hình chính xác bằng thuật toán L*: Thuật toán L* có thể học được mô hình DFA tối tiểu mô tả chính xác hành vi của thành phần phần mềm. Độ phức tạp tính toán của thuật toán là O(k n² + n log m), trong đó k là kích thước bảng chữ cái, n là số trạng thái của mô hình, và m là độ dài phản ví dụ. Tuy nhiên, việc cài đặt thực tế gặp khó khăn do yêu cầu tương tác phức tạp với đối tượng Teacher và chi phí kiểm tra tương thích cao.

2. Phương pháp xây dựng mô hình sử dụng thuật toán Thompson: Thu thập tập dẫn xuất hành vi có độ dài tối đa maxLength, xây dựng biểu thức chính quy và ôtômát hữu hạn tương ứng. Độ phức tạp của quá trình là O(maxLength * n^{maxLength}), với n là kích thước bảng chữ cái. Mô hình thu được có thể không tối tiểu và không đơn định, nhưng có thể được tối ưu hóa qua các bước loại bỏ quy tắc rỗng, đơn định hóa và tối tiểu hóa.

3. Công cụ GenModelTool: Đã được phát triển để tự động hóa quá trình 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ụ nhận đầu vào là bảng chữ cái và tập các dẫn xuất hành vi, xuất ra ôtômát hữu hạn mô tả chính xác hành vi. Ví dụ thực nghiệm với thành phần Sender cho thấy công cụ có thể xây dựng mô hình với tập hành vi {in, send, ack} và các dẫn xuất {in, in send, in send ack} một cách hiệu quả.

4. Ý nghĩa thực tiễn: Mô hình thu được từ GenModelTool có thể làm đầu vào cho các công cụ kiểm chứng giả định như AGTool, hỗ trợ kiểm chứng đảm bảo giả định trong phát triển phần mềm hướng thành phần, giúp giảm thiểu chi phí kiểm chứng toàn bộ hệ thống.

Thảo luận kết quả

Kết quả cho thấy phương pháp học L* là toàn diện và cho mô hình tối tiểu, nhưng khó áp dụng thực tế do yêu cầu tương tác phức tạp và chi phí tính toán cao. Trong khi đó, phương pháp thuật toán Thompson tuy đơn giản hơn và dễ cài đặt, nhưng mô hình thu được cần qua các bước tối ưu để đạt hiệu quả sử dụng cao.

So sánh với các nghiên cứu trong ngành, việc kết hợp hai phương pháp có thể mang lại lợi ích tối ưu: sử dụng thuật toán Thompson để xây dựng mô hình ban đầu, sau đó áp dụng thuật toán học L* hoặc các kỹ thuật tối ưu hóa để cải thiện mô hình. Việc áp dụng các mô hình này trong kiểm thử tự động và kiểm chứng mô hình giúp nâng cao độ tin cậy và giảm thiểu lỗi phần mềm.

Dữ liệu có thể được trình bày qua biểu đồ so sánh độ phức tạp tính toán, bảng thống kê số trạng thái mô hình trước và sau tối ưu hóa, cũng như sơ đồ kiến trúc công cụ GenModelTool.

Đề xuất và khuyến nghị

1. Phát triển và hoàn thiện công cụ học mô hình L*: Tập trung vào việc tối ưu hóa thuật toán Vasilevskii-Chow để giảm chi phí kiểm tra tương thích, đồng thời xây dựng giao diện tương tác hiệu quả với đối tượng Teacher nhằm tăng tính khả thi của phương pháp học L* trong thực tế.

2. Tích hợp hai phương pháp xây dựng mô hình: Sử dụng thuật toán Thompson để tạo mô hình ban đầu, sau đó áp dụng thuật toán học L* hoặc các kỹ thuật tối ưu hóa để cải thiện mô hình, nhằm cân bằng giữa độ chính xác và chi phí tính toán.

3. Mở rộng phạm vi ứng dụng công cụ GenModelTool: Phát triển thêm các tính năng hỗ trợ nhập xuất dữ liệu đa dạng, tích hợp với các công cụ kiểm thử tự động và kiểm chứng mô hình, đồng thời hỗ trợ các ngôn ngữ lập trình và môi trường phát triển khác nhau.

4. Đào tạo và phổ biến kiến thức: Tổ chức các khóa đào tạo, hội thảo về phương pháp xây dựng mô hình tự động và ứng dụng trong kiểm thử phần mềm, nhằm nâng cao nhận thức và kỹ năng cho các nhà phát triển phần mềm và kiểm thử viên.

Các giải pháp trên nên được thực hiện trong vòng 1-2 năm, với sự phối hợp giữa các nhóm nghiên cứu, doanh nghiệp phát triển phần mềm và các tổ chức đào tạo.

Đối tượng nên tham khảo luận văn

1. Nhà nghiên cứu và sinh viên ngành Công nghệ phần mềm: Luận văn cung cấp kiến thức sâu rộng về các phương pháp hình thức, thuật toán học máy hữu hạn trạng thái và ứng dụng trong xây dựng mô hình phần mềm, hỗ trợ nghiên cứu và học tập chuyên sâu.

2. Kỹ sư phát triển phần mềm hướng thành phần: Các kỹ sư có thể áp dụng các phương pháp và công cụ được đề xuất để xây dựng mô hình hành vi thành phần, từ đó nâng cao chất lượng và độ tin cậy của sản phẩm phần mềm.

3. Chuyên gia kiểm thử và kiểm chứng phần mềm: Luận văn cung cấp cơ sở lý thuyết và công cụ hỗ trợ kiểm thử tự động và kiểm chứng mô hình, giúp cải thiện hiệu quả và độ chính xác của quá trình kiểm thử.

4. Doanh nghiệp phát triển phần mềm và tổ chức đào tạo: Các tổ chức này có thể sử dụng luận văn làm tài liệu tham khảo để phát triển công cụ, quy trình kiểm thử và đào tạo nhân lực chuyên môn cao trong lĩnh vực kiểm thử và phát triển phần mềm hướng thành phần.

Câu hỏi thường gặp

1. Phương pháp học L* có thể áp dụng cho các thành phần phần mềm phức tạp không?
   Phương pháp L* có thể áp dụng cho các thành phần phức tạp nhưng chi phí tính toán và yêu cầu tương tác với đối tượng Teacher tăng theo kích thước mô hình, do đó cần tối ưu thuật toán và công cụ hỗ trợ để đảm bảo khả thi.

2. Thuật toán Thompson có ưu điểm gì so với L*?
   Thuật toán Thompson đơn giản, dễ cài đặt và không yêu cầu tương tác phức tạp, phù hợp để xây dựng mô hình ban đầu nhanh chóng. Tuy nhiên, mô hình thu được có thể không tối tiểu và cần tối ưu thêm.

3. Làm thế nào để kiểm tra tính chính xác của mô hình xây dựng tự động?
   Tính chính xác được kiểm tra bằng giải thuật Vasilevskii-Chow, so sánh hành vi mô hình với hành vi thực tế của thành phần phần mềm thông qua các chuỗi hành động thực hiện được.

4. Công cụ GenModelTool có thể áp dụng cho các ngôn ngữ lập trình khác nhau không?
   GenModelTool xây dựng mô hình dựa trên hành vi quan sát được, do đó có thể áp dụng cho các thành phần phần mềm viết bằng bất kỳ ngôn ngữ nào, miễn là có thể thu thập được tập các dẫn xuất hành vi.

5. Làm sao để tích hợp mô hình xây dựng tự động vào quy trình phát triển phần mềm hiện tại?
   Mô hình có thể được sử dụng làm đầu vào cho các công cụ kiểm thử tự động và kiểm chứng mô hình, từ đó tích hợp vào quy trình phát triển Agile hoặc DevOps nhằm nâng cao chất lượng và giảm thiểu lỗi phần mềm.

Kết luận

• Luận văn đã nghiên cứu và đề xuất hai phương pháp xây dựng mô hình tự động mô tả chính xác hành vi thành phần phần mềm: thuật toán học L* và thuật toán Thompson.
• Phương pháp học L* cho mô hình tối tiểu và chính xác nhưng khó áp dụng thực tế do chi phí tính toán cao. Thuật toán Thompson đơn giản, dễ cài đặt và đã được phát triển công cụ hỗ trợ GenModelTool.
• Công cụ GenModelTool có ý nghĩa quan trọng trong việc tự động hóa xây dựng mô hình, hỗ trợ kiểm thử tự động và kiểm chứng mô hình, góp phần nâng cao chất lượng phần mềm hướng thành phần.
• Các bước tiếp theo bao gồm hoàn thiện công cụ học L*, tích hợp hai phương pháp, mở rộng ứng dụng công cụ và đào tạo nhân lực chuyên môn.
• Khuyến khích các nhà nghiên cứu, kỹ sư phát triển và kiểm thử phần mềm áp dụng kết quả nghiên cứu để nâng cao hiệu quả phát triển và kiểm thử phần mềm.

Hãy bắt đầu áp dụng các phương pháp xây dựng mô hình tự động để nâng cao chất lượng phần mềm và tối ưu hóa quy trình phát triển ngay hôm nay!

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. LUAN VAN CHAT LUONG download : add [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ó LUAN VAN CHAT LUONG download : add [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. LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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. LUAN VAN CHAT LUONG download : add [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: LUAN VAN CHAT LUONG download : add [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.