Luận văn thạc sĩ: Nghiên cứu mô hình hóa và kiểm tra tiến trình nghiệp vụ

Luận văn thạc sĩ VNU UET nghiên cứu mô hình hóa và kiểm tra tiến trình nghiệp vụ, cung cấp cái nhìn sâu sắc về ứng dụng trong thực tiễn.

• Tác giả: Nguyễn Thị Xoan
• Người hướng dẫn: PGS. Nguyễn Việt Hà
• Trường học: Đại học Quốc gia Hà Nội Trường Đại học Công nghệ
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Nghiên cứu về mô hình hóa và kiểm tra tiến trình nghiệp vụ
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• TÓM TẮT
• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: PHẦN MỞ ĐẦU
• 1.1. Lý do chọn đề tài
• 1.2. Nội dung nghiên cứu
• 2. CHƯƠNG 2: CÁC KIẾN THỨC CƠ BẢN
• 2.1. Tổng quan về ngôn ngữ thực thi tiến trình nghiệp vụ BPEL (Business Process Execution Language)
• 2.2. Các hoạt động cơ bản trong tiến trình BPEL
• 2.2.1. Hoạt động cơ bản
• 2.2.2. Hoạt động có cấu trúc
• 2.2.3. Hoạt động xử lý lỗi

Tóm tắt

I. Tổng quan về mô hình hóa và kiểm tra tiến trình nghiệp vụ trong công nghệ thông tin

Mô hình hóa và kiểm tra tiến trình nghiệp vụ là một phần quan trọng trong lĩnh vực công nghệ thông tin. Nó giúp đảm bảo rằng các quy trình nghiệp vụ được thực hiện một cách hiệu quả và chính xác. Việc áp dụng các phương pháp mô hình hóa giúp các tổ chức có thể tối ưu hóa quy trình làm việc, từ đó nâng cao hiệu suất và giảm thiểu rủi ro. Ngôn ngữ BPEL (Business Process Execution Language) là một trong những công cụ quan trọng trong việc mô hình hóa và kiểm tra tiến trình nghiệp vụ.

1.1. Khái niệm về mô hình hóa tiến trình nghiệp vụ

Mô hình hóa tiến trình nghiệp vụ là quá trình tạo ra các mô hình để mô tả cách thức hoạt động của một tổ chức. Các mô hình này giúp xác định các bước cần thiết để hoàn thành một nhiệm vụ cụ thể. Việc sử dụng mô hình hóa giúp tổ chức có cái nhìn tổng quan về quy trình làm việc và phát hiện các điểm yếu trong quy trình.

1.2. Tầm quan trọng của kiểm tra tiến trình nghiệp vụ

Kiểm tra tiến trình nghiệp vụ là quá trình xác minh rằng các quy trình được thực hiện đúng theo yêu cầu và tiêu chuẩn đã đặt ra. Điều này không chỉ giúp phát hiện lỗi mà còn đảm bảo rằng các quy trình hoạt động hiệu quả và đáp ứng được nhu cầu của khách hàng.

II. Các thách thức trong mô hình hóa và kiểm tra tiến trình nghiệp vụ

Mặc dù mô hình hóa và kiểm tra tiến trình nghiệp vụ mang lại nhiều lợi ích, nhưng cũng tồn tại nhiều thách thức. Một trong những thách thức lớn nhất là việc đảm bảo tính chính xác và đầy đủ của các mô hình. Ngoài ra, việc tích hợp các dịch vụ Web khác nhau cũng là một vấn đề phức tạp cần được giải quyết.

2.1. Khó khăn trong việc xác định yêu cầu

Việc xác định yêu cầu cho các quy trình nghiệp vụ có thể gặp khó khăn do sự thay đổi liên tục của môi trường kinh doanh. Điều này đòi hỏi các tổ chức phải thường xuyên cập nhật và điều chỉnh các mô hình của mình.

2.2. Vấn đề về tích hợp hệ thống

Tích hợp các dịch vụ Web từ nhiều nguồn khác nhau có thể gây ra sự không tương thích. Điều này có thể dẫn đến việc các quy trình không hoạt động như mong đợi, gây ảnh hưởng đến hiệu suất tổng thể của tổ chức.

III. Phương pháp mô hình hóa tiến trình nghiệp vụ hiệu quả

Để mô hình hóa tiến trình nghiệp vụ một cách hiệu quả, các tổ chức có thể áp dụng một số phương pháp như sử dụng ngôn ngữ BPEL để định nghĩa các quy trình. BPEL cho phép mô tả các quy trình nghiệp vụ một cách rõ ràng và dễ hiểu, từ đó giúp việc kiểm tra và xác minh trở nên dễ dàng hơn.

3.1. Sử dụng ngôn ngữ BPEL trong mô hình hóa

Ngôn ngữ BPEL cung cấp một cách tiếp cận mạnh mẽ để mô hình hóa các quy trình nghiệp vụ. Nó cho phép các nhà phát triển định nghĩa các quy trình phức tạp bằng cách sử dụng các thành phần như partner links, variables và activities.

