Mô Hình Xác Thực Nghiệp Vụ Phần Mềm Theo Hướng Lập Trình Đặc Tả

Luận án tiến sĩ về mô hình xác thực nghiệp vụ phần mềm theo hướng lập trình đặc tả. Nghiên cứu ứng dụng mạng Petri màu và chuỗi luật ECA để nâng cao độ tin cậy.

• Tác giả: Nguyễn Thanh Tuấn
• Người hướng dẫn: PTS. Lê Thành Nhân
• Trường học: Trường Đại học Bách Khoa - Đại học Đà Nẵng
• Chuyên ngành: Khoa Học Máy Tính
• Đề tài: Mô Hình Xác Thực Nghiệp Vụ Phần Mềm Theo Hướng Lập Trình Đặc Tả
• Loại tài liệu: Luận án tiến sĩ
• Năm xuất bản: 2024
• Địa điểm: Đà Nẵng

Mục lục chi tiết

• LỜI CAM ĐOAN
• LỜI CẢM ƠN
• 1. CHƯƠNG 1: TỔNG QUAN QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ
• 1.1. Quy trình nghiệp vụ và mô hình hoá bằng BPMN
• 1.1.1. Quy trình nghiệp vụ
• 1.1.2. Mô hình hóa quy trình nghiệp vụ sử dụng BPMN
• 1.1.3. Quy trình nghiệp vụ và mô hình hoá bằng BPMN
• 1.2. Quy tắc nghiệp vụ và mô hình hoá bằng DMN
• 1.2.1. Định nghĩa Quy tắc nghiệp vụ
• 1.2.2. Mô hình hóa quy tắc nghiệp vụ sử dụng DMN
• 1.2.3. Kết hợp DMN trong mô hình BPMN
• 1.3. Định nghĩa và Cấu trúc Luật ECA
• 1.3.1. Vai trò và Khả năng Thực thi của Luật ECA
• 1.3.2. Ứng dụng và Triển khai Luật ECA
• 1.3.3. Chuỗi luật ECA
• 1.4. Kết luận chương 1
• 2. CHƯƠNG 2: XÁC THỰC QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ
• 2.1. Hình thức hóa quy trình nghiệp vụ
• 2.2. Mạng Petri màu
• 2.3. Mạng Petri màu phân cấp
• 2.4. Hiện trạng nghiên cứu về xác thực quy trình và quy tắc nghiệp vụ
• 2.5. Xác thực quy trình nghiệp vụ
• 2.6. Xác thực quy tắc nghiệp vụ
• 2.7. So sánh các phương pháp
• 2.8. Vòng đời phát triển quy trình và quy tắc nghiệp vụ mở rộng
• 2.9. Kết luận chương 2
• 3. CHƯƠNG 3: XÁC THỰC QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ SỬ DỤNG MẠNG PETRI MÀU
• 3.1. Xác thực quy trình nghiệp vụ với CPN
• 3.2. Đề xuất mô hình xác thực quy trình và quy tắc nghiệp vụ - VeBPRu
• 3.3. Hình thức hóa quy trình và quy tắc nghiệp vụ
• 3.3.1. Các quy tắc chuyển đổi
• 3.3.2. Tích hợp hàm CPN-ML vào mô hình CPN
• 3.3.3. Thuật toán chuyển đổi quy trình và quy tắc nghiệp vụ biểu diễn bằng BPMN/DMN sang CPN
• 3.3.4. Ví dụ minh họa: Quy trình xác nhận đơn hàng
• 3.4. Xác thực quy trình và quy tắc nghiệp vụ với CPN
• 3.4.1. Các yếu tố xác thực
• 3.4.2. Xác thực mô hình CPN
• 3.5. Chuyển đổi mô hình CPN sang chuỗi luật ECA
• 3.5.1. Mô hình CPN-ECA
• 3.5.2. Hình thức hóa quy trình CPN sang chuỗi ECA
• 3.5.3. Ví dụ minh họa
• 3.6. Thử nghiệm và đánh giá
• 3.6.1. Sự cần thiết khi thực hiện Thử nghiệm và Đánh giá mô hình VeBPRu
• 3.6.2. Thiết lập thử nghiệm nền tảng VeBPRu
• 3.6.3. Bộ dữ liệu mô hình thử nghiệm
• 3.6.4. Kết quả thử nghiệm
• 3.7. Kết luận chương 3
• 4. CHƯƠNG 4: XÁC THỰC QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ PHẦN MỀM SỬ DỤNG MẠNG PETRI MÀU PHÂN CẤP
• 4.1. Phân cấp quy trình và quy tắc nghiệp vụ
• 4.1.1. Tính Phân Cấp trong BPMN
• 4.1.2. Tính Phân Cấp trong DMN
• 4.2. Mô hình VeBPRu2: xác thực quy trình và quy tắc nghiệp vụ phân cấp
• 4.3. Hình thức hóa quy trình và quy tắc nghiệp vụ với HCPN
• 4.3.1. Các quy tắc chuyển đổi
• 4.3.2. Thuật toán chuyển đổi BPMN/DMN sang HCPN
• 4.3.3. Phân tích thuật toán
• 4.3.4. Ví dụ minh họa: Quy trình xác nhận đơn hàng
• 4.4. Chuyển đổi mô hình HCPN sang ECA
• 4.4.1. Thuật toán chuyển đổi HCPN sang ECA
• 4.4.2. Ví dụ minh họa
• 4.5. Thử nghiệm và đánh giá
• 4.5.1. Thiết lập thử nghiệm nền tảng VeBPRu2
• 4.5.2. Bộ dữ liệu mô hình thử nghiệm
• 4.5.3. Bộ dữ liệu mô hình thử nghiệm
• 4.5.4. Kết quả thử nghiệm
• 4.5.5. So sánh giữa VeBPRu và VeBPRu2
• 4.6. Kết luận chương 4
• KẾT LUẬN
• CÁC CÔNG TRÌNH KHOA HỌC ĐÃ CÔNG BỐ
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Mô Hình Xác Thực Nghiệp Vụ Phần Mềm Hiện Nay

Trong lĩnh vực công nghệ phần mềm, việc giao tiếp và chuyển giao hiệu quả các yêu cầu giữa chuyên gia ứng dụng và chuyên gia công nghệ thông tin là yếu tố then chốt. Sự tham gia của cả hai bên đảm bảo hiểu đúng nhu cầu ứng dụng và sử dụng công nghệ phù hợp. Lỗi trong giai đoạn thiết kế gây khó khăn và tốn kém ở các giai đoạn sau. Do đó, việc xác định và khắc phục sớm các lỗi này là vô cùng quan trọng. Xu hướng phát triển phần mềm hiện nay là sử dụng các nền tảng low-code, cho phép xây dựng ứng dụng mà không cần nhiều code. Các nền tảng này cung cấp giao diện trực quan, khả năng tùy chỉnh và kết nối dễ dàng. Bên cạnh đó, Quy trình nghiệp vụ được áp dụng như một công cụ mô hình hóa để tăng hiệu quả giao tiếp. Mô hình Quy trình Nghiệp vụ (Business Process Model) là một chuỗi các hoạt động mà một công ty nên thực hiện. Các công cụ như BPMN và DMN đã trở thành nền tảng quan trọng trong việc hỗ trợ trực quan hóa và chuẩn hóa quy trình nghiệp vụ. Tiêu chuẩn Ký hiệu và Mô hình quy trình nghiệp vụ (BPMN), được quản lý bởi tổ chức Object Management Group (OMG), hiện là một trong những công cụ được sử dụng rộng rãi nhất để thiết kế và mô tả các mô hình như vậy

1.1. Vai Trò Của BPMN Trong Mô Hình Hóa Nghiệp Vụ Phần Mềm

BPMN (Business Process Model and Notation) đóng vai trò then chốt trong việc mô hình hóa quy trình nghiệp vụ trong các ứng dụng hướng quy trình (PDA). Nó cung cấp một tiêu chuẩn trực quan để biểu diễn các bước và luồng công việc, tạo điều kiện giao tiếp hiệu quả giữa các bên liên quan. BPMN giúp xác định chức năng và hành vi của hệ thống phần mềm trong quá trình triển khai, đảm bảo rằng ứng dụng đáp ứng chính xác các yêu cầu nghiệp vụ. Nó đóng vai trò quan trọng trong việc xác định chức năng và hành vi của hệ thống phần mềm trong quá trình triển khai. Trong ngữ cảnh này, BPMN được sử dụng làm công cụ chính để mô hình hóa Quy trình nghiệp vụ trong PDA.

Ví dụ minh họa: Hình 1.2 trong tài liệu gốc cung cấp một ví dụ cụ thể về sơ đồ BPMN, thể hiện rõ cấu trúc và các thành phần của một quy trình nghiệp vụ được mô hình hóa.

1.2. Kết Hợp DMN Để Xây Dựng Quy Tắc Nghiệp Vụ Linh Hoạt

DMN (Decision Model and Notation) là tiêu chuẩn để mô hình hóa các quy tắc nghiệp vụ, cho phép phân biệt rõ ràng giữa quy trình và quy tắc. DMN tích hợp các điều kiện và hành động cần thực hiện khi một sự kiện xảy ra, giúp hệ thống phần mềm phản ứng linh hoạt với các thay đổi. Tiêu chuẩn Ký hiệu và Mô hình Quyết định (DMN) được tích hợp để mô hình hóa các quy tắc nghiệp vụ [3]. Trong bối cảnh phát triển phần mềm hiện đại, việc kết nối giữa người sử dụng (chuyên gia nghiệp vụ) và nhà phát triển phần mềm không chỉ giúp giảm thiểu sai sót trong thiết kế mà còn đảm bảo rằng các hệ thống phần mềm được xây dựng đáp ứng chính xác nhu cầu nghiệp vụ.

Ví dụ minh họa: Hình 1.10 trong tài liệu gốc cho thấy cách DMN được kết hợp trong BPMN, minh họa sự tương tác giữa quy trình và quy tắc.

II. Thách Thức Trong Xác Thực Quy Trình Quy Tắc Nghiệp Vụ

BPMN và DMN tuy cung cấp khả năng trực quan hóa và chuẩn hóa quy trình nghiệp vụ, nhưng lại thiếu khả năng tích hợp và xác thực tự động, đặc biệt trong các hệ thống phức tạp. Khoảng trống này làm tăng nguy cơ sai sót trong quá trình triển khai phần mềm và là một thách thức lớn đối với doanh nghiệp. Cần có một phương pháp hình thức để xác thực đồng thời quy trình và quy tắc nghiệp vụ, đáp ứng nhu cầu thực tiễn và nâng cao hiệu quả phát triển phần mềm. Hiện chưa có phương pháp hình thức nào mô tả cả quy trình nghiệp vụ và các quy tắc đi kèm, dẫn đến sự hiểu lầm trong quá trình mô hình hóa và triển khai ứng dụng. Quá trình xác thực liên tục trong vòng đời phát triển quy trình và quy tắc nghiệp vụ chưa được quan tâm đúng mức, làm tăng rủi ro và chi phí.

2.1. Sự Thiếu Hụt Phương Pháp Hình Thức Hóa Đồng Bộ

Hiện chưa có phương pháp hình thức nào được đề xuất để mô tả cả quy trình nghiệp vụ và các quy tắc đi cùng. Thiếu sự kết hợp này có thể dẫn đến sự hiểu lầm hoặc nhầm lẫn trong quá trình mô hình hóa, và có thể tạo ra những tác động tiêu cực lớn khi triển khai các ứng dụng từ mô hình sang môi trường thực tế. Ví dụ, nếu quy trình nghiệp vụ và các quy tắc không được hình thức hóa một cách đồng bộ, có thể dẫn đến việc bỏ sót các ràng buộc quan trọng hoặc tạo ra các xung đột logic, gây ra lỗi trong quá trình thực thi.

2.2. Xác Thực Liên Tục Trong Vòng Đời Phát Triển Phần Mềm

Quá trình xác thực liên tục trong vòng đời phát triển quy trình và quy tắc nghiệp vụ chưa nhận được sự quan tâm đầy đủ. Việc xác thực mô hình cung cấp thông tin về độ chính xác của cả lỗi hoạt động và cấu trúc trong mô hình. Khi cả quy trình và quy tắc nghiệp vụ được xác thực, điều này giúp giảm thời gian, chi phí và rủi ro liên quan đến triển khai các ứng dụng dựa trên quy trình. Nếu việc xác thực chỉ được thực hiện ở giai đoạn cuối của quá trình phát triển, việc phát hiện và sửa chữa lỗi sẽ tốn kém hơn rất nhiều so với việc xác thực liên tục trong suốt vòng đời.

III. Mạng Petri Màu Giải Pháp Xác Thực Quy Trình Nghiệp Vụ Hiệu Quả

Luận án này đề xuất sử dụng Mạng Petri màu (CPN) như một phương pháp hình thức để đặc tả và xác thực các quy trình nghiệp vụ và các quy tắc nghiệp vụ phần mềm. Mạng Petri màu cho phép mô hình hóa các quy trình và quy tắc một cách trực quan và chính xác. Các phương pháp mới để chuyển đổi các mô hình BPMN và DMN thành các mô hình CPN có khả năng bao hàm cả quy trình và quy tắc nghiệp vụ cũng được đề xuất. CPN-ML được sử dụng để tích hợp các hàm và logic vào mô hình CPN, tăng cường khả năng biểu diễn và xác thực.

3.1. Chuyển Đổi BPMN DMN Sang CPN Cách Tiếp Cận Mới

Luận án đề xuất các phương pháp mới để chuyển đổi các mô hình BPMN và DMN thành các mô hình CPN và HCPN có khả năng bao hàm cả quy trình và quy tắc nghiệp vụ. Phương pháp mới này sẽ phải xử lý các thách thức khác nhau, bao gồm cách thức biểu diễn quy tắc nghiệp vụ trong các mô hình CPN và HCPN, cách thức chuyển đổi các quy tắc nghiệp vụ từ các mô hình BPMN và DMN sang các mô hình CPN và HCPN tương ứng. Nghiên cứu sẽ tập trung vào việc phát triển các giải thuật và phương pháp để giải quyết các thách thức này.

3.2. Tích Hợp CPN ML Để Xử Lý Quy Tắc Nghiệp Vụ Phức Tạp

Việc tích hợp hàm CPN-ML vào mô hình CPN giúp xử lý các quy tắc nghiệp vụ phức tạp. CPN-ML cho phép định nghĩa các hàm và logic để xác thực và thực thi các quy tắc, đảm bảo tính chính xác và nhất quán của hệ thống. Nghiên cứu sẽ tập trung vào việc phát triển một 5 phương pháp mới để chuyển đổi các mô hình CPN và HCPN thành các bộ luật ECA có thể kiểm tra và xác thực. Phương pháp mới sẽ tập trung vào việc tạo ra các bộ luật ECA từ các mô hình CPN và HCPN bằng cách sử dụng các thuật toán và kỹ thuật chuyển đổi mô hình.

3.3. Thuật Toán Chuyển Đổi Quy Trình Nghiệp Vụ Biểu Diễn Bằng BPMN DMN Sang CPN

Luận án cung cấp các quy tắc chuyển đổi từ các mô hình BPMN và DMN thành các mô hình CPN, cho phép tự động hóa quá trình chuyển đổi và đảm bảo tính chính xác của mô hình kết quả. Các quy tắc này được thiết kế để xử lý các thành phần khác nhau của BPMN và DMN, bao gồm các hoạt động, các sự kiện, các cổng và các quy tắc quyết định. Hình 3.2 trong tài liệu gốc minh họa mô hình chuyển đổi quy trình và quy tắc nghiệp vụ sang mạng Petri màu.

IV. VeBPRu Mô Hình Xác Thực Quy Trình Quy Tắc Nghiệp Vụ Phần Mềm

Luận án đề xuất mô hình VeBPRu, một phương pháp hình thức để xác thực đồng thời quy trình và quy tắc nghiệp vụ. Mô hình VeBPRu tích hợp CPN và CPN-ML để mô hình hóa và xác thực các quy trình và quy tắc. Nó bao gồm các yếu tố xác thực như tính chính xác, tính nhất quán, tính đầy đủ và tính tuân thủ. Các thuật toán và kỹ thuật để chuyển đổi các mô hình CPN sang chuỗi luật ECA cũng được phát triển để thực thi các quy trình nghiệp vụ đã được xác thực.

4.1. Các Yếu Tố Xác Thực Trong Mô Hình VeBPRu

VeBPRu tập trung vào các yếu tố xác thực như tính chính xác, tính nhất quán, tính đầy đủ và tính tuân thủ của mô hình CPN. Tính chính xác đảm bảo rằng mô hình phản ánh đúng thực tế quy trình nghiệp vụ. Tính nhất quán đảm bảo rằng không có xung đột logic trong mô hình. Tính đầy đủ đảm bảo rằng tất cả các khía cạnh của quy trình đều được mô hình hóa. Tính tuân thủ đảm bảo rằng mô hình tuân thủ các quy tắc và tiêu chuẩn nghiệp vụ. Các yếu tố này được xác thực thông qua phân tích không gian trạng thái và kiểm tra mô hình.

4.2. Chuyển Đổi Mô Hình CPN Sang Chuỗi Luật ECA Để Thực Thi

Luận án phát triển các thuật toán và kỹ thuật để chuyển đổi các mô hình CPN sang chuỗi luật ECA. Các chuỗi luật ECA cho phép kiểm tra và thực thi các hành động được kích hoạt bởi các sự kiện và điều kiện. Việc sử dụng ECA cho phép hệ thống phản ứng nhanh chóng với các sự kiện xảy ra, duy trì tính linh hoạt và khả năng mở rộng trong các hệ thống lớn. Mô hình CPN-ECA được sử dụng để biểu diễn mối quan hệ giữa các trạng thái CPN và các luật ECA.

Hình 3.8 trong tài liệu gốc minh họa mô hình CPN-ECA.

V. VeBPRu2 Xác Thực Quy Trình Quy Tắc Nghiệp Vụ Phân Cấp

Mô hình VeBPRu2 được đề xuất, mở rộng VeBPRu bằng cách sử dụng mạng Petri màu phân cấp (HCPN). VeBPRu2 cho phép mô hình hóa và xác thực các quy trình và quy tắc nghiệp vụ phức tạp có cấu trúc phân cấp. Việc sử dụng HCPN giúp giảm độ phức tạp của mô hình và tăng khả năng quản lý. Các thuật toán và kỹ thuật để chuyển đổi các mô hình HCPN sang chuỗi luật ECA cũng được phát triển để thực thi các quy trình nghiệp vụ phân cấp.

5.1. Tính Phân Cấp Trong BPMN Và DMN Cho Mô Hình VeBPRu2

VeBPRu2 tận dụng tính phân cấp trong BPMN và DMN để mô hình hóa các quy trình nghiệp vụ phức tạp. Các quy trình và quy tắc được chia thành các mô-đun nhỏ hơn, dễ quản lý hơn, cho phép xác thực và bảo trì hiệu quả hơn. Bảng 4.1 trong tài liệu gốc thể hiện chuyển đổi Quy trình con.

5.2. Ưu Điểm Của Việc Sử Dụng HCPN Trong Mô Hình VeBPRu2

HCPN giúp giảm độ phức tạp của mô hình và tăng khả năng quản lý. Các quy trình và quy tắc nghiệp vụ được tổ chức thành các mô-đun phân cấp, cho phép các nhà phát triển tập trung vào các thành phần cụ thể của hệ thống. HCPN cũng cho phép tái sử dụng các mô-đun đã được xác thực, giảm thời gian và chi phí phát triển. Bảng 4.6 trong tài liệu gốc so sánh giữa VeBPRu và VeBPRu2.

5.3. Chuyển Đổi HCPN sang ECA trong Mô Hình VeBPRu2

Luận án phát triển các thuật toán và kỹ thuật để chuyển đổi các mô hình HCPN sang chuỗi luật ECA. Các chuỗi luật ECA cho phép kiểm tra và thực thi các hành động được kích hoạt bởi các sự kiện và điều kiện. Việc sử dụng ECA cho phép hệ thống phản ứng nhanh chóng với các sự kiện xảy ra, duy trì tính linh hoạt và khả năng mở rộng trong các hệ thống lớn. Bảng 4.5 trong tài liệu gốc thể hiện Thời gian chuyển đổi sang ECA từ mô hình HCPN.

VI. Kết Luận Hướng Phát Triển Xác Thực Nghiệp Vụ Phần Mềm

Luận án đã đề xuất các phương pháp hình thức để đặc tả và xác thực các quy trình nghiệp vụ và quy tắc nghiệp vụ phần mềm sử dụng Mạng Petri màu và mạng Petri màu phân cấp. Mô hình VeBPRu và VeBPRu2 đã được chứng minh là hiệu quả trong việc xác thực các quy trình và quy tắc phức tạp. Các kết quả nghiên cứu này có ý nghĩa khoa học và thực tiễn quan trọng, góp phần nâng cao chất lượng và độ tin cậy của phần mềm.

6.1. Tóm Tắt Các Đóng Góp Chính Của Nghiên Cứu

Nghiên cứu đã đóng góp vào việc phát triển các phương pháp hình thức để đặc tả và xác thực các quy trình và quy tắc nghiệp vụ phần mềm. Các phương pháp này cho phép mô hình hóa và xác thực các quy trình phức tạp một cách chính xác và hiệu quả. Nghiên cứu cũng đã phát triển các thuật toán và kỹ thuật để chuyển đổi các mô hình CPN và HCPN sang chuỗi luật ECA, cho phép thực thi các quy trình nghiệp vụ đã được xác thực.

6.2. Các Hướng Nghiên Cứu Tiềm Năng Trong Tương Lai

Trong tương lai, nghiên cứu có thể tập trung vào việc mở rộng các mô hình VeBPRu và VeBPRu2 để hỗ trợ các loại quy trình nghiệp vụ phức tạp hơn, chẳng hạn như các quy trình có tính phân tán cao hoặc các quy trình yêu cầu sự tương tác giữa nhiều hệ thống. Nghiên cứu cũng có thể tập trung vào việc phát triển các công cụ hỗ trợ tự động hóa quá trình xác thực và thực thi các quy trình nghiệp vụ.

Nội dung chính

Tổng quan luận án

Trong kỹ nghệ phần mềm hiện đại, việc đảm bảo tính nhất quán và chính xác giữa yêu cầu nghiệp vụ của các chuyên gia miền ứng dụng và thiết kế kỹ thuật của kỹ sư công nghệ thông tin là yếu tố mang tính quyết định. Sự phát triển của các ứng dụng hướng quy trình (Process-Driven Applications - PDA) và các nền tảng lập trình ít viết mã (low-code) như Microsoft Power Platform hay Appian đã đưa mô hình quy trình nghiệp vụ trở thành thành phần cốt lõi trong kiến trúc hệ thống. Hai tiêu chuẩn quốc tế được công nhận rộng rãi bởi Object Management Group (OMG) là BPMN (Business Process Model and Notation) để mô hình hóa luồng quy trình và DMN (Decision Model and Notation) để đặc tả các quy tắc và quyết định nghiệp vụ.

Tuy nhiên, BPMN và DMN về bản chất là các ngôn ngữ bán hình thức (semi-formal), thiếu các cơ chế tích hợp chặt chẽ và công cụ xác thực tự động. Lỗi xuất hiện trong giai đoạn thiết kế nếu không được phát hiện sớm sẽ dẫn đến chi phí khắc phục cao và rủi ro lớn khi triển khai trên môi trường thực tế. Văn bản luận án chỉ ra hai khoảng trống nghiên cứu chính:

1. Vấn đề 1: Thiếu phương pháp hình thức hóa thống nhất có khả năng mô tả đồng thời cả quy trình nghiệp vụ (BPMN) và các quy tắc nghiệp vụ đi kèm (DMN). Việc tách rời hai thành phần này dễ gây sai lệch ngữ nghĩa khi chuyển giao từ thiết kế sang môi trường thực thi.
2. Vấn đề 2: Quy trình xác thực liên tục trong toàn bộ vòng đời phát triển quy trình và quy tắc nghiệp vụ chưa nhận được sự quan tâm đầy đủ, dẫn đến việc thiếu hụt các công cụ kiểm tra tự động các lỗi hoạt động và cấu trúc mô hình.

Mục tiêu nghiên cứu của luận án được xác định rõ qua 3 nhiệm vụ cụ thể:

1. Đánh giá các phương pháp và công cụ hiện có về mô hình hóa và xác thực quy trình, quy tắc nghiệp vụ (BPMN, DMN, CPN, HCPN, ECA).
2. Phát triển phương pháp mới để hình thức hóa quy trình và quy tắc nghiệp vụ bằng cách chuyển đổi từ BPMN và DMN sang mạng Petri màu (CPN) và mạng Petri màu phân cấp (HCPN).
3. Đề xuất kỹ thuật, thuật toán và công cụ hỗ trợ xác thực đồng thời quy trình và quy tắc nghiệp vụ trên mô hình hình thức hóa, sau đó chuyển đổi mô hình đã xác thực sang chuỗi luật Event-Condition-Action (ECA) để thực thi.

Đối tượng nghiên cứu của đề tài bao gồm các tiêu chuẩn mô hình hóa BPMN, DMN; các mô hình hình thức mạng Petri, CPN, HCPN; cấu trúc luật ECA và các kỹ thuật phân tích không gian trạng thái (state space analysis). Phạm vi nghiên cứu tập trung vào sơ đồ quy trình nghiệp vụ đơn lẻ trong BPMN (Process Diagram), bảng quyết định DMN cấp độ logic (Decision Logic Level - DLL) và sơ đồ yêu cầu quyết định (Decision Requirements Diagram - DRD) sử dụng chính sách trúng duy nhất (Unique hit policy), cùng kỹ thuật ánh xạ sang CPN/HCPN và chuỗi luật ECA để kiểm tra tính đúng đắn cấu trúc và hành vi.

---

Tổng quan tài liệu và vị trí của luận án

Luận án đã khảo cứu có hệ thống các công trình nghiên cứu và chuẩn mô hình hóa trong quản trị quy trình nghiệp vụ và công nghệ phần mềm:

• Các ngôn ngữ mô hình hóa quy trình: Event-driven Process Chain (EPC) tập trung vào sự kiện và chức năng; Unified Modeling Language (UML) với Activity Diagram và Use Case Diagram; Semantics of Business Vocabulary and Business Rules (SBVR) cung cấp khung ngữ nghĩa cho thuật ngữ và quy tắc; BPMN (OMG) chuẩn hóa ký hiệu đồ họa cho luồng quy trình nghiệp vụ; DMN (OMG) chuẩn hóa mô hình quyết định.
• Lý thuyết mạng Petri và kiểm tra mô hình: Mạng Petri cổ điển do Carl Adam Petri phát minh; Mạng Petri màu (CPN) và Mạng Petri màu phân cấp (HCPN) do Jensen và Kristensen phát triển, cho phép gắn nhãn dữ liệu (token màu) và cấu trúc hóa module; Các kỹ thuật kiểm tra mô hình sử dụng logic nhánh tính toán (Computation Tree Logic - CTL) và framework bPERFECT để tự động hóa kiểm thử quy trình.
• Hệ thống quy tắc và cơ sở dữ liệu động: Cấu trúc luật Event-Condition-Action (ECA) được Dayal và Widom nghiên cứu trong Active Database Management Systems (ADBMS), cùng các biến thể mở rộng như ECATRTE nhằm kiểm soát các ràng buộc thời gian và sự kiện lặp lại.
• Công cụ và nền tảng hỗ trợ: Bộ API DMN của Camunda phục vụ thực thi quy tắc quyết định trong hệ thống quản lý quy trình.

Phương pháp / Ngôn ngữ	Khả năng biểu diễn quy trình	Khả năng biểu diễn quy tắc	Năng lực xác thực hình thức	Khả năng thực thi tự động
BPMN thuần túy	Cao (Luồng công việc)	Thấp (Phụ thuộc Gateway)	Thấp (Bán hình thức)	Trung bình (Cần BPM Engine)
DMN thuần túy	Không hỗ trợ	Cao (Bảng quyết định/DRD)	Trung bình (Kiểm tra logic bảng)	Cao (Rule Engine)
Mạng Petri cổ điển	Trung bình (Luồng điều khiển)	Thấp (Không có kiểu dữ liệu)	Rất cao (Toán học chặt chẽ)	Thấp
CPN / HCPN	Cao (Luồng & dữ liệu phức tạp)	Cao (Tích hợp hàm CPN-ML)	Rất cao (Không gian trạng thái)	Trung bình (Qua công cụ CPN)
Chuỗi luật ECA	Trung bình (Chuỗi phản ứng)	Cao (Cặp điều kiện - hành động)	Trung bình (Phân tích chuỗi)	Rất cao (Active Engine)
VeBPRu / VeBPRu2 (Luận án)	Toàn diện (BPMN)	Toàn diện (DMN nhúng)	Toàn diện (CPN/HCPN State Space)	Toàn diện (Chuỗi ECA sinh ra)

Vị trí của luận án: Khác với các nghiên cứu trước đây chỉ giải quyết riêng lẻ xác thực luồng điều khiển BPMN hoặc kiểm tra tính nhất quán trong bảng DMN, luận án xây dựng một chuỗi chuyển đổi khép kín từ mô hình thiết kế cấp cao (BPMN + DMN) sang mô hình hình thức toán học (CPN/HCPN) phục vụ xác thực toàn diện, rồi tự động sinh mã thực thi cấp thấp dưới dạng chuỗi luật ECA.

---

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

Luận án dựa trên nền tảng toán học và kỹ thuật phần mềm với các định nghĩa hình thức:

1. Khung lý thuyết và cấu trúc hình thức

• Đồ thị mạng Petri cơ bản: Là bộ 4 thành phần $(P, T, A, w)$ gồm tập hữu hạn các vị trí $P$, tập hữu hạn các chuyển tiếp $T$, tập các cung $A \subseteq (P \times T) \cup (T \times P)$, và hàm trọng số $w$. Trạng thái mạng xác định bởi đánh dấu $m: P \rightarrow \mathbb{N}$. Chuyển tiếp $t \in T$ khả hoạt khi $\forall p \in {}^\bullet t, m(p) \ge w(p, t)$.
• Mạng Petri màu (CPN): Là bộ $N = (P, T, A, \Sigma, C, N, E, G, I)$ trong đó $\Sigma$ là tập các kiểu màu (colorsets), $C: P \rightarrow \Sigma$ là hàm gán màu cho vị trí, $E$ là hàm biểu thức trên cung, $G$ là hàm biểu thức canh (guard function) trả về giá trị Boolean trên chuyển tiếp, và $I$ là hàm khởi tạo đánh dấu.
• Mạng Petri màu phân cấp (HCPN): Được tổ chức thành các module CPN $\Sigma_M = (\Sigma, T_{sub}, P_{port}, PT)$, trong đó $T_{sub}$ là tập các chuyển tiếp thay thế (substitution transitions) đại diện cho quy trình con, $P_{port}$ là tập các vị trí cổng kết nối (port places), và $PT$ là hàm xác định loại cổng (In, Out, InOut).
• Sơ đồ Yêu cầu Quyết định (DRD): Bộ 4 thành phần $(N, IR, T, f)$ với $N = D \cup f$ (tập nút quyết định và dữ liệu đầu vào), $IR \subset N \times N$ là tập cạnh quan hệ thông tin không chu trình, $T$ là tập tên gọi, và $f: N \rightarrow T$ là hàm ánh xạ tên.
• Bảng quyết định DMN (DLL): Bộ $(T, I, O, Type, R, Order, H)$ với $I, O$ là tập thuộc tính vào/ra, $Type$ gán kiểu dữ liệu, $R = {r_1, r_2, \dots}$ là tập quy tắc $\langle If_i, Then_i \rangle$ viết bằng ngôn ngữ FEEL/S-FEEL, $Order$ là hàm thứ tự ưu tiên, và $H$ là chỉ số trúng ($H \in {u, f, c}$, luận án sử dụng $u$ - Unique).
• Luật và Chuỗi luật ECA: Luật đơn lẻ $ECA = (E, C, A)$ kích hoạt hành động $A$ khi sự kiện $E$ xuất hiện và điều kiện $C$ thỏa mãn: $$ECA(E, C, A) = \begin{cases} \text{Thực hiện } A & \text{khi } E \text{ xảy ra và } C = \text{True} \ \text{Không thực hiện} & \text{trường hợp khác} \end{cases}$$ Chuỗi luật ECA được định nghĩa là một dãy liên kết $Chain(ECA_1, ECA_2, \dots, ECA_n)$, trong đó hành động $A_i$ của $ECA_i$ kích hoạt sự kiện $E_{i+1}$ của $ECA_{i+1}$.

2. Phương pháp nghiên cứu và công cụ kỹ thuật

Phương pháp luận của nghiên cứu gồm hai trục chính:

1. Hình thức hóa và Xác thực: Chuyển đổi các phần tử đồ họa của BPMN (Task, Event, Gateway, Data Object, Subprocess) và bảng quyết định DMN thành các vị trí, chuyển tiếp, biểu thức cung và hàm CPN-ML (ngôn ngữ lập trình chức năng của CPN Tools). Xác thực tính đúng đắn mô hình thông qua kiểm tra tính đầy đủ, tính không xung đột, tính đạt được (reachability), tính sống (liveness) và phát hiện bế tắc (deadlock) bằng kỹ thuật phân tích không gian trạng thái.
2. Thực thi hóa: Phát triển thuật toán ánh xạ cấu trúc CPN/HCPN đã qua xác thực sang tập chuỗi luật ECA để chạy trên các engine quy tắc nghiệp vụ.

Nguồn dữ liệu thực nghiệm bao gồm 3 bộ dữ liệu mô hình quy trình: Bộ dữ liệu 1 (các quy trình nghiệp vụ chuẩn có tích hợp bảng quyết định), Bộ dữ liệu 2 (các mô hình phức tạp với số lượng phần tử tăng dần), và Bộ dữ liệu 3 (các mô hình quy trình có cấu trúc phân cấp đa tầng). Các ca nghiên cứu thực tế gồm có Quy trình xác nhận đơn hàng (Order Confirmation), Quy trình thanh toán (Payment Business), Hệ thống Mua sắm Trực tuyến (Online Shopping), và Quy trình điều khiển máy lạnh theo nhiệt độ.

---

Nội dung chính theo từng chương

Chương 1: Tổng quan quy trình và quy tắc nghiệp vụ

Chương này hệ thống hóa các khái niệm nền tảng về Quản lý Quy trình Nghiệp vụ (BPM) và phân tích 4 giai đoạn trong vòng đời phát triển quy trình nghiệp vụ:

• Thiết kế (Design): Xác định phạm vi, mục tiêu, các bên liên quan và xây dựng mô hình quy trình đồ họa.
• Triển khai (Implementation): Hiện thực hóa mô hình vào tổ chức hoặc cấu hình trên hệ thống công nghệ thông tin.
• Kiểm soát (Control): Vận hành quy trình trong môi trường thực và thu thập dữ liệu giám sát thời gian thực.
• Phân tích (Analysis): Đối chiếu dữ liệu thực thi với thiết kế, phát hiện các điểm nghẽn và sai lệch để tối ưu hóa.

Chương 1 đi sâu phân tích tiêu chuẩn BPMN với các thành phần cốt lõi: Hồ bơi (Pool), Hoạt động (Activity/Task/Subprocess), Kết nối (Sequence Edge, Message Edge), Cổng phân nhánh/kết hợp (Gateway: Exclusive, Parallel, Inclusive), Sự kiện (Start, Intermediate, End Event), và Đối tượng dữ liệu (Data Objects, Data Store). Tiếp đó, chương phân tích tiêu chuẩn DMN với hai cấp độ trừu tượng: Sơ đồ Yêu cầu Quyết định (DRD) và Bảng Quyết định (DLL) sử dụng biểu thức FEEL/S-FEEL. Luận án minh họa lợi ích của việc tích hợp DMN qua tác vụ Business Rule Task: thay vì sử dụng các Gateway phức tạp với nhiều nhánh rẽ rối rắm trong BPMN (như ví dụ điều khiển máy lạnh theo nhiệt độ phòng), việc nhúng DMN giúp tách biệt và trừu tượng hóa logic quyết định thành bảng quyết định độc lập, nâng cao khả năng bảo trì. Cuối cùng, chương giới thiệu cú pháp ON Event IF Condition DO Action của luật ECA và cơ chế liên kết chuỗi luật ECA phục vụ thực thi quy trình.

Chương 2: Xác thực quy trình và quy tắc nghiệp vụ

Chương 2 phân tích hiện trạng các kỹ thuật xác thực quy trình và quy tắc nghiệp vụ, làm rõ cơ sở toán học của Mạng Petri, Mạng Petri màu (CPN) và Mạng Petri màu phân cấp (HCPN). Tác giả chỉ ra rằng mạng Petri truyền thống gặp hạn chế lớn khi không thể mô hình hóa luồng dữ liệu phức tạp và quy tắc logic do chỉ có một loại token không phân biệt. CPN khắc phục nhược điểm này bằng cách hỗ trợ token màu và biểu thức gác (guard expression).

Từ việc so sánh ưu nhược điểm của các phương pháp hiện hành, luận án đề xuất một mô hình "Vòng đời phát triển quy trình và quy tắc nghiệp vụ mở rộng". Mô hình mở rộng này bổ sung giai đoạn Xác thực hình thức (Formal Verification) vào ngay sau giai đoạn Thiết kế và trước giai đoạn Triển khai. Việc chèn thêm pha xác thực cho phép phân tích không gian trạng thái, phát hiện sớm các lỗi cấu trúc (deadlock, livelock, nhánh không thể đạt tới) và lỗi logic nghiệp vụ (mâu thuẫn quy tắc, thiếu trường hợp trong bảng quyết định), từ đó ngăn ngừa các sai sót lan truyền sang pha vận hành.

Chương 3: Xác thực quy trình và quy tắc nghiệp vụ sử dụng mạng Petri màu

Chương này trình bày mô hình VeBPRu (Verification Business Process and Business Rules Model) — giải pháp hình thức hóa và xác thực đồng thời BPMN và DMN bằng CPN phẳng.

Nội dung trọng tâm gồm:

1. Tập quy tắc chuyển đổi (Mapping Rules):
   • Tác vụ BPMN (Task) chuyển đổi thành chuyển tiếp CPN kèm vị trí đầu vào/đầu ra.
   • Luồng tuần tự (Sequence Flow) chuyển thành cung CPN.
   • Cổng Exclusive, Parallel chuyển đổi thành các cấu trúc rẽ nhánh/hợp nhất tương ứng trong CPN.
   • Đối tượng dữ liệu (Data Object) chuyển thành vị trí chứa token có kiểu màu tương ứng kiểu dữ liệu XML Schema.
   • Bảng quyết định DMN trong Business Rule Task được chuyển đổi thành hàm CPN-ML tương ứng, với đầu vào là các tham số của bảng và đầu ra là giá trị quyết định. Biểu thức cung và biểu thức gác sử dụng hàm CPN-ML này để điều khiển việc bắn token.
2. Mô hình CPN-ECA: Thuật toán duyệt qua cấu trúc đồ thị CPN đã được xác thực để sinh tự động tập các luật ECA, trong đó sự kiện $E$ tương ứng với sự xuất hiện token tại vị trí vào, điều kiện $C$ là biểu thức gác của chuyển tiếp, và hành động $A$ là việc tiêu thụ/tạo mới token tại vị trí ra.
3. Chuỗi công cụ và Thử nghiệm thực chứng:
   • Xây dựng chuỗi công cụ VeBPRu tích hợp với CPN Tools.
   • Thử nghiệm trên ca nghiên cứu "Quy trình xác nhận đơn hàng" (Order Confirmation Process) có quy tắc tính chiết khấu (Discount Rules) và hệ thống Mua sắm Trực tuyến (Online Shopping - Order Business).
   • Đánh giá định lượng trên Bộ dữ liệu mô hình 1 và Bộ dữ liệu mô hình 2: Đo lường thời gian chuyển đổi từ BPMN/DMN sang CPN, tỷ lệ phát hiện lỗi không gian trạng thái, và thời gian sinh chuỗi luật ECA theo quy mô số lượng phần tử.

Chương 4: Xác thực quy trình và quy tắc nghiệp vụ phần mềm sử dụng mạng Petri màu phân cấp

Chương 4 mở rộng mô hình VeBPRu lên quy mô hệ thống phức tạp thông qua mô hình VeBPRu2, ứng dụng Mạng Petri màu phân cấp (HCPN).

1. Xử lý tính phân cấp: Phân tích cấu trúc phân cấp trong BPMN (Subprocess lồng nhau) và tính phân cấp trong DMN (DRD nhiều tầng quyết định phụ thuộc).
2. Hình thức hóa với HCPN: Đề xuất thuật toán chuyển đổi BPMN Subprocess thành Chuyển tiếp thay thế ($T_{sub}$) và ánh xạ các biến dữ liệu qua lại giữa mô hình cha và mô hình con thông qua các Vị trí cổng ($P_{port}$: In-port, Out-port, InOut-port). Tác vụ thanh toán (Payment Business) trong hệ thống Order Business được minh họa chi tiết dưới dạng module con của HCPN.
3. Thuật toán chuyển đổi HCPN sang ECA: Thiết lập thuật toán đệ quy xử lý các module con để tạo ra cây chuỗi luật ECA hoàn chỉnh, bảo toàn tính thứ bậc và phụ thuộc dữ liệu.
4. Thử nghiệm và So sánh VeBPRu với VeBPRu2:
   • Thử nghiệm trên Bộ dữ liệu mô hình 3 gồm các quy trình nghiệp vụ phân cấp quy mô lớn.
   • Kết quả so sánh cho thấy: Đối với các mô hình phức tạp, VeBPRu2 giảm thiểu sự bùng nổ không gian trạng thái (state space explosion), rút ngắn đáng kể thời gian phân tích và xác thực mô hình so với VeBPRu phẳng, đồng thời giữ cho cấu trúc mô hình trực quan, dễ quản lý theo module.

---

Kết quả và những đóng góp mới

Luận án đã đạt được các kết quả khoa học và thực tiễn chính:

1. Đóng góp về mặt lý luận và khoa học

• Đề xuất phương pháp hình thức hóa tích hợp, kết hợp thành công BPMN, DMN, Mạng Petri màu (CPN/HCPN) và chuỗi luật ECA trong một khung làm việc thống nhất.
• Mở rộng lý thuyết ứng dụng của Mạng Petri màu trong kỹ nghệ phần mềm bằng cách tích hợp trực tiếp logic bảng quyết định DMN thông qua các hàm ngôn ngữ chức năng CPN-ML, giải quyết bài toán xác thực đồng thời luồng điều khiển và ràng buộc dữ liệu nghiệp vụ.
• Thiết lập quy tắc toán học và thuật toán chuyển đổi từ mô hình hình thức CPN/HCPN sang chuỗi luật phản ứng ECA, bắc cầu nối giữa giai đoạn kiểm tra mô hình toán học và giai đoạn thực thi hệ thống.
• Bổ sung giai đoạn xác thực hình thức vào vòng đời phát triển quy trình nghiệp vụ (BPM Lifecycle mở rộng), cung cấp cơ sở lý thuyết cho việc kiểm soát chất lượng phần mềm ở giai đoạn thiết kế sớm.

2. Đóng góp về mặt thực tiễn và giải pháp công nghệ

• Xây dựng hoàn chỉnh hai chuỗi công cụ thực nghiệm: nền tảng VeBPRu (cho mô hình CPN phẳng) và nền tảng VeBPRu2 (cho mô hình HCPN phân cấp).
• Cung cấp giải pháp kỹ thuật tự động hóa toàn bộ quy trình: nhập mô hình BPMN/DMN (chuẩn XML/XSD) $\rightarrow$ chuyển đổi sang CPN/HCPN $\rightarrow$ chạy kiểm tra không gian trạng thái phát hiện lỗi $\rightarrow$ xuất tập luật ECA sẵn sàng tích hợp vào các công cụ quy tắc (rule engines) và nền tảng low-code.
• Chứng minh tính khả thi và hiệu năng thông qua thực nghiệm trên các bài toán thực tế (hệ thống đặt hàng trực tuyến, quy trình thanh toán, bài toán điều khiển môi trường), giúp doanh nghiệp giảm thiểu rủi ro triển khai và chi phí sửa lỗi phần mềm.

---

Hạn chế và hướng nghiên cứu tiếp

Dựa trên phạm vi và nội dung trình bày trong văn bản luận án:

• Hạn chế về phạm vi mô hình hóa: Luận án tập trung vào sơ đồ quy trình nghiệp vụ đơn lẻ (Process Diagram) trong BPMN, chưa mở rộng sang toàn bộ các sơ đồ hợp tác phức tạp đa tổ chức (Collaboration, Choreography Diagrams) có nhiều luồng thông điệp bất đồng bộ đan xen.
• Hạn chế về chính sách quyết định: Về phía DMN, nghiên cứu tập trung sâu vào bảng quyết định với chính sách trúng duy nhất (Unique hit policy), các chính sách trúng phức tạp khác như Collect hay First chưa được bao phủ toàn diện trong thuật toán ánh xạ tự động.
• Vấn đề bùng nổ không gian trạng thái: Dù HCPN trong VeBPRu2 đã cải thiện đáng kể hiệu năng phân tích, việc kiểm tra không gian trạng thái đối với các hệ thống quy mô cực lớn với không gian dữ liệu vô hạn vẫn là một thách thức tính toán.
• Hướng nghiên cứu tiếp:
  1. Mở rộng thuật toán chuyển đổi cho các dạng biểu đồ BPMN/DMN còn lại và hỗ trợ toàn bộ các chính sách trúng (Hit Policies) của DMN.
  2. Tích hợp chuỗi luật ECA sinh ra vào các engine thực thi quy trình mã nguồn mở thời gian thực để đánh giá hiệu năng vận hành trực tiếp.
  3. Phát triển các kỹ thuật tối ưu hóa không gian trạng thái nâng cao cho HCPN khi xử lý dữ liệu quy mô lớn.

---

Giá trị tham khảo

Luận án là tài liệu tham khảo chuyên sâu trong các lĩnh vực:

• Đối với nghiên cứu sinh và nhà nghiên cứu: Cung cấp phương pháp luận chặt chẽ về hình thức hóa phần mềm (formal methods), kỹ thuật ánh xạ mô hình bán hình thức sang mô hình toán học (CPN/HCPN), và phương pháp phân tích không gian trạng thái. Nội dung Chương 2, 3, 4 là tài liệu giá trị về lý thuyết mạng Petri ứng dụng.
• Đối với giảng viên và cơ sở đào tạo: Là tài liệu tham khảo phục vụ giảng dạy các môn học sau đại học như: Kỹ nghệ phần mềm nâng cao, Quản lý quy trình nghiệp vụ (BPM), Phương pháp hình thức trong công nghệ phần mềm, và Kiểm thử & Xác thực hệ thống.
• Đối với kỹ sư phần mềm, kiến trúc sư hệ thống và nhà phát triển nền tảng Low-Code: Cung cấp giải pháp kiến trúc và thuật toán chi tiết để xây dựng module xác thực thiết kế quy trình tự động, giúp nâng cao độ tin cậy của các hệ thống PDA trong các lĩnh vực tài chính, thương mại điện tử, logistics và y tế.

---

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

1. Tại sao luận án lại chọn kết hợp BPMN và DMN thay vì chỉ sử dụng một mình BPMN?

Trả lời: BPMN là tiêu chuẩn mô hình hóa luồng quy trình nhưng khi gặp các quy tắc nghiệp vụ phức tạp, BPMN buộc phải sử dụng các cổng rẽ nhánh (Gateway) đan xen dày đặc, làm sơ đồ trở nên rối rắm và khó bảo trì. Việc tích hợp DMN thông qua Business Rule Task giúp tách biệt hoàn toàn logic quyết định ra khỏi luồng điều khiển, biểu diễn chúng dưới dạng bảng quyết định rõ ràng và độc lập.

2. Mô hình VeBPRu trong Chương 3 giải quyết bài toán xác thực bằng cơ chế nào?

Trả lời: VeBPRu chuyển đổi sơ đồ BPMN thành cấu trúc đồ thị CPN và chuyển đổi bảng quyết định DMN thành các hàm CPN-ML nhúng trực tiếp vào chuyển tiếp CPN. Sau đó, mô hình sử dụng kỹ thuật phân tích không gian trạng thái (state space analysis) của CPN Tools để kiểm tra tính đúng đắn cấu trúc và hành vi, bao gồm việc phát hiện bế tắc (deadlock), vòng lặp vô hạn, tính sống (liveness), và các trạng thái không thể đạt tới.

3. Sự khác biệt cốt lõi giữa mô hình VeBPRu (Chương 3) và VeBPRu2 (Chương 4) là gì?

Trả lời: VeBPRu áp dụng mạng Petri màu phẳng (CPN), phù hợp với các quy trình đơn lẻ mức độ vừa phải nhưng dễ gặp hiện tượng bùng nổ không gian trạng thái khi quy mô tăng. VeBPRu2 sử dụng Mạng Petri màu phân cấp (HCPN), cho phép mô hình hóa các quy trình con (Subprocess) và DRD nhiều tầng thành các module phân cấp thông qua Chuyển tiếp thay thế ($T_{sub}$) và Vị trí cổng ($P_{port}$), giúp giảm đáng kể thời gian xác thực và tối ưu bộ nhớ.

4. Vai trò của chuỗi luật ECA trong kiến trúc tổng thể của luận án là gì?

Trả lời: Chuỗi luật ECA đóng vai trò là cầu nối thực thi. Sau khi mô hình CPN/HCPN được xác thực là không có lỗi, thuật toán chuyển đổi sẽ tự động sinh ra tập luật theo cú pháp ON Event IF Condition DO Action. Cấu trúc này giúp quy trình nghiệp vụ đã xác thực có thể triển khai và thực thi trực tiếp, tự động trên các hệ thống cơ sở dữ liệu động và engine quy tắc hiện đại mà không cần lập trình lại từ đầu.

5. Loại chính sách trúng (Hit Policy) nào trong bảng quyết định DMN được luận án tập trung nghiên cứu?

Trả lời: Luận án tập trung vào chính sách trúng duy nhất Unique ($u$). Chính sách này quy định rằng với một tập dữ liệu đầu vào cụ thể, chỉ có duy nhất một hàng quy tắc trong bảng quyết định được kích hoạt, đảm bảo tính tất định và không xảy ra xung đột luật trong quá trình chuyển đổi sang hàm CPN-ML và luật ECA.

---

Kết luận

Luận án của NCS. Nguyễn Thanh Tuấn đã giải quyết trọn vẹn bài toán xác thực đồng thời quy trình nghiệp vụ (BPMN) và quy tắc nghiệp vụ (DMN) trong kỹ nghệ phần mềm hướng lập trình đặc tả. Thông qua việc phát triển hai mô hình hình thức VeBPRu (dựa trên CPN) và VeBPRu2 (dựa trên HCPN phân cấp), tác giả đã cung cấp một khung làm việc toán học chuẩn xác để phát hiện sớm các lỗi cấu trúc và dữ liệu trong giai đoạn thiết kế. Khả năng tự động sinh chuỗi luật thực thi ECA từ mô hình đã xác thực mang lại tính ứng dụng cao, đóng góp thiết thực cho việc nâng cao chất lượng và độ tin cậy của các ứng dụng hướng quy trình và nền tảng low-code hiện nay.

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

Chương 1: Tổng quan về quy trình và quy tắc nghiệp vụ phần mềm. Chương này trình bày tổng quan về quy trình nghiệp vụ và quy tắc nghiệp vụ, cùng với việc mô hình hóa chúng sử dụng BPMN và DMN. Phần này cũng giới thiệu về luật ECA và chuỗi luật ECA. • Chương 2: Xác thực quy trình và quy tắc nghiệp vụ phần mềm.

Đề cập đến mạng Petri, mạng Petri màu, mạng Petri màu phân cấp, và hiện trạng nghiên cứu về xác thực quy trình và quy tắc nghiệp vụ. Chương này cũng đề xuất vòng đời phát triển quy trình và quy tắc nghiệp vụ. • Chương 3: Xác thực quy trình và quy tắc nghiệp vụ phần mềm sử dụng mạng Petri màu. Trình bày phương pháp VeBPRu, một cách tiếp cận mới trong xác thực quy trình và quy tắc nghiệp vụ, cùng với các kỹ thuật chuyển đổi và tích hợp hàm CPN-ML.

• Chương 4: Xác thực quy trình và quy tắc nghiệp vụ phần mềm sử dụng mạng Petri màu phân cấp. Phân tích mô hình phân cấp quy trình và quy tắc nghiệp vụ, và hình thức hóa chúng với HCPN. Chương này cũng đề xuất thuật toán chuyển đổi BPMN/DMN sang HCPN và từ HCPN sang ECA, cùng với thử nghiệm và đánh giá. TỔNG QUAN QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ Chương này đặt nền móng cho toàn bộ luận án bằng cách trình bày một cái nhìn tổng quan về quy trình nghiệp vụ và quy tắc nghiệp vụ, bao gồm cả lý thuyết và ứng dụng thực tế.

Đồng thời, chương này cũng khám phá các phương pháp mô hình hóa quy trình nghiệp vụ hiện đại như BPMN và DMN, cũng như cách chúng được sử dụng để tạo ra, đánh giá và cải thiện các quy trình nghiệp vụ và quy tắc nghiệp vụ. Ngoài ra ngôn ngữ ECA và chuỗi ECA cũng được giới thiệu như là một công cụ trung gian để thực thi các quy trình và quy tắc nghiệp vụ. Qua đó, chương này không chỉ cung cấp kiến thức cơ bản về quy trình và quy tắc nghiệp vụ mà còn đề cập đến tầm quan trọng của việc áp dụng các công nghệ và phương pháp tiên tiến trong quản lý quy trình và quy tắc nghiệp vụ, từ đó mở đường cho việc xác thực và tối ưu hóa chúng thông qua sử dụng các công cụ mô hình hóa CPN và HCPN trong các chương tiếp theo của luận án. Quy trình nghiệp vụ và mô hình hoá bằng BPMN 1.

Quy trình nghiệp vụ 1. Quản lý quy trình nghiệp vụ Quản lý quy trình nghiệp vụ (BPM) là tập hợp các hoạt động để hỗ trợ và cải thiện hiệu suất tổ chức thông qua quản lý chuỗi sự kiện, nhiệm vụ và quyết định cuối cùng mang lại giá trị cho tổ chức. Nó bao gồm các khái niệm, phương pháp và kỹ thuật để hỗ trợ thiết kế, quản trị, cấu hình, thi hành và phân tích các quy trình nghiệp vụ [4]. Quy trình nghiệp vụ đã được định nghĩa theo nhiều cách khác nhau [5, 6, 7, 8], điểm chung của các định nghĩa này là xem Quy trình nghiệp vụ là tập hợp các hoạt 10 động được thực hiện để đạt được mục tiêu kinh doanh.

Tuy vậy, định nghĩa 1.1 được đưa ra trong [9] cho cái nhìn rõ ràng nhất về khái niệm Quy trình nghiệp vụ. Một tập hợp các hoạt động liên quan và được cấu trúc thực hiện bởi một hoặc nhiều tổ chức để đạt được một mục tiêu cụ thể. Trong một tổ chức, quy trình nghiệp vụ dẫn đến cung cấp dịch vụ hoặc sản xuất hàng hóa cho các bên liên quan bên trong hoặc bên ngoài. Ngoài ra, các quy trình nghiệp vụ thường liên quan đến nhau vì việc thực hiện một quy trình nghiệp vụ thường dẫn đến kích hoạt các quy trình nghiệp vụ liên quan trong cùng một tổ chức hoặc tổ chức khác.

Vòng đời phát triển quy trình nghiệp vụ Vì các quy trình nghiệp vụ được thực thi và tương tác với thế giới thực có thể thay đổi liên tục nên bản thân các quy trình nghiệp vụ cũng cần được điều chỉnh liên tục. Sự thích ứng liên tục này có thể được mô tả bằng một quy trình tuần hoàn được gọi là vòng đời phát triển quy trình nghiệp vụ được minh họa trong Hình 1. Theo vòng đời này, mỗi quy trình nghiệp vụ liên tục trải qua bốn giai đoạn, mỗi giai đoạn bao gồm các hoạt động khác nhau được tiến hành liên quan đến quy trình. (1) Thiết kế: Để phân tích, cải tiến và triển khai các quy trình nghiệp vụ, đầu tiên phải xác định mục tiêu và các bên liên quan trong quy trình nghiệp vụ, và thiết kế mô hình quy trình nghiệp vụ, đó là một tập hợp các hoạt động và ràng buộc thực thi giữa chúng.

Bước này đại diện cho giai đoạn đầu tiên là giai đoạn Thiết kế trong vòng đời phát triển quy trình nghiệp vụ [11, 12, 4]. Hoạt động chính trong giai đoạn này là xác định phạm vi của các quy trình nghiệp vụ, vì thông thường một tổ chức đã tiến hành nhiều hoạt động nhưng mối tương quan của các hoạt động này với các quy trình nghiệp vụ là không rõ ràng. Sau đó, các quy trình nghiệp vụ được xác định có thể được trình bày trong các mô hình quy trình tương ứng. Điều này cho phép lập tài liệu, xác nhận các quy trình và mô hình của chúng.

Vì các mô hình quy trình chủ yếu là mô hình đồ họa nên chúng là cơ sở để trao đổi thông tin.1: Vòng đời phát triển quy trình [10] (2) Triển khai: Sau khi hoàn thành giai đoạn thiết kế, quy trình nghiệp vụ sẽ bước vào giai đoạn Triển khai. Trong giai đoạn này, quy trình nghiệp vụ được triển khai trong tổ chức. Việc triển khai có thể được thực hiện trong hệ thống Công nghệ thông tin hoặc không. Trong trường hợp đơn giản, quy trình có thể chỉ được thực hiện bằng cách phân công nhân sự thực hiện các bước cần thiết theo trình tự đã định.

Các triển khai nâng cao hơn có thể có sẵn hệ thống phần mềm hỗ trợ thực hiện quy trình nghiệp vụ. (3) Kiểm soát: Trong giai đoạn kiểm soát, quy trình nghiệp vụ được thực thi trong môi trường thực. Trong quá trình này, dữ liệu thực thi sẽ được tạo ra. Dữ liệu này có thể được sử dụng để cung cấp thông tin giám sát về trạng thái hiện tại của quy trình trong quá trình thực thi.

Ví dụ: mô hình quy trình có thể được nâng cao để trực quan hóa hoạt động nào hiện đang được thực hiện hoặc mỗi hoạt động mất bao nhiêu thời gian cho đến nay. Ngoài ra, dữ liệu được thu thập có thể được sử dụng trong giai đoạn tiếp theo của vòng đời. 12 (4) Phân tích: Giai đoạn cuối cùng liên quan đến việc phân tích quy trình nghiệp vụ. Vì luôn có khoảng cách giữa quy trình được thiết kế dưới dạng mô hình và quy trình được thực hiện trong thế giới thực, nên các nhà phân tích có thể sử dụng dữ liệu thực hiện được thu thập để kiểm tra xem mô hình và dữ liệu được căn chỉnh chính xác hoặc nếu có bất kỳ sai lệch nào.

Hơn nữa, các điểm nghẽn trong quy trình có thể được xác định và loại bỏ, chẳng hạn như bằng cách chỉ định nhiều tài nguyên hơn cho một số nhiệm vụ nhất định hoặc bằng cách thực hiện đồng thời một số hoạt động. Mô hình hóa quy trình nghiệp vụ sử dụng BPMN Trong giai đoạn Thiết kế của Vòng đời Phát triển Quy trình Nghiệp vụ, người thiết kế quy trình sẽ tạo ra một mô hình quy trình. Mô hình này cần được biểu diễn một cách rõ ràng và dễ hiểu để thúc đẩy giao tiếp hiệu quả giữa các bên liên quan. Các ngôn ngữ mô hình hóa chuyên biệt được sử dụng để đảm bảo sự nhất quán và khả năng trao đổi thông tin giữa các bên, đồng thời hỗ trợ quá trình điều chỉnh và cải tiến mô hình.

Quá trình thiết kế này thường yêu cầu việc thu thập và phân tích nhiều nguồn thông tin cũng như các quan điểm khác nhau [13]. Ngôn ngữ mô hình hóa quy trình nghiệp vụ: Nhiều ngôn ngữ và kỹ thuật mô hình hóa đã được đề xuất để xử lý các khía cạnh khác nhau của quy trình nghiệp vụ. Mỗi ngôn ngữ có vai trò và đặc điểm riêng biệt nhằm hỗ trợ việc thiết kế, triển khai và phân tích quy trình. Dưới đây là một số ngôn ngữ phổ biến: • Event-driven Process Chain (EPC): EPC là một phương pháp mô hình hóa quy trình nghiệp vụ tập trung vào việc biểu diễn các sự kiện (event) và chức năng (function).

EPC thường được sử dụng trong các dự án phân tích và cải tiến quy trình, đặc biệt là trong lĩnh vực sản xuất và logistics. Ngôn ngữ này giúp xác định trình tự và mối quan hệ giữa các sự kiện và chức năng trong quy trình, hỗ trợ việc tối ưu hóa luồng công việc [14]. 13 • Unified Modeling Language (UML): UML là một ngôn ngữ mô hình hóa đa dụng, được thiết kế để hỗ trợ phân tích và thiết kế hệ thống phức tạp, bao gồm cả quy trình nghiệp vụ. UML bao gồm nhiều loại sơ đồ, như sơ đồ hoạt động (activity diagram) và sơ đồ trường hợp sử dụng (use case diagram), cho phép biểu diễn quy trình nghiệp vụ từ nhiều góc độ khác nhau.

UML thường được sử dụng trong các dự án phần mềm để tích hợp quy trình nghiệp vụ vào hệ thống thông tin [15]. • Semantics of Business Vocabulary and Business Rules (SBVR): SBVR là một khung ngữ nghĩa cho phép định nghĩa và quản lý các thuật ngữ và quy tắc nghiệp vụ. SBVR không chỉ cung cấp ngữ nghĩa chặt chẽ cho các thuật ngữ nghiệp vụ mà còn hỗ trợ tích hợp các quy tắc vào các ngôn ngữ mô hình hóa như BPMN và DMN. Điều này giúp đảm bảo tính rõ ràng và chính xác trong việc biểu diễn và thực thi các quy tắc nghiệp vụ [16].

• Business Process Model and Notation (BPMN): BPMN là tiêu chuẩn toàn cầu để mô hình hóa quy trình nghiệp vụ. Ngôn ngữ này cung cấp một tập hợp các ký hiệu đồ họa tiêu chuẩn nhằm biểu diễn các bước, hoạt động, và thủ tục trong quy trình nghiệp vụ [17]. Các đặc điểm kỹ thuật và chi tiết của BPMN sẽ được trình bày rõ hơn ở phần sau của luận án. • Decision Model and Notation (DMN): DMN là một tiêu chuẩn để mô hình hóa và thực thi các quyết định nghiệp vụ.

DMN hỗ trợ việc quản lý và tự động hóa các quy tắc nghiệp vụ, giúp cải thiện tính nhất quán và hiệu quả của quy trình. DMN sẽ được mô tả chi tiết trong các phần tiếp theo của luận án, tập trung vào vai trò và ứng dụng của nó trong việc tích hợp quy tắc nghiệp vụ vào quy trình [3].