Luận án Tiến sĩ Khoa học máy tính: Mô hình xác thực nghiệp vụ phần mềm theo hướng lập trình đặc tả

Chia sẻ: _ _ | Ngày: | Loại File: PDF | Số trang:167

Thêm vào BST

Báo xấu

4
lượt xem 3
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Luận án Tiến sĩ Khoa học máy tính "Mô hình xác thực nghiệp vụ phần mềm theo hướng lập trình đặc tả" trình bày các nội dung chính sau: Tổng quan về quy trình và quy tắc nghiệp vụ phần mềm; 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; 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ủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Luận án Tiến sĩ Khoa học máy tính: Mô hình xác thực nghiệp vụ phần mềm theo hướng lập trình đặc tả

ĐẠI HỌC ĐÀ NẴNG TRƯỜNG ĐẠI HỌC BÁCH KHOA ————————————— Nguyễn Thanh Tuấn 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Ĩ NGÀNH KHOA HỌC MÁY TÍNH Đà Nẵng – 2024
ĐẠI HỌC ĐÀ NẴNG TRƯỜNG ĐẠI HỌC BÁCH KHOA ————————————— Nguyễn Thanh Tuấn MÔ HÌNH XÁC THỰC NGHIỆP VỤ PHẦN MỀM THEO HƯỚNG LẬP TRÌNH ĐẶC TẢ Chuyên ngành: Khoa học máy tính Mã số: 9 48 01 01 LUẬN ÁN TIẾN SĨ NGÀNH KHOA HỌC MÁY TÍNH NGƯỜI HƯỚNG DẪN KHOA HỌC: 1. GS. TSKH. Lê Thành Nhân 2. TS. Hoàng Thị Thanh Hà Đà Nẵng – 2024
i LỜI CAM ĐOAN Tôi xin cam đoan các kết quả trình bày trong luận án là công trình nghiên cứu của tôi dưới sự hướng dẫn của các cán bộ hướng dẫn. Các số liệu, các kết quả trình bày trong luận án hoàn toàn trung thực và chưa được công bố trong các công trình trước đây. Các dữ liệu tham khảo được trích dẫn đầy đủ. Đà Nẵng, ngày 28 tháng 10 năm 2024 Nguyễn Thanh Tuấn
ii LỜI CẢM ƠN Trong quá trình nghiên cứu và hoàn thành Luận án, Nghiên cứu sinh đã nhận được sự định hướng, giúp đỡ, các ý kiến đóng góp quý báu và những lời động viên của các nhà khoa học, các thầy cô giáo, đồng nghiệp và gia đình. Trước hết, Nghiên cứu sinh xin bày tỏ lời cảm ơn tới thầy PGS.TSKH Lê Thành Nhân và cô TS. Hoàng Thị Thanh Hà đã tận tình hướng dẫn và giúp đỡ trong quá trình nghiên cứu. Cho phép Nghiên cứu sinh chân thành cảm ơn các thầy cô giáo, các nhà khoa học của Khoa Công nghệ thông tin, trường Đại học Bách Khoa - Đại học Đà Nẵng đã có các góp ý quý báu cho Nghiên cứu sinh trong quá trình thực hiện Luận án này. Nghiên cứu sinh chân thành cảm ơn Ban Giám đốc, Ban Đào tạo, Đại học Đà Nẵng, Ban giám hiệu, Khoa Tin học trường Đại học Sư phạm, Ban giám hiệu, Khoa Khoa học máy tính trường Đại học Công nghệ thông tin và Truyền thông Việt Hàn đã tạo điều kiện thuận lợi để Nghiên cứu sinh hoàn thành nhiệm vụ nghiên cứu. Cuối cùng Nghiên cứu sinh bày tỏ lời cảm ơn tới các đồng nghiệp, gia đình, bạn bè đã luôn động viên, chia sẻ, ủng hộ và giúp đỡ Nghiên cứu sinh vượt qua khó khăn để đạt được những kết quả nghiên cứu trong Luận án này. NCS Nguyễn Thanh Tuấn
iii MỤC LỤC LỜI CẢM ƠN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ii MỤC LỤC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii DANH MỤC CÁC KÝ HIỆU, CÁC TỪ VIẾT TẮT . . . . . . . . . . . . vii DANH MỤC CÁC HÌNH VẼ . . . . . . . . . . . . . . . . . . . . . . . . . ix DANH MỤC CÁC BẢNG BIỂU . . . . . . . . . . . . . . . . . . . . . . . x MỞ ĐẦU 1 A. Tính cấp thiết của đề tài nghiên cứu: . . . . . . . . . . . . . . . . . . . . 1 B. Mục tiêu nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 C. Nội dung nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 D. Đối tượng và phạm vi nghiên cứu . . . . . . . . . . . . . . . . . . . . . . 5 E. Phương pháp nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 F. Ý nghĩa khoa học và thực tiễn của luận án . . . . . . . . . . . . . . . . . 6 G. Bố cục của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 CHƯƠNG 1. TỔNG QUAN QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ 9 1.1 Quy trình nghiệp vụ và mô hình hoá bằng BPMN . . . . . . . . . . 9 1.1.1 Quy trình nghiệp vụ . . . . . . . . . . . . . . . . . . . . . . . 9 1.1.2 Mô hình hóa quy trình nghiệp vụ sử dụng BPMN . . . . . 12 1.2 Quy trình nghiệp vụ và mô hình hoá bằng BPMN . . . . . . . . . . 14 1.3 Quy tắc nghiệp vụ và mô hình hoá bằng DMN . . . . . . . . . . . . 18 1.3.1 Định nghĩa Quy tắc nghiệp vụ . . . . . . . . . . . . . . . . . . 18 1.3.2 Mô hình hóa quy tắc nghiệp vụ sử dụng DMN . . . . . . . . . 20 1.3.3 Kết hợp DMN trong mô hình BPMN . . . . . . . . . . . . . . 24 1.4 Luật ECA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1.4.1 Định nghĩa và Cấu trúc Luật ECA . . . . . . . . . . . . . . 27
iv 1.4.2 Vai trò và Khả năng Thực thi của Luật ECA . . . . . . . . 28 1.4.3 Ứng dụng và Triển khai Luật ECA . . . . . . . . . . . . . . 29 1.5 Chuỗi luật ECA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1.6 Kết luận chương 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 CHƯƠNG 2. XÁC THỰC QUY TRÌNH VÀ QUY TẮC NGHIỆP VỤ 32 2.1 Mạng Petri . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.2 Mạng Petri màu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.3 Mạng Petri màu phân cấp . . . . . . . . . . . . . . . . . . . . . . . . 37 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ụ 38 2.4.1 Hình thức hóa quy trình nghiệp vụ . . . . . . . . . . . . . . 39 2.4.2 Xác thực quy trình nghiệp vụ . . . . . . . . . . . . . . . . . 43 2.4.3 Xác thực quy tắc nghiệp vụ . . . . . . . . . . . . . . . . . . 44 2.5 So sánh các phương pháp . . . . . . . . . . . . . . . . . . . . . . . . 45 2.6 Vòng đời phát triển quy trình và quy tắc nghiệp vụ mở rộng . . . 47 2.7 Kết luận chương 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 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 52 3.1 Xác thực quy trình nghiệp vụ với CPN . . . . . . . . . . . . . . . . 52 3.2 Đề xuất mô hình xác thực quy trình và quy tắc nghiệp vụ - VeBPRu 53 3.3 Hình thức hóa quy trình và quy tắc nghiệp vụ . . . . . . . . . . . . 56 3.3.1 Các quy tắc chuyển đổi . . . . . . . . . . . . . . . . . . . . . 56 3.3.2 Tích hợp hàm CPN-ML vào mô hình CPN . . . . . . . . . 68 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 . . . . . . . . . . . . . . 69 3.3.4 Ví dụ minh họa: Quy trình xác nhận đơn hàng . . . . . . . 71 3.4 Xác thực quy trình và quy tắc nghiệp vụ với CPN . . . . . . . . . . 74 3.4.1 Các yếu tố xác thực . . . . . . . . . . . . . . . . . . . . . . . 74 3.4.2 Xác thực mô hình CPN . . . . . . . . . . . . . . . . . . . . . 81
v 3.5 Chuyển đổi mô hình CPN sang chuỗi luật ECA . . . . . . . . . . . 83 3.5.1 Mô hình CPN-ECA . . . . . . . . . . . . . . . . . . . . . . . 83 3.5.2 Hình thức hóa quy trình CPN sang chuỗi ECA . . . . . . . 85 3.5.3 Ví dụ minh họa . . . . . . . . . . . . . . . . . . . . . . . . . . 88 3.6 Thử nghiệm và đánh giá . . . . . . . . . . . . . . . . . . . . . . . . . 90 3.6.1 Sự cần thiết khi thực hiện Thử nghiệm và Đánh giá mô hình VeBPRu . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 3.6.2 Thiết lập thử nghiệm nền tảng VeBPRu . . . . . . . . . . . 92 3.6.3 Bộ dữ liệu mô hình thử nghiệm . . . . . . . . . . . . . . . . 96 3.6.4 Kết quả thử nghiệm . . . . . . . . . . . . . . . . . . . . . . . 99 3.7 Kết luận chương 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 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 110 4.1 Phân cấp quy trình và quy tắc nghiệp vụ . . . . . . . . . . . . . . . 110 4.1.1 Tính Phân Cấp trong BPMN . . . . . . . . . . . . . . . . . . 111 4.1.2 Tính Phân Cấp trong DMN . . . . . . . . . . . . . . . . . . 112 4.2 Mô hình VeBPRu2: xác thực quy trình và quy tắc nghiệp vụ phân cấp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 4.3 Hình thức hóa quy trình và quy tắc nghiệp vụ với HCPN . . . . . 114 4.3.1 Các quy tắc chuyển đổi . . . . . . . . . . . . . . . . . . . . . 114 4.3.2 Thuật toán chuyển đổi BPMN/DMN sang HCPN . . . . . . 115 4.3.3 Phân tích thuật toán . . . . . . . . . . . . . . . . . . . . . . . 117 4.3.4 Ví dụ minh họa: Quy trình xác nhận đơn hàng . . . . . . . 119 4.4 Chuyển đổi mô hình HCPN sang ECA . . . . . . . . . . . . . . . . 122 4.4.1 Thuật toán chuyển đổi HCPN sang ECA . . . . . . . . . . . 122 4.4.2 Ví dụ minh họa . . . . . . . . . . . . . . . . . . . . . . . . . . 125 4.5 Thử nghiệm và đánh giá . . . . . . . . . . . . . . . . . . . . . . . . . 127 4.5.1 Thiết lập thử nghiệm nền tảng VeBPRu2 . . . . . . . . . . 128 4.5.2 Bộ dữ liệu mô hình thử nghiệm . . . . . . . . . . . . . . . . 131
vi 4.5.3 Bộ dữ liệu mô hình thử nghiệm . . . . . . . . . . . . . . . . 131 4.5.4 Kết quả thử nghiệm . . . . . . . . . . . . . . . . . . . . . . . 133 4.5.5 So sánh giữa VeBPRu và VeBPRu2 . . . . . . . . . . . . . . 138 4.6 Kết luận chương 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 KẾT LUẬN 141 CÁC CÔNG TRÌNH KHOA HỌC ĐÃ CÔNG BỐ 144 TÀI LIỆU THAM KHẢO 146
vii DANH MỤC CÁC KÝ HIỆU, CÁC CHỮ VIẾT TẮT Ký hiệu/Từ viết tắt Ý nghĩa Diễn giải BPMN Business Process Model Tiêu chuẩn mô hình và ký and Notation hiệu quy trình nghiệp vụ BPM Business Process Man- Quản lý quy trình nghiệp agement vụ CPN Colored Petri Net Mạng Petri màu CPN-ML CPN-ML Programming Ngôn ngữ lập trình CPN- Language ML sử dụng cho CPN DMN Decision Model and No- Tiêu chuẩn Mô hình và tation Ký hiệu Quyết định DLL Decision Logic Level Biểu diễn quy tắc dưới dạng một bảng quyết định DRD Decision Requirements Sơ đồ Yêu cầu Quyết Diagram định ECA Event-Condition-Action Luật Event-Condition- Action FEEL Friendly Enough Expres- Ngôn ngữ biểu đạt sử sion Language dụng trong bảng quyết định OMG Object Management Tổ chức quản lý đối Group tượng PDA Process-Driven Applica- Ứng dụng hướng quy tions trình
viii Ký hiệu/Từ viết tắt Ý nghĩa Diễn giải HCPN Hierarchical Colored Mạng Petri màu phân cấp Petri Net S-FEEL Simple Friendly Enough Một tập con của FEEL, Expression Language sử dụng trong bảng quyết định VeBPRu Verification Business Tên của mô hình xác Process and Business thực quy trình và quy Rules Model tắc nghiệp vụ sử dụng mạng Petri màu (được định nghĩa trong luận án) VeBPRu2 Version 2 of ”Verification Phiên bản 2 của mô hình of Business Process and xác thực quy trình và quy Business Rules Model” tắc nghiệp vụ sử dụng mạng Petri màu phân cấp (được định nghĩa trong luận án) XML Extensible Markup Lan- Ngôn ngữ đánh dấu mở guage rộng XSD XML Schema Chỉ định cách mô tả chính thức các phần tử trong tài liệu XML
ix DANH MỤC CÁC HÌNH VẼ Hình 1.1 Vòng đời phát triển quy trình [10] . . . . . . . . . . . . . . . . . 11 Hình 1.2 Một ví dụ về sơ đồ BPMN . . . . . . . . . . . . . . . . . . . . . 15 Hình 1.3 Mô hình BPMN có Hồ bơi (Pool) [17] . . . . . . . . . . . . . . 16 Hình 1.4 Các loại Hoạt động (Activity) [17] . . . . . . . . . . . . . . . . . 17 Hình 1.5 Các loại Connection Edge [17] . . . . . . . . . . . . . . . . . . . 17 Hình 1.6 Các loại Gateway [17] . . . . . . . . . . . . . . . . . . . . . . . 19 Hình 1.7 Các loại arterfact được xem xét [17] . . . . . . . . . . . . . . . . 20 Hình 1.8 Ví dụ về DRD . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Hình 1.9 Các thành phần trong Bảng quyết định . . . . . . . . . . . . . . 23 Hình 1.10 Ví dụ về kết hợp DMN trong BPMN . . . . . . . . . . . . . . . 26 Hình 2.1 Ví dụ về đồ thị mạng Petri . . . . . . . . . . . . . . . . . . . . . 34 Hình 2.2 Ví dụ về mạng Petri màu . . . . . . . . . . . . . . . . . . . . . . 36 Hình 2.3 Phân loại các nghiên cứu liên quan . . . . . . . . . . . . . . . . 39 Hình 2.4 Vòng đời phát triển quy trình và quy tắc nghiệp vụ mở rộng với giai đoạn xác thực . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Hình 3.1 VeBPRu - Mô hình xác thực quy trình và quy tắc nghiệp vụ . . . 54 Hình 3.2 Mô hình chuyển đổi quy trình và quy tắc nghiệp vụ sang mạng Petri màu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 Hình 3.3 Mẫu hàm trong ngôn ngữ CPN-ML . . . . . . . . . . . . . . . . 68 Hình 3.4 Sơ đồ BPMN của Quy trình xác nhận đơn hàng . . . . . . . . . 71 Hình 3.5 Bảng quyết định DMN của quy tắc nghiệp vụ chiết khấu . . . . 72 Hình 3.6 Mô hình CPN của Quy trình xác nhận đơn hàng . . . . . . . . . 73 Hình 3.7 Hàm CPN-ML xử lý quy tắc chiết khấu . . . . . . . . . . . . . . 74 Hình 3.8 CPN-ECA model . . . . . . . . . . . . . . . . . . . . . . . . . . 84
x Hình 3.9 Mô hình CPN cho Order Business trong hệ thống Online Shopping 89 Hình 3.10 Các khai báo của mô hình CPN cho Order Business . . . . . . . 90 Hình 3.11 Sơ đồ thành phần của chuỗi công cụ VeBPRu . . . . . . . . . . . 93 Hình 3.12 Quy trình sử dụng nền tảng VeBPRu . . . . . . . . . . . . . . . . 95 Hình 3.13 Biểu đồ biểu diễn dữ liệu trong bảng Bộ dữ liệu mô hình 1. . . . 98 Hình 3.14 Biểu đồ so sánh thời gian chuyển đổi của VeBPRu và BPMN2CPN theo nhóm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 Hình 3.15 Biểu đồ biểu diễn thời gian chuyển đổi và số phần tử của bộ dữ liệu mô hình 2. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 Hình 3.16 Biểu đồ minh họa thời gian chuyển đổi và số lượng luật ECA sinh ra từ mô hình CPN . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Hình 4.1 VeBPRu2 - Phương pháp xác thực quy trình và quy tắc nghiệp vụ phân cấp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 Hình 4.2 Các khai báo của mô hình con Payment Business . . . . . . . . 119 Hình 4.3 Mô hình HCPN phân cấp của Order Business . . . . . . . . . . . 120 Hình 4.4 Mô hình con Payment Business trong Order Business. . . . . . . 121 Hình 4.5 Sơ đồ thành phần của chuỗi công cụ VeBPRu2 . . . . . . . . . . 129 Hình 4.6 Quy trình sử dụng nền tảng VeBPRu2 . . . . . . . . . . . . . . . 130 Hình 4.7 Biểu đồ biểu diễn số lượng mô hình và số phần tử trung bình trong từng nhóm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 Hình 4.8 Biểu đồ biểu diễn thời gian chuyển đổi và số phần tử trung bình của bộ dữ liệu mô hình 3. . . . . . . . . . . . . . . . . . . . . . . . . . 135 Hình 4.9 Biểu diễn thời gian chuyển đổi sang ECA từ mô hình HCPN . . 136 Hình 4.10 Biểu diễn thời gian chuyển đổi sang ECA từ mô hình HCPN . . 138
xi DANH MỤC CÁC BẢNG BIỂU Bảng 2.1 So sánh các phương pháp mô hình hóa và xác thực quy trình nghiệp vụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Bảng 3.1 Ánh xạ các thành phần chung của BPMN sang CPN . . . . . . . 58 Bảng 3.2 Quy tắc BP2CPN2: Chuyển đổi Công việc, Sự kiện và Luồng trình tự từ BPMN sang CPN . . . . . . . . . . . . . . . . . . . . . . . 61 Bảng 3.3 Chuyển đổi Cổng từ BPMN sang CPN . . . . . . . . . . . . . . 63 Bảng 3.4 Chuyển đổi Luồng Thông điệp . . . . . . . . . . . . . . . . . . . 64 Bảng 3.5 Chuyển đổi Xử lý Ngoại lệ . . . . . . . . . . . . . . . . . . . . . 65 Bảng 3.6 Chuyển đổi Các Thành phần Dữ liệu (Data Elements) . . . . . . 66 Bảng 3.7 Bộ dữ liệu mô hình 1 . . . . . . . . . . . . . . . . . . . . . . . . 97 Bảng 3.8 Bộ dữ liệu mô hình 2 . . . . . . . . . . . . . . . . . . . . . . . . 99 Bảng 3.9 Thời gian chuyển đổi sang CPN bộ dữ liệu mô hình 1 . . . . . . 100 Bảng 3.10 Thời gian và tỷ lệ xác thực bộ dữ liệu mô hình 1 . . . . . . . . . 102 Bảng 3.11 Thời gian chuyển đổi sang CPN bộ dữ liệu mô hình 2 . . . . . . 103 Bảng 3.12 Thời gian xác thực bộ dữ liệu mô hình 2 . . . . . . . . . . . . . 105 Bảng 3.13 Thời gian chuyển đổi sang ECA từ mô hình CPN . . . . . . . . 107 Bảng 4.1 Chuyển đổi Quy trình con . . . . . . . . . . . . . . . . . . . . . 115 Bảng 4.2 Bộ dữ liệu mô hình 3 . . . . . . . . . . . . . . . . . . . . . . . . 132 Bảng 4.3 Thời gian chuyển đổi sang HCPN bộ dữ liệu mô hình 3 . . . . . 134 Bảng 4.4 Thời gian xác thực bộ dữ liệu mô hình 3 . . . . . . . . . . . . . 136 Bảng 4.5 Thời gian chuyển đổi sang ECA từ mô hình HCPN . . . . . . . 137 Bảng 4.6 So sánh giữa VeBPRu và VeBPRu2 . . . . . . . . . . . . . . . . 139
1 MỞ ĐẦU A. Tính cấp thiết của đề tài nghiên cứu: Một trong những điểm quan trọng nhất ảnh hưởng đến hiệu quả của các hoạt động trong lĩnh vực công nghệ phần mềm là các chuyên gia trong lĩnh vực ứng dụng và chuyên gia công nghệ thông tin có thể trao đổi với nhau và chuyển tải các yêu cầu mang tính chuyên môn hiệu quả và rõ ràng như thế nào. Việc thực hiện thành công các hoạt động này cần có sự tham gia của cả hai bên, đảm bảo rằng các nhu cầu của ứng dụng được hiểu đúng và các công nghệ được sử dụng đúng cách. Trên thực tế, các lỗi được tạo ra trong giai đoạn thiết kế sẽ dẫn đến các vấn đề khó khăn trong giai đoạn phát triển sau này, việc không hiểu đúng yêu cầu của các chuyên gia sẽ làm tốn kém hơn và gây ra một số rủi ro cho dự án. Do đó, xác định và khắc phục sớm các lỗi trong giai đoạn thiết kế sẽ giúp các dự án đạt được thành công và giảm thiểu rủi ro. Một xu hướng mới trong phát triển phần mềm là sử dụng các nền tảng low-code, cho phép xây dựng các ứng dụng mà không cần viết nhiều code. Các nền tảng low- code cung cấp các giao diện kéo và thả trực quan, cho phép người dùng tùy chỉnh các chức năng có mã hóa, kết nối với các nguồn dữ liệu và triển khai ứng dụng một cách nhanh chóng và trực quan. Các nền tảng low-code giúp tiết kiệm thời gian, chi phí và nguồn lực cho các doanh nghiệp, đồng thời tăng khả năng thích ứng và sáng tạo của các lập trình viên. Một số các nền tảng low-code hiện đại như Microsoft Power Platform (https://powerplatform.microsoft.com) hay Appian (https://appian.com/) đã được tích hợp một thành phần quan trọng đó là Quy trình nghiệp vụ. Khái niệm ”Quy trình nghiệp vụ” (business process), được phát triển trước tiên trong lĩnh vực tổ chức và quản lý kinh doanh, đang nhanh chóng được áp dụng như một công cụ mô hình hóa trong công nghệ phần mềm để tăng hiệu quả giao tiếp giữa các bên liên quan.
2 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 để đạt được một mục tiêu nghiệp vụ nhất định [1]. Đây là một tập hợp các bước liên tục được thực hiện để chuyển đổi đầu vào thành đầu ra có giá trị. Quy trình nghiệp vụ có thể bao gồm nhiều khía cạnh, bao gồm công việc, các quy tắc và tương tác giữa các thành phần khác nhau. Hơn nữa, các mô hình thuộc loại này có thể được kết hợp để xây dựng mô hình Hợp tác, mô tả sự phối hợp của nhiều nhóm làm việc cùng nhau để đạt được các mục tiêu chung. 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. Đối với Ứng dụng hướng Quy trình (PDA) [2], mô hình Quy trình nghiệp vụ đó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. Bên cạnh Quy trình nghiệp vụ, khía cạnh Quy tắc nghiệp vụ cũng được quan tâm xem xét. Quy tắc nghiệp vụ là các nguyên tắc, quy định, hoặc luật lệ được thiết lập để hướng dẫn và điều chỉnh các quyết định và hành động trong quy trình nghiệp vụ. Các quy tắc nghiệp vụ thường xuyên định rõ các điều kiện và hành động cần thực hiện khi xảy ra một sự kiện cụ thể. Để phân biệt rõ ràng giữa quy trình nghiệp vụ và quy tắc nghiệp vụ, 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ụ. 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ụ. Tuy nhiên, BPMN và DMN vẫn chưa cung cấp đầy đủ khả năng tích hợp và xác thực tự động các quy trình và quy tắc nghiệp vụ, đặ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à
3 một thách thức lớn đối với doanh nghiệp. Do đó, nghiên cứu này hướng đến phát triển một phương pháp hình thức nhằm 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. Rất nhiều nghiên cứu đã được thực hiện để giải quyết khía cạnh này nhưng vẫn còn một vẫn còn một số vấn đề chưa được được quan tâm trong các nghiên cứu trước đây đó là: • Vấn đề 1: Hiện chưa có một 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ấn đề 2: 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. B. Mục tiêu nghiên cứu Mục đích chính của luận án này là đề 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à các quy tắc nghiệp vụ phần mềm Các mục tiêu nghiên cứu cụ thể bao gồm: • Đánh giá các phương pháp và công cụ hiện có để mô hình hóa và xác thực các quy trình nghiệp vụ và các quy tắc nghiệp vụ. • Phát triển một phương pháp mới để hình thức hóa các quy trình và quy tắc nghiệp vụ.
4 • Dựa trên mô hình hình thức hóa, đưa ra các kỹ thuật và công cụ để xác thực đồng thời quy trình và quy tắc nghiệp vụ. C. Nội dung nghiên cứu Từ các mục tiêu trên, luận án đưa ra các nội dung nghiên cứu như sau: 1. Luận án sẽ tập trung vào đánh giá các phương pháp và công cụ hiện có để mô hình hóa và xác thực các quy trình nghiệp vụ và các quy tắc nghiệp vụ như BPMN, DMN, Mạng Petri màu (CPN), Mạng Petri màu phân cấp (HCPN), Luật Event- Condition-Action (ECA) và các phương pháp khác. Việc đánh giá này sẽ xác định được các ưu điểm và nhược điểm của các phương pháp và công cụ. Nghiên cứu cũng sẽ phân tích các ứng dụng thực tế của các phương pháp và công cụ này, từ đó đưa ra những đánh giá về tính khả thi và hiệu quả của chúng. 2. Luận án sẽ đề 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. Một trong những vấn đề quan trọng trong phát triển các hệ thống nghiệp vụ phức tạp là việc thực thi các quy trình và quy tắc nghiệp vụ. Để làm được điều này, một phương pháp phổ biến là sử dụng 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. Tuy nhiên, để tạo ra các chuỗi luật ECA, một cách tiếp cận thường được sử dụng là chuyển đổi từ các mô hình CPN và HCPN, là một công cụ mạnh mẽ để mô hình hóa các quy trình và quy tắc nghiệp vụ. Việc chuyển đổi này rất phức tạp và đòi hỏi nhiều công sức từ các nhà phát triển. Do đó, luận án sẽ hướng đến 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. 4. Luận án cũng tập trung tìm hiểu các phương pháp phân tích không gian trạng thái và các kỹ thuật khác như kiểm tra mô hình. Áp dụng các phương pháp đó để đánh giá các mô hình CPN được phát triển trong các mục tiêu trước đó của nghiên cứu. D. Đối tượng và phạm vi nghiên cứu Đối tượng và phạm vi nghiên cứu của đề tài này bao gồm: • Các phương pháp và công cụ hiện có để mô hình hóa và xác thực các quy trình nghiệp vụ và các quy tắc nghiệp vụ, bao gồm BPMN, DMN, CPN, HCPN, ECA và các công cụ hỗ trợ việc sử dụng chúng. • Các phương pháp và công cụ mới được đề xuất để chuyển đổi các mô hình BPMN và DMN thành các mô hình CPN và HCPN. Kỹ thuật chuyển đổi các mô hình CPN và HCPN thành các chuỗi luật ECA cũng được đề xuất. • Các kỹ thuật phân tích không gian trạng thái và các kỹ thuật khác để đánh giá tính chính xác, tính nhất quán, tính đầy đủ và tính tuân thủ của các mô hình CPN, HCPN và ECA. E. Phương pháp nghiên cứu Phương pháp nghiên cứu của luận án được xây dựng dựa trên các nguyên lý hình thức hóa và sử dụng các phương pháp tiên tiến để giải quyết bài toán xác thực và thực thi quy trình kết hợp với quy tắc nghiệp vụ. Phương pháp này bao gồm hai giai đoạn
6 chính: chuyển đổi từ BPMN/DMN sang CPN/HCPN và sử dụng chuỗi luật ECA để thực thi các quy trình nghiệp vụ đã được xác thực. Trong giai đoạn chuyển đổi từ BPMN/DMN sang CPN/HCPN, các thành phần của quy trình nghiệp vụ (bao gồm hoạt động, luồng điều khiển, và ràng buộc nghiệp vụ) được mô hình hóa dưới dạng các trạng thái và chuyển tiếp trong mạng Petri. Phương pháp này đảm bảo rằng các ràng buộc nghiệp vụ từ DMN được tích hợp chặt chẽ với các trạng thái trong mạng Petri, tạo ra một mô hình hình thức hóa có thể xác thực. Mạng CPN/HCPN được sử dụng để phân tích tính chính xác và tính toàn vẹn của luồng công việc, bao gồm việc kiểm tra các tiêu chí như tính đầy đủ, không xung đột, và tính nhất quán. Sau khi quá trình xác thực hoàn tất, chuỗi luật ECA được áp dụng để thực thi các quy trình nghiệp vụ. Các điều kiện và hành động được thiết lập dựa trên các trạng thái và ràng buộc của mạng CPN/HCPN, đảm bảo rằng các quy trình nghiệp vụ được thực thi chính xác theo thiết kế ban đầu. 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. Phương pháp nghiên cứu đảm bảo tính hiện đại thông qua việc kết hợp các tiêu chuẩn quốc tế như BPMN và DMN với các công cụ hình thức mạnh mẽ như mạng Petri và ECA. Tính hợp lý của phương pháp được thể hiện qua cấu trúc rõ ràng của các bước nghiên cứu, từ mô hình hóa đến thực thi. Cuối cùng, độ tin cậy của phương pháp được kiểm chứng thông qua các thử nghiệm trên các quy trình nghiệp vụ thực tế, cho thấy khả năng ứng dụng cao trong các hệ thống phức tạp. F. Ý nghĩa khoa học và thực tiễn của luận án Luận án mang lại các giá trị khoa học nổi bật, góp phần mở rộng và củng cố lý thuyết trong lĩnh vực hình thức hóa và mô hình hóa quy trình nghiệp vụ, cụ thể: 1. Phát triển phương pháp kết hợp xác thực quy trình và quy tắc nghiệp vụ: Lần đầu tiên, luận án đề xuất một phương pháp kết hợp giữa BPMN, DMN, mạng
7 Petri (CPN/HCPN) và chuỗi luật ECA để xác thực và thực thi quy trình nghiệp vụ. Phương pháp này không chỉ đảm bảo tính chính xác và toàn vẹn trong thiết kế mà còn giải quyết bài toán xác thực đồng thời quy trình và quy tắc nghiệp vụ, vốn là một thách thức lớn trong lĩnh vực Khoa học máy tính. 2. Mở rộng lý thuyết mạng Petri trong mô hình hóa quy trình nghiệp vụ: Bằng cách tích hợp các ràng buộc logic từ DMN vào mạng Petri, luận án đã cải tiến khả năng biểu diễn và xác thực các quy trình nghiệp vụ phức tạp, đồng thời mở rộng phạm vi ứng dụng của mạng Petri trong các bài toán thực tế. 3. Đóng góp vào lĩnh vực hình thức hóa trong phát triển phần mềm: Phương pháp luận của luận án kết hợp hình thức hóa với tính ứng dụng cao, cung cấp một cách tiếp cận mới cho các bài toán xác thực và thực thi quy trình nghiệp vụ trong môi trường phát triển phần mềm doanh nghiệp. Về mặc thực tiễn, Luận án mang lại các đóng góp mới mang tính ứng dụng cao, hỗ trợ doanh nghiệp và các tổ chức trong việc tối ưu hóa quy trình nghiệp vụ, cụ thể: 1. Tích hợp hiệu quả các công cụ và tiêu chuẩn quốc tế: Phương pháp của luận án cho phép kết hợp BPMN và DMN để mô hình hóa quy trình và quy tắc nghiệp vụ, đồng thời sử dụng mạng Petri (CPN/HCPN) để xác thực và chuỗi luật ECA để thực thi. Điều này tạo ra một cách tiếp cận toàn diện, giúp các doanh nghiệp dễ dàng chuyển đổi và thực thi các quy trình nghiệp vụ. 2. Tăng cường khả năng thực thi và quản lý quy trình: Sử dụng ECA để thực thi các quy trình nghiệp vụ đã được xác thực giúp tăng cường khả năng phản ứng linh hoạt với các sự kiện xảy ra trong hệ thống, phù hợp với các lĩnh vực như tài chính, chuỗi cung ứng, và y tế. 3. Có thể ứng dụng trong các hệ thống lớn và phức tạp: Các phương pháp và kết quả của luận án đã được kiểm chứng qua thực nghiệm, cho thấy khả năng áp dụng hiệu quả trong các hệ thống yêu cầu tính tích hợp và quản lý quy trình toàn diện.