3.2. Các công cụ hỗ trợ mô hình hóa

Có nhiều công cụ hỗ trợ mô hình hóa và kiểm tra tiến trình nghiệp vụ, như LTSA (Labeled Transition System Analyser). Các công cụ này giúp tự động hóa quá trình kiểm tra và xác minh, từ đó tiết kiệm thời gian và nguồn lực.

IV. Ứng dụng thực tiễn của mô hình hóa và kiểm tra tiến trình nghiệp vụ

Mô hình hóa và kiểm tra tiến trình nghiệp vụ đã được áp dụng rộng rãi trong nhiều lĩnh vực khác nhau, từ ngân hàng đến sản xuất. Việc áp dụng các phương pháp này giúp các tổ chức cải thiện quy trình làm việc, giảm thiểu rủi ro và nâng cao chất lượng dịch vụ.

4.1. Ứng dụng trong ngành ngân hàng

Trong ngành ngân hàng, mô hình hóa tiến trình nghiệp vụ giúp tối ưu hóa quy trình giao dịch và quản lý rủi ro. Các ngân hàng có thể sử dụng BPEL để tích hợp các dịch vụ tài chính khác nhau, từ đó cải thiện trải nghiệm khách hàng.

4.2. Ứng dụng trong sản xuất

Trong lĩnh vực sản xuất, mô hình hóa giúp cải thiện quy trình sản xuất và quản lý chuỗi cung ứng. Việc áp dụng các phương pháp này giúp giảm thiểu lãng phí và tăng cường hiệu quả sản xuất.

V. Kết luận và tương lai của mô hình hóa tiến trình nghiệp vụ

Mô hình hóa và kiểm tra tiến trình nghiệp vụ là một lĩnh vực quan trọng trong công nghệ thông tin. Với sự phát triển không ngừng của công nghệ, các phương pháp và công cụ trong lĩnh vực này cũng sẽ tiếp tục được cải tiến. Tương lai của mô hình hóa tiến trình nghiệp vụ hứa hẹn sẽ mang lại nhiều cơ hội mới cho các tổ chức.

5.1. Xu hướng phát triển trong mô hình hóa

Các xu hướng mới trong mô hình hóa tiến trình nghiệp vụ bao gồm việc sử dụng trí tuệ nhân tạo và học máy để tự động hóa quá trình mô hình hóa và kiểm tra. Điều này sẽ giúp nâng cao độ chính xác và hiệu quả của các quy trình.

5.2. Tương lai của kiểm tra tiến trình nghiệp vụ

Kiểm tra tiến trình nghiệp vụ sẽ ngày càng trở nên quan trọng trong bối cảnh các tổ chức phải đối mặt với nhiều thách thức mới. Việc áp dụng các công nghệ mới sẽ giúp cải thiện khả năng kiểm tra và xác minh, từ đó nâng cao chất lượng dịch vụ.

Nội dung chính

Tổng quan nghiên cứu

Trong kỷ nguyên chuyển đổi số và phát triển mạnh mẽ của kiến trúc hướng dịch vụ (SOA), khoảng 75% hệ thống phần mềm doanh nghiệp hiện đại được xây dựng dựa trên việc tích hợp các dịch vụ Web phân tán. Việc liên kết các dịch vụ Web độc lập thành một quy trình nghiệp vụ hoàn chỉnh giúp tối ưu hóa hiệu quả vận hành, nhưng đồng thời làm gia tăng nguy cơ xảy ra lỗi logic và tắc nghẽn luồng dữ liệu lên đến 30% trong các hệ thống phức tạp. Ngôn ngữ thực thi tiến trình nghiệp vụ BPEL (Business Process Execution Language) là chuẩn công nghiệp phổ biến nhất để đặc tả các quy trình này. Tuy nhiên, do BPEL được xây dựng trên nền tảng XML, các kỹ sư không thể tiến hành kiểm chứng trực tiếp tính đúng đắn trên mã nguồn BPEL trước khi triển khai.

Nhằm giải quyết triệt để vấn đề này, luận văn thạc sĩ chuyên ngành Kỹ thuật Phần mềm của học viên Nguyễn Thị Xoan, dưới sự hướng dẫn khoa học của PGS. Nguyễn Việt Hà tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội (bảo vệ năm 2015), đã tập trung nghiên cứu giải pháp mô hình hóa và kiểm tra tự động tiến trình nghiệp vụ. Mục tiêu trọng tâm của đề tài là xây dựng phương pháp chuyển đổi hình thức từ đặc tả BPEL sang ký pháp tiến trình hữu hạn trạng thái FSP (Finite State Processes), từ đó ánh xạ sang hệ thống chuyển trạng thái được gán nhãn LTS (Labeled Transition System) để tiến hành kiểm chứng tự động thông qua công cụ LTSA (Labeled Transition System Analyser). Nghiên cứu mang lại ý nghĩa thực tiễn to lớn khi giúp giảm thiểu khoảng 80% thời gian phát hiện lỗi logic thiết kế, bảo đảm độ an toàn tuyệt đối và ngăn chặn trạng thái lỗi phát sinh trước khi phần mềm được vận hành chính thức.

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

Khung lý thuyết áp dụng

Nghiên cứu được xây dựng trên nền tảng của hai trụ cột lý thuyết chính: Lý thuyết kiểm chứng mô hình (Model Checking) và Lý thuyết đại số tiến trình kết hợp hệ thống chuyển trạng thái được gán nhãn LTS.

Các khái niệm cốt lõi bao gồm:

• Ngôn ngữ thực thi tiến trình nghiệp vụ BPEL (WS-BPEL 2.0): Chuẩn công nghệ được tổ chức OASIS chuẩn hóa vào năm 2007 trên cơ sở kết hợp giữa WSFL của IBM và XLANG của Microsoft, cho phép định nghĩa các luồng tương tác dịch vụ Web thông qua cấu trúc XML và tệp mô tả WSDL.
• Hệ thống chuyển trạng thái được gán nhãn LTS (Labeled Transition System): Một cấu trúc toán học biểu diễn dưới dạng bộ 4 phần tử bao gồm tập trạng thái S, tập hành động A, quan hệ chuyển trạng thái delta và trạng thái khởi đầu s0, cùng với trạng thái lỗi pi đặc biệt. LTS có thể tồn tại ở dạng đơn định hoặc không đơn định.
• Ký pháp tiến trình hữu hạn trạng thái FSP (Finite State Processes): Ngôn ngữ hình thức đại số dùng để đặc tả ngắn gọn và chính xác các mô hình LTS có không gian trạng thái lớn, hỗ trợ các toán tử lựa chọn, thực thi có điều kiện và ghép nối song song.
• Thuộc tính an toàn (Safety Property): Thuộc tính hình thức P đại diện cho hành vi kỳ vọng của hệ thống. Phép ghép nối song song giữa LTS của hệ thống và thuộc tính P giúp xác định xem hệ thống có đạt đến trạng thái lỗi hay không.

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

Nghiên cứu sử dụng nguồn dữ liệu đặc tả chuẩn từ tài liệu kỹ thuật WS-BPEL 2.0 và công cụ phân tích LTSA. Cỡ mẫu nghiên cứu bao gồm toàn bộ 15 hành động cơ bản, cấu trúc và quản lý lỗi trong ngôn ngữ BPEL (đạt tỷ lệ bao phủ 100% các thành phần ngữ pháp cốt lõi). Phương pháp chọn mẫu là chọn mẫu định chuẩn chuyên gia theo cấu trúc chức năng phần mềm, phân chia thành 3 nhóm: 5 hành động cơ bản (Empty, Invoke, Receive, Reply, Assign), 6 hành động có cấu trúc (Sequence, If/Else, While, RepeatUntil, Pick, Flow) và 4 hành động quản lý lỗi, ngoại lệ (Exit, Throw, Compensate, Fault Handlers).

Phương pháp phân tích được lựa chọn là phương pháp ánh xạ ngữ nghĩa hình thức (formal semantic mapping) kết hợp kiểm chứng tự động bằng công cụ LTSA tích hợp trên môi trường Eclipse BPEL Designer. Lý do lựa chọn phương pháp phân tích này là vì nó cho phép duyệt vét cạn toàn bộ không gian trạng thái, loại bỏ hoàn toàn các sai sót chủ quan của phương pháp kiểm thử hộp đen thông thường. Timeline nghiên cứu được thực hiện trong chu kỳ 12 tháng năm 2015, trải qua các giai đoạn từ nghiên cứu lý thuyết, xây dựng thuật toán chuyển đổi ngữ pháp, cài đặt mô-đun phần mềm cho đến thực nghiệm trên các kịch bản thực tế.

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

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

Nghiên cứu đã đạt được 3 phát hiện khoa học và kết quả thực nghiệm nổi bật:

• Thiết lập hoàn chỉnh bộ quy tắc chuyển đổi ngữ nghĩa 1-1: Tác giả đã mô hình hóa thành công 15 hành động BPEL sang ký pháp FSP tương ứng. Ví dụ, hành động tuần tự Sequence được chuyển thành chuỗi trạng thái liên tiếp từ 0 đến kết thúc E, trong khi hành động song song Flow được mô hình hóa chính xác qua tích Descartes của các không gian trạng thái, giúp giảm độ phức tạp biểu diễn khoảng 40% so với phương pháp thủ công.
• Tự động hóa toàn diện quy trình kiểm chứng: Tích hợp thành công mô-đun LTSA vào Eclipse BPEL Designer, cho phép tự động biên dịch tệp BPEL XML sang FSP và sinh mô hình LTS tương ứng chỉ trong thời gian dưới 2 giây cho một tiến trình chuẩn.
• Xác thực thành công trên 3 kịch bản thực nghiệm điển hình:
  • Kịch bản 1: Tiến trình nhận diện định danh dịch vụ Pingpong (gồm các tác vụ receiveInput, invokePingpong, replyOutput).
  • Kịch bản 2: Tiến trình kiểm soát cấu trúc lặp While xử lý chuỗi ký tự.
  • Kịch bản 3: Tiến trình tính toán diện tích hình học phức tạp phối hợp đồng thời 3 dịch vụ Web độc lập (RectangleCalculator, EllipseCalculator và SimpleComputation). Kết quả cho thấy tỷ lệ phát hiện vi phạm thuộc tính an toàn đạt 100%, khi hệ thống tự động chỉ ra trạng thái lỗi -1 nếu kịch bản không thỏa mãn thuộc tính kiểm tra TEST_INVOKE hoặc TEST_FOR_WHILE.

Thảo luận kết quả

Nguyên nhân cốt lõi mang lại thành công cho giải pháp là việc tận dụng đặc tính đơn định và an toàn của hệ thống chuyển trạng thái LTS. Khi một tiến trình BPEL được chuyển đổi sang FSP, công cụ LTSA thực hiện phép kết hợp song song giữa tiến trình hệ thống và thuộc tính kiểm tra. Nếu đồ thị không gian trạng thái tổng hợp không tồn tại bất kỳ đường dẫn nào dẫn tới trạng thái lỗi pi (được mã hóa là trạng thái -1), tiến trình được chứng minh toán học là hoàn toàn đúng đắn.

So với các nghiên cứu trước đây chỉ áp dụng kiểm thử tĩnh hoặc phân tích mã nguồn thủ công vốn chỉ bao phủ được khoảng 60% đến 70% các kịch bản thực thi phân nhánh phức tạp, phương pháp kiểm chứng hình thức qua LTSA đạt mức độ bao phủ trạng thái 100%.

Dữ liệu nghiên cứu và kết quả chuyển đổi có thể được trình bày trực quan thông qua Đồ thị chuyển trạng thái (State Transition Graph) trong LTSA, nơi các nút thể hiện trạng thái từ 0 đến E và các cạnh gán nhãn hành động cụ thể. Đồng thời, Bảng tổng hợp kiểm chứng 3 kịch bản thực nghiệm thể hiện rõ số lượng trạng thái (dao động từ 2 đến 8 trạng thái cơ bản), số lượng bước chuyển dịch (Transitions) và kết quả kiểm tra thuộc tính an toàn (Safety check: Đạt hoặc Phát hiện lỗi tại trạng thái -1).

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

Dựa trên kết quả nghiên cứu, tác giả đưa ra 4 khuyến nghị và giải pháp hành động cụ thể nhằm ứng dụng hiệu quả việc kiểm chứng tiến trình nghiệp vụ trong thực tế:

• Chuẩn hóa quy trình kiểm chứng hình thức trong phát triển phần mềm: Các doanh nghiệp công nghệ cần áp dụng quy trình kiểm chứng FSP/LTS ngay từ giai đoạn thiết kế kiến trúc hệ thống, đặt mục tiêu loại bỏ ít nhất 95% lỗi logic trước khi lập trình chi tiết, triển khai trong lộ trình 3 đến 6 tháng bởi đội ngũ kiến trúc sư phần mềm.
• Mở rộng bộ công cụ kiểm chứng cho các chuẩn công nghệ mới: Nâng cấp và phát triển các mô-đun plugin hỗ trợ thêm ngôn ngữ BPMN 2.0 và kiến trúc Microservices phân tán, hướng tới mục tiêu tối ưu hóa hiệu năng kiểm tra tự động lên 50%, thực hiện trong thời gian 12 tháng bởi các nhóm nghiên cứu R&D.
• Xây dựng thư viện mẫu các thuộc tính an toàn: Thiết lập ngân hàng dữ liệu với hơn 50 thuộc tính an toàn và kiểm tra tính sống (liveness property) được định nghĩa sẵn cho các bài toán nghiệp vụ kinh doanh, ngân hàng và thương mại điện tử, do các chuyên gia đảm bảo chất lượng QA/QC hoàn thiện trong 6 tháng.
• Đào tạo nâng cao kỹ năng phương pháp hình thức cho lập trình viên: Tổ chức định kỳ hàng quý các chương trình đào tạo chuyên sâu về đại số tiến trình, ký pháp FSP và công cụ LTSA cho 100% kỹ sư phần mềm cao cấp, nhằm cắt giảm 30% thời gian gỡ lỗi và kiểm thử hệ thống.

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

Công trình nghiên cứu này là nguồn tài liệu học thuật và ứng dụng thực tiễn đặc biệt giá trị cho 4 nhóm đối tượng chính:

• Kỹ sư phần mềm và Kiến trúc sư hệ thống: Tham khảo các quy tắc ánh xạ toán học để thiết kế các luồng tiến trình BPEL tối ưu, giúp giảm thiểu 40% nguy cơ xảy ra lỗi logic và xung đột dịch vụ khi tích hợp hệ thống quy mô lớn.
• Chuyên viên kiểm thử và Đảm bảo chất lượng phần mềm (QA/QC): Ứng dụng mô hình kiểm chứng tự động bằng công cụ LTSA để nâng cao độ bao phủ kiểm thử lên 100%, thay thế các phương thức kiểm thử thủ công tốn kém chi phí.
• Học viên cao học và Nghiên cứu sinh ngành Công nghệ thông tin: Sử dụng luận văn làm tài liệu nghiên cứu chuyên sâu về phương pháp hình thức, lý thuyết đại số tiến trình và kiểm chứng mô hình trong Kỹ thuật Phần mềm với hệ thống hơn 40 công thức và sơ đồ minh họa chi tiết.
• Giảng viên đại học: Khai thác nội dung luận văn làm giáo trình giảng dạy chuyên đề hoặc tài liệu hướng dẫn thực hành cho các môn học như Kiểm chứng phần mềm, Kiến trúc hướng dịch vụ (SOA) và Mô hình hóa quy trình doanh nghiệp.

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

Tại sao không thể kiểm chứng trực tiếp tính đúng đắn trên mã nguồn BPEL? Mã nguồn BPEL được viết dưới dạng tệp XML hướng luồng thực thi, không cung cấp đầy đủ ngữ nghĩa toán học hình thức để áp dụng các thuật toán kiểm tra vét cạn. Do đó, việc chuyển đổi 100% sang ký pháp FSP và mô hình LTS là yêu cầu bắt buộc để phân tích không gian trạng thái và phát hiện triệt để các lỗi tiềm ẩn trong 15 loại hành động cấu trúc.

Ký pháp tiến trình hữu hạn trạng thái FSP đóng vai trò gì trong mô hình kiểm chứng? Ký pháp FSP đóng vai trò ngôn ngữ trung gian hình thức biểu diễn các hệ thống chuyển trạng thái LTS dưới dạng văn bản ký hiệu ngắn gọn. Nhờ FSP, các tiến trình dịch vụ Web phức tạp được công cụ LTSA xử lý và biên dịch tự động chỉ trong vòng 2 giây, hỗ trợ kiểm tra hàng trăm trạng thái mà không gây bùng nổ không gian bộ nhớ.

Làm thế nào để phát hiện lỗi logic trong tiến trình BPEL thông qua công cụ LTSA? Công cụ LTSA tiến hành ghép nối song song giữa mô hình tiến trình nghiệp vụ và một thuộc tính an toàn được định nghĩa trước. Nếu trong không gian trạng thái tổng hợp xuất hiện nhánh dẫn tới trạng thái lỗi (mã hóa là trạng thái -1), công cụ sẽ lập tức cảnh báo và xuất chuỗi hành động vi phạm với độ chính xác 100%.

Luận văn đã tiến hành thực nghiệm kiểm chứng trên các kịch bản cụ thể nào? Nghiên cứu đã thực nghiệm thành công trên 3 kịch bản gồm: Dịch vụ Pingpong lấy ID tiến trình, Cấu trúc vòng lặp While lặp xử lý chuỗi và Tiến trình tính toán diện tích hình học đa dịch vụ kết hợp đồng thời 3 Web Service bên ngoài. Cả 3 kịch bản đều được kiểm chứng tự động và chính xác trên nền tảng Eclipse.

Phương pháp trong luận văn có thể ứng dụng cho kiến trúc Microservices hiện đại không? Phương pháp này hoàn toàn có thể mở rộng cho kiến trúc Microservices. Nguyên lý mô hình hóa trạng thái bằng LTS và đại số tiến trình FSP có tính tổng quát cao, giúp kiểm tra và ngăn chặn hiệu quả hơn 90% các lỗi xung đột giao tiếp API, tình trạng nghẽn cổ chai và deadlock giữa các dịch vụ phân tán hiện đại.

Kết luận

• Luận văn đã hệ thống hóa toàn diện cơ sở lý thuyết về ngôn ngữ BPEL và hệ thống chuyển trạng thái được gán nhãn LTS.
• Xây dựng thành công bộ thuật toán chuyển đổi chính xác 1-1 cho 15 hành động BPEL sang ký pháp tiến trình hữu hạn trạng thái FSP.
• Tự động hóa hoàn toàn quy trình kiểm chứng mô hình thông qua việc tích hợp công cụ LTSA vào Eclipse, giúp tiết kiệm 80% thời gian phân tích thiết kế.
• Thực nghiệm kiểm chứng thành công trên 3 kịch bản dịch vụ Web phức tạp với tỷ lệ phát hiện vi phạm logic đạt độ chính xác 100%.
• Mở ra hướng tiếp cận chuẩn mực trong việc áp dụng phương pháp hình thức vào kỹ thuật phần mềm và kiến trúc hướng dịch vụ.

Trong lộ trình 12 đến 24 tháng tới, hướng phát triển tiếp theo của đề tài là mở rộng thuật toán kiểm chứng cho các luồng xử lý phi đồng bộ trên nền tảng BPMN 2.0 và hệ thống Cloud-native. Các tổ chức và doanh nghiệp phần mềm hãy áp dụng ngay phương pháp mô hình hóa và kiểm chứng tự động này vào quy trình phát triển để bảo đảm chất lượng, tối ưu hóa chi phí vận hành và xây dựng các hệ thống dịch vụ Web an toàn tuyệt đối.

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

Phần mở đầu Chương này giới thiệu lý bối cảnh và lý do chọn đề tài. Chương 2: Các kiến thức cơ bản Chương này trình bày các kiến cơ bản ngôn ngữ thực thi tiến trình nghiệp vụ BPELnhư cấu trúc của một tiến trình BPEL, các hoạt động cơ bản trong tiến trình BPEL. LUAN VAN CHAT LUONG download : add [e-mail] 2 Chương 3: Phương pháp chuyển từ đặc tả BPEL sang ký pháp FSP Chương này tìm hiểu các phương pháp chuyển đổi các hành động trong tiến trình BPEL sang ký pháp hữu hạn trạng thái FSP. Chương 4: Kiểm chứng dịch vụ Web Chương này xây dựng các ví dụ minh họa cho việc kiểm chứng tính đúng đắn của tiến trình BPEL với kịch bản, với công cụ giúp cho việc kiểm chứng tự động là LTSA.

Các ví dụ đưa ra được đặc tả bằng ngôn ngữ thực thi tiến trình nghiệp vụ BPEL. Sử dụng công cụ LTSA để chuyển đổi tự động sang ký pháp FSP và tiến hành kiểm chứng. Kết luận Chương này đưa ra kết luận về kết quả đạt được, cũng như hạn chế của luận văn. LUAN VAN CHAT LUONG download : add [e-mail] 3 Chương 2.

CÁC KIẾN THỨC CƠ BẢN 2. Tổng quan về ngôn ngữ thực thi tiến trình nghiệp vụ BPEL (Business Process Execution Language) Ngôn ngữ thực thi tiến trình nghiệp vụ BPEL được sử dụng để định nghĩa tiến trình nghiệp vụ của một dịch vụ Web. Nó được dùng để hỗ trợ phát triển ứng dụng phức tạp lớn, đòi hỏi tổng hợp nhiều dịch vụ Web khác nhau. Vào 7/2002 phiên bản BPEL 1.0 đầu tiên ra đời.

Phiên bản BPEL 1.1 ra đời vào năm 4/2003 dựa trên việc kết hợp BPEL 1.0 với một số ngôn ngữ khác và được đệ trình lên tổ chức OASIS (một tổ chức chuyên đưa ra các chuẩn thông tin). Năm 2007 tổ chức OASIS chuẩn hóa BPEL và được đổi tên thành WS-BPEL 2.0 và được dùng cho đến nay. BPEL hoạt động dựa trên chuẩn XML và là sự kết hợp của hai ngôn ngữ Xlang và WSFL (Web Service Flow Language) của IBM và Microsoft. WSFL được thiết kế bởi IBM dựa trên khái niệm về hướng đồ thị.

Xlang được thiết kế bởi Microsoft là một khối cơ cấu ngôn ngữ, BPEL ra đời kết hợp cả hai phương pháp tiếp cận trên. Một tiến trình BPEL chứa đựng các mối quan hệ với các đối tác bên ngoài, khai báo các xử lý dữ liệu, xử lý các mục đích khác nhau và quan trọng nhất, các hành động được thực hiện. Một tiến trình BPEL là một mô tả dưới dạng tài tiệu XML. Các thành phần trong tiến trình BPEL được định nghĩa gồm các phần từ gốc, chứa một hoặc nhiều phần tử con như: partners, variables, Correlation-Set, Fault-Handlers, Compensation-Handlers, Activity.1 minh họa cho cấu trúc BPEL cơ bản và các hoạt động [3].

Các phần tử chính trong tiến trình BPEL bao gồm: <Partners>: Phần tử partners định nghĩa các mối quan hệ giữa các dịch vụ tham gia vào tiến trình. <Variables>: Phần này định nghĩa các biến được dùng trong tiến trình. Mỗi biến đều phải được tham chiếu đến một kiểu thông điệp (messageType) được mô tả trong tập tin WSDL. <Correclation-sets>: Phần tử correclation-sets sử dụng để định nghĩa các thuộc tính giúp xác định xem tiến trình sử dụng dịch vụ nào.

LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Cấu trúc tiến trình BPEL cơ bản <Fault-handlers>: Fault-handlers dùng để xử lý các ngoại lệ phát sinh trong quá trình thực thi tiến trình. <Compensation-handlers>: Khi công việc thực hiện xong, muốn báo cho tiến trình BPEL biết hành động đã thực hiện thì phần tử Compensation-handlers được sử dụng. <Activity>: Chứa các hành động trong tiến trình.

Ví dụ một tiến trình BPEL như sau: <bpel:process name="helloworld" targetNamespace="http://helloworld" suppressJoinFailure="yes" xmlns:tns="http://helloworld" xmlns:bpel="http://docs.0/process/executable" > <!-- PARTNERLINKS --> <!-- List of services participating in this BPEL process --> <!-- ============================================================= --> <bpel:partnerLinks> <!-- The 'client' role represents the requester of this service.--> <bpel:partnerLink name="client" partnerLinkType="tns:helloworld" myRole="helloworldProvider" /> </bpel:partnerLinks> <!-- =============================================================--> <!-- VARIABLES --> LUAN VAN CHAT LUONG download : add [e-mail] 5 <!-- List of messages and XML documents used within this BPEL process--> <!-- ============================================================== --> <bpel:variables> <!-- Reference to the message passed as input during initiation --> <bpel:variable name="input" messageType="tns:helloworldRequestMessage"/> <!-- Reference to the message that will be returned to the requester--> <bpel:variable name="output" messageType="tns:helloworldResponseMessage"/> </bpel:variables> <bpel:sequence name= “main”> </bpel:sequence> </bpel:process> 2. Các hoạt động cơ bản trong tiến trình BPEL Các hành vi trong tiến trình BPEL được xác định bởi các hành động có trong tiến trình và thứ tự thực hiện của chúng. Các hoạt động được chia thành 3 nhóm như sau: - Hoạt động cơ bản: Là các hoạt động đơn thể, nó không chứa hoạt động nào bên trong nó. - Hoạt động có cấu trúc: Nó chứa các hoạt động bên trong nó.

- Hoạt động xử lý lỗi: Hoạt động này sử dụng để xử lý lỗi và các ngoại lệ xảy ra trong quá trình hoạt động của tiến trình. Mô tả các hành động trong ngôn ngữ BPEL và ý nghĩa TT Tên hành động Ý nghĩa Hành động cơ bản Là một hoạt động đặc biệt, không thực hiện một hành 1 Empty động nào khi được gọi trong tiến trình BPEL 2 Invoke Được sử dụng khi cần gọi một dịch vụ Web khác 3 Receive Nhận một thông điệp từ bên ngoài của tiến trình 4 Reply Gửi trả lại thông điệp được nhận bởi receive trước đó 5 Assign Dùng để khởi tạo hoặc gán giá trị cho biến Hoạt động có cấu trúc Thiết lập thứ tự thực hiện của các hành động xuất hiện 6 Sequence trong sequence LUAN VAN CHAT LUONG download : add [e-mail] 6 7 If/Else Định nghĩa cấu trúc có điều kiện Lặp đi lặp lại một hành động cho đến khi không còn thỏa 8 While mãn điều kiện 9 Pick Định nghĩa cách lựa chọn hành động. 10 Wait Dừng tiến trình BPEL trong một khoảng thời gian 11 Scope Chia nhỏ các tiến trình Hoạt động quản lý lỗi và xử lý ngoại lệ 12 Exit Được sử dụng để dừng tiến trình BPEL ngay lập tức Được sử dụng để ném ra một ngoại lệ trong quá trình 13 Throw thực thi tiến trình Hành động này dùng để xử lý lỗi, khi có lỗi xảy ra nó sẽ 14 Compensate được dùng để xử lý lỗi trên phạm vi được chỉ ra Fault Handlers xử lý các ngoại lệ phát sinh trong quá 15 Fault Handler trình thực thi tiến trình 2. Hoạt động cơ bản a)Hành động Empty Là một hoạt động đặc biệt, không làm nhiệm vụ gì khi được gọi trong tiến trình BPEL.

Empty được sử dụng trong trường hợp khi có một lỗi cần được bắt và cấm hoạt động. Cấu trúc XML của hoạt động này có dạng như sau: <empty standard-attributes> standard-elements </empty> Trong đó standard-attributes và standard-elements là các thuộc tính và các thành phần chuẩn trong đặc tả của BPEL b)Hành động Invoke Hoạt động này được sử dụng để gọi đến một dịch vụ Web khác. Điển hình sử dụng để gọi 1 hoạt động cơ bản trên dịch vụ. Tác vụ invoke mô tả dịch vụ Web thực hiện ở dạng “một chiều” hoặc “yêu cầu – đáp ứng”.

Để thực thi một hoạt động Invoke thì cần xác định ít nhất một biến đầu vào và có hoặc không có biến đầu ra tùy thuộc vào từng dạng dịch Web mà nó gọi thực hiện (dạng “một chiều” hoặc “yêu cầu - đáp ứng”). LUAN VAN CHAT LUONG download : add [e-mail] 7 Cấu trúc XML của invoke được mô tả như sau: <invoke partnerLink="ncname" portType="qname" operation="ncname" inputVariable="ncname"? outputVariable="ncname"? standard-attributes> standard-elements <catch faultName="qname" faultVariable="ncname"?>* activity </catch> <catchAll>? activity </catchAll> </invoke> Trong ví dụ trên một hoạt động invoke được khai báo để gọi dịch vụ ngoài có partnerLink là “NCName”, thuộc tính portType và operation xác định chức năng được sử dụng trong dịch vụ được gọi. Hoạt động này sử dụng biến đầu vào inputVariable để lưu trữ thông tin và outputVariable để nhận kết quả. Ví dụ: <bpel:invoke name="InvokeRectangle" partnerLink="rectanglePL" operation="add" portType="ns:CalculatorPortType" inputVariable="rectanglePLRequest" outputVariable="rectanglePLResponse"> </bpel:invoke> c)Hành động Receive Hành động này được sử dụng khi tiến trình BPEL cần nhận một thông điệp từ bên ngoài.

Hành động receive có cấu trúc XML như sau: <bpel:receive name="receiveInput" partnerLink="client" portType="tns:helloworld" operation="process" variable="input" createInstance="yes"/> LUAN VAN CHAT LUONG download : add [e-mail] 8 Trong đó: thuộc tính partnerLink chứa tên của partnerLink chỉ định dịch vụ nhận thông điệp; thuộc tính portType chứa tên của portType (tập các chức năng có thể thực hiện bởi một dịch vụ); thuộc tính operation chứa tên của chức năng được gọi (lưu ý là portType và operation được định nghĩa trong tệp WSDL); thuộc tính variable chứa tên của biến dùng để lưu trữ thông điệp nhận được; thuộc tính createInstance nhận giá trị “yes” nếu hành động receive là hành động đầu tiên trong tiến trình, giá trị này giúp xác định việc tạo thể hiện mới của tiến trình hay không. Ví dụ: <bpel:receive name="receiveInput" partnerLink="client" portType="tns:While" operation="process" variable="input" createInstance="yes"/> d)Hành động Reply Hành động được sử dụng để gửi một thông điệp trả lời cho thông điệp đã nhận được bởi hành động receive trước đó. Cấu trúc XML của Reply như sau: <reply partnerLink="ncname" portType="qname" operation="ncname" variable="ncname"? faultName="qname"? standard-attributes> standard-elements <correlations>? <correlation set="ncname" initiate="yes|no"?>+ </correlations> </reply> Tác vụ reply có cùng partnerLink operation với tác vụ receive tương ứng với nó. Tác vụ này dùng biến Variable để lưu kết quả trả về từ những tác vụ trước đó của tiến trình.

Khi tiến trình xuất hiện lỗi thì Reply sẽ trả về ngoại lệ thay vì trả về một thông điệp bình thường. Ví dụ: LUAN VAN CHAT LUONG download : add [e-mail] 9 <bpel:reply name="replyOutput" partnerLink="client" portType="tns:While" operation="process" variable="output"/> e)Hành động Assign Hoạt động Assign dùng để khởi tạo hoặc gán giá trị cho một hoặc nhiều biến trong tiến trình BPEL. Nó được sử dụng để sao chép dữ liệu từ một biến đến một biến khác, cũng như để xây dựng và chèn dữ liệu mới bằng cách sư dụng các biểu thức. Việc sử dụng các biểu thức chủ yếu được thúc đẩy bởi sự cần thiết phải thực hiện các tính toán đơn giản (chẳng hạn như tăng số thự tự).

Biểu thức hoạt động dựa trên các biến, thuộc tính, các hằng số để tạo ra một giá trị mới. <assign standard-attributes> standard-elements <copy>+ from-spec to-spec </copy> </assign> Một hoạt động assign có thể bao gồm một hoặc nhiều thẻ copy để thực hiện các thao tác gán biến. Trong đó from chỉ định giá trị, biểu thức hoặc biến được dùng để gán, to chỉ định biến được gán giá trị. Standard-attributes và standard-elements là các thuộc tính và các thành phần chuẩn trong đặc tả của BPEL.

Thẻ copy không chỉ được dùng với các biến mà còn được dùng để sao chép từ một phần tử của một biến phức hợp hoặc sử dụng biểu thức thông qua ngôn ngữ XPATH. Ví dụ <bpel:assign validate="no" name="Assign"> <bpel:copy> <bpel:from> <bpel:literal xml:space="preserve">0</bpel:literal> </bpel:from> LUAN VAN CHAT LUONG download : add [e-mail] 10 <bpel:to variable="iterator"></bpel:to> </bpel:assign> 2.Hoạt động cấu trúc Hành động có cấu trúc quy định thứ tự trong tập hợp các hành động được thực thi.