Luận văn: Kiểm chứng hệ tương tranh CSP# và công cụ PAT

Luận văn thạc sĩ: Kiểm chứng hệ thống tương tranh dùng CSP và PAT. Nghiên cứu hình thức, mô hình hóa, và xác minh tính đúng đắn của hệ thống.

• Tác giả: Nguyễn Văn Trãi
• Người hướng dẫn: TS. Nguyễn Trường Thắng
• Trường học: Trường Đại học Công nghệ - Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Kiểm Chứng Hình Thức Cho Hệ Thống Tương Tranh Sử Dụng Ngôn Ngữ Đặc Tả CSP# Và Công Cụ PAT
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2013
• Địa điểm: Hà Nội

Mục lục chi tiết

• Lời cảm ơn
• Lời cam đoan
• Mục lục
• Danh mục các bảng
• Danh mục các hình vẽ
• Lời mở đầu
• 1. Chương 1: Kiểm chứng mô hình
• 1.1. Tổng quan về kiểm chứng mô hình
• 1.2. Các đặc tính của kiểm chứng mô hình
• 1.2.1. Các pha thực hiện
• 1.2.2. Ưu điểm và nhược điểm
• 2. Chương 2: Hệ thống tương tranh
• 2.1. Tổng quan về hệ tương tranh
• 2.2. Mô hình hóa hệ tương tranh bởi hệ dịch chuyển
• 2.2.1. Xử lý đan xen (Interleaving)
• 2.2.2. Giao tiếp qua biến chia sẻ (Shared Variables)
• 2.2.3. Tương tác dạng bắt tay (Handshaking)
• 2.2.4. Giao tiếp thông qua kênh truyền (Channel Systems)
• 2.2.5. Xử lý song song đồng bộ (Synchronous Parallelism)
• 3. Chương 3: Đặc tả mô hình hệ tương tranh với CSP#
• 3.1. Ngôn ngữ CSP#
• 3.1.1. Các định nghĩa toàn cục
• 3.1.2. Định nghĩa tiến trình
• 3.2. Một cách tiếp cận trích xuất mô hình từ mã nguồn C#
• 3.2.1. Xử lý đa luồng trong C#
• 3.2.2. Trích xuất mô hình từ mã nguồn C#
• 3.2.3. Hướng phát triển
• 4. Chương 4: Kiểm chứng thử nghiệm với PAT
• 4.1. Tổng quan về PAT
• 4.2. Mô-đun CSP
• 4.3. Ví dụ thử nghiệm
• 4.4. So sánh đánh giá
• Kết luận
• Danh mục công trình khoa học liên quan đến luận văn
• Tài liệu tham khảo

Tóm tắt

I. Giới thiệu CSP và PAT cho Kiểm chứng Mô hình Tương tranh

Trong bối cảnh các hệ thống phần mềm ngày càng phức tạp, việc kiểm chứng tính đúng đắn của các hệ thống tương tranh trở nên vô cùng quan trọng. Các hệ thống này, với sự tương tác phức tạp giữa các thành phần, thường tiềm ẩn những lỗi khó phát hiện bằng các phương pháp kiểm thử truyền thống. Kiểm chứng hình thức nổi lên như một giải pháp hiệu quả, sử dụng các phương pháp toán học để mô hình hóa và phân tích hệ thống, đảm bảo tính đúng đắn với sự chặt chẽ của toán học.

Bài viết này giới thiệu cách tiếp cận kiểm chứng mô hình cho hệ xử lý tương tranh, tập trung vào phương pháp mô hình hóa hệ thống. Ngôn ngữ Communicating Sequential Processes Sharp (CSP#), một ngôn ngữ mô hình hóa cụ thể, sẽ được giới thiệu, và các mô hình đặc tả bằng ngôn ngữ này sẽ được sử dụng trong phần kiểm chứng thử nghiệm với bộ công cụ Process Analysis Toolkit (PAT). PAT là một công cụ kiểm chứng mô hình mạnh mẽ, hỗ trợ ngôn ngữ CSP#, giúp tự động xác minh mô hình hệ thống tương tranh và phát hiện các lỗi tiềm ẩn như deadlock, liveness và safety violations.

Theo tài liệu gốc, các kỹ thuật như kiểm thử thường đem lại hiệu quả rất thấp vì lỗi trong hệ tương tranh thường không có xu hướng lặp lại [1]. Vì vậy, việc sử dụng PAT và CSP# là vô cùng quan trọng.

1.1. Tổng quan về Hệ thống Tương tranh và Thách thức Kiểm chứng

Hệ thống tương tranh bao gồm nhiều tiến trình độc lập, được thực thi đồng thời và có thể tương tác với nhau. Việc xác định tính đúng đắn cho các hệ thống này rất khó khăn vì sự tương tác phức tạp giữa các thành phần cùng xử lý trong hệ thống. Các lỗi xuất hiện thường không có xu hướng lặp lại, vì thế rất khó phát hiện bởi các ca kiểm thử. Do đó việc mô hình hóa hệ thống đồng thời và kiểm chứng mô hình hệ tương tranh là vô cùng cần thiết. Các kỹ thuật như model checking sẽ có hiệu quả cao hơn các phương pháp testing phần mềm thông thường. Việc sử dụng các formal method là điều cần thiết.

1.2. Giới thiệu Ngôn ngữ CSP và Vai trò trong Kiểm chứng

CSP# là một ngôn ngữ hình thức đặc tả mô hình hệ tương tranh, kế thừa từ CSP và mở rộng thêm một số thành phần. Nó cho phép các tiến trình được định nghĩa dưới cả hai dạng là tiến trình tuần tự và các thành phần song song kết hợp từ nhiều tiến trình. Quan hệ giữa các tiến trình và cách mà chúng giao tiếp với môi trường được đặc tả bằng các toán tử Process Algebra. Kiểm chứng CSP sẽ giúp các nhà phát triển có thể tìm và sửa lỗi một cách hiệu quả. Sử dụng CSP# để mô tả hệ thống là bước đầu tiên, sau đó sử dụng PAT để kiểm chứng CSP#.

1.3. Công cụ PAT và Quy trình Kiểm chứng Mô hình CSP

PAT (Process Analysis Toolkit) là một công cụ hỗ trợ kiểm chứng mô hình mạnh mẽ, được phát triển để phân tích và xác minh các hệ thống phần mềm phức tạp. Nó cung cấp một môi trường toàn diện để mô hình hóa, mô phỏng, và kiểm chứng các hệ thống tương tranh, đặc biệt là những hệ thống được mô tả bằng ngôn ngữ CSP#. PAT hỗ trợ nhiều kỹ thuật kiểm chứng, bao gồm model checking, simulation, và refinement checking, cho phép người dùng phân tích mô hình và xác định các lỗi tiềm ẩn. Theo tài liệu gốc PAT sẽ giúp kiểm chứng thử nghiệm trên hệ thống tương tranh sử dụng ngôn ngữ CSP#. Cần tham khảo thêm các tài liệu PAT để hiểu rõ hơn về công cụ này.

II. Thách thức Mô hình hóa Hệ tương tranh với CSP

Mặc dù CSP# cung cấp một phương tiện mạnh mẽ để mô hình hóa các hệ thống tương tranh, nhưng quá trình này vẫn tiềm ẩn những thách thức đáng kể. Một trong những thách thức lớn nhất là quản lý độ phức tạp của hệ thống. Các hệ thống tương tranh thường bao gồm nhiều thành phần tương tác, mỗi thành phần có trạng thái và hành vi riêng. Việc mô hình hóa tất cả các thành phần này một cách chính xác và hiệu quả đòi hỏi sự hiểu biết sâu sắc về hệ thống và khả năng trừu tượng hóa tốt.

Một thách thức khác là đảm bảo tính chính xác của mô hình. Mô hình phải phản ánh chính xác hành vi của hệ thống thực tế, nếu không kết quả kiểm chứng sẽ không có giá trị. Điều này đòi hỏi phải có một quy trình mô hình hóa cẩn thận và tỉ mỉ, cũng như các công cụ và kỹ thuật để xác minh tính chính xác của mô hình. Ngoài ra, việc lựa chọn mức độ trừu tượng phù hợp cũng là một thách thức quan trọng. Một mô hình quá chi tiết có thể trở nên quá phức tạp để kiểm chứng, trong khi một mô hình quá trừu tượng có thể bỏ qua các chi tiết quan trọng, dẫn đến kết quả kiểm chứng không đầy đủ. Theo tài liệu gốc, quá trình mô hình hóa hệ thống thường không sử dụng trực tiếp hệ dịch chuyển mà thông qua một ngôn ngữ mô hình hóa trung gian để đảm bảo tính trực quan đối với người dùng. Sau đó các đặc tả mô hình bằng ngôn ngữ này được chuyển tự động qua dạng hệ dịch chuyển dựa trên ngữ nghĩa của ngôn ngữ đã sử dụng.

2.1. Quản lý Độ phức tạp trong Mô hình hóa Hệ Tương tranh

Các hệ thống tương tranh thường có số lượng lớn các trạng thái và chuyển đổi trạng thái, dẫn đến vấn đề bùng nổ không gian trạng thái. Để giải quyết vấn đề này, cần sử dụng các kỹ thuật trừu tượng hóa để giảm kích thước của mô hình mà vẫn giữ lại các thuộc tính quan trọng cần kiểm chứng. Các kỹ thuật này bao gồm data abstraction, control flow abstraction, và symmetry reduction.

2.2. Đảm bảo Tính chính xác của Mô hình CSP

Để đảm bảo tính chính xác của mô hình CSP#, cần sử dụng các kỹ thuật xác minh mô hình. Điều này có thể được thực hiện bằng cách mô phỏng mô hình và so sánh hành vi của nó với hành vi mong đợi của hệ thống thực tế. Ngoài ra, có thể sử dụng các kỹ thuật kiểm chứng hình thức để xác minh rằng mô hình đáp ứng các thuộc tính mong muốn.

2.3. Lựa chọn Mức độ Trừu tượng Phù hợp trong Mô hình hóa

Việc lựa chọn mức độ trừu tượng phù hợp trong mô hình hóa là rất quan trọng. Một mô hình quá chi tiết có thể trở nên quá phức tạp để kiểm chứng, trong khi một mô hình quá trừu tượng có thể bỏ qua các chi tiết quan trọng. Cần tìm một sự cân bằng giữa độ chi tiết và tính trừu tượng để đảm bảo rằng mô hình có thể được kiểm chứng một cách hiệu quả và chính xác.

III. Phương pháp Kiểm chứng Mô hình CSP bằng Công cụ PAT

PAT cung cấp một loạt các phương pháp kiểm chứng để xác minh các thuộc tính của mô hình CSP#. Các phương pháp này bao gồm model checking, simulation, và refinement checking. Model checking là một kỹ thuật tự động kiểm chứng rằng mô hình đáp ứng một đặc tả nhất định. Simulation là một kỹ thuật thủ công để khám phá hành vi của mô hình. Refinement checking là một kỹ thuật để kiểm chứng rằng một mô hình là một bản tinh chỉnh của một mô hình khác.

Để kiểm chứng mô hình CSP# bằng PAT, cần thực hiện các bước sau: (1) Xây dựng mô hình CSP# của hệ thống. (2) Xác định các thuộc tính cần kiểm chứng. (3) Sử dụng PAT để kiểm chứng rằng mô hình đáp ứng các thuộc tính. Nếu mô hình không đáp ứng các thuộc tính, PAT sẽ cung cấp một phản ví dụ (counterexample) cho thấy lý do tại sao mô hình không đáp ứng các thuộc tính. Theo tài liệu gốc, sơ đồ toàn bộ quá trình kiểm chứng mô hình bao gồm yêu cầu, hệ thống, hình thức hóa, mô hình hóa, đặc tả thuộc tính, kiểm chứng mô hình và mô phỏng.

3.1. Sử dụng Model Checking trong PAT để Xác minh Thuộc tính

Model checking là một kỹ thuật kiểm chứng hình thức tự động kiểm chứng rằng một mô hình đáp ứng một đặc tả nhất định. PAT hỗ trợ nhiều loại đặc tả, bao gồm Linear Temporal Logic (LTL), Computation Tree Logic (CTL), và các đặc tả tùy chỉnh. Để sử dụng model checking trong PAT, cần cung cấp mô hình CSP# và một đặc tả của các thuộc tính cần kiểm chứng. PAT sẽ tự động khám phá không gian trạng thái của mô hình và kiểm chứng xem mô hình có đáp ứng đặc tả hay không.

3.2. Mô phỏng Mô hình CSP trong PAT để Khám phá Hành vi

Simulation là một kỹ thuật thủ công để khám phá hành vi của mô hình. PAT cung cấp một giao diện đồ họa cho phép người dùng tương tác với mô hình và quan sát hành vi của nó. Simulation có thể được sử dụng để hiểu rõ hơn về hành vi của mô hình và để xác định các lỗi tiềm ẩn. Qua quá trình simulation các nhà phát triển có thể tìm được những ví dụ kiểm chứng CSP#.

3.3. Kiểm tra Tinh chỉnh Refinement Checking để So sánh Mô hình

Refinement checking là một kỹ thuật để kiểm chứng rằng một mô hình là một bản tinh chỉnh của một mô hình khác. Điều này có thể được sử dụng để kiểm chứng rằng một phiên bản mới của một hệ thống tương thích với các phiên bản cũ. PAT hỗ trợ nhiều loại quan hệ tinh chỉnh, bao gồm trace refinement, failure refinement, và failure-divergence refinement. Qua refinement checking ta có thể biết được tính đúng đắn của hệ thống.

IV. Ứng dụng Thực tiễn Kiểm chứng CSP bằng PAT Nghiên cứu điển hình

Để minh họa cách kiểm chứng hệ thống tương tranh bằng CSP# và PAT, ta xét một ví dụ đơn giản: một hệ thống hàng đợi (queue). Hệ thống này bao gồm một producer tạo ra các item và một consumer tiêu thụ các item này từ hàng đợi. Chúng ta sẽ mô hình hóa hệ thống này bằng CSP# và sử dụng PAT để kiểm chứng các thuộc tính như: (1) Hàng đợi không bao giờ bị tràn. (2) Các item được tiêu thụ theo đúng thứ tự được tạo ra (FIFO). (3) Không có deadlock xảy ra.

Ví dụ này cho thấy cách CSP# và PAT có thể được sử dụng để kiểm chứng các thuộc tính quan trọng của hệ thống tương tranh. Bằng cách mô hình hóa hệ thống và sử dụng PAT để kiểm chứng các thuộc tính, ta có thể đảm bảo chất lượng phần mềm và phát hiện các lỗi tiềm ẩn trước khi chúng gây ra vấn đề trong thực tế. Theo tài liệu gốc, có thể xem xét các ví dụ CSP# để hiểu rõ hơn về cách mô hình hóa và kiểm chứng.

4.1. Mô hình hóa Hệ thống Hàng đợi bằng CSP

Để mô hình hóa hệ thống hàng đợi bằng CSP#, ta cần định nghĩa các tiến trình cho producer, consumer, và hàng đợi. Producer tạo ra các item và gửi chúng đến hàng đợi thông qua một kênh (channel). Consumer nhận các item từ hàng đợi thông qua một kênh khác. Hàng đợi lưu trữ các item và đảm bảo rằng chúng được tiêu thụ theo đúng thứ tự FIFO.

4.2. Đặc tả Thuộc tính của Hệ thống Hàng đợi

Sau khi mô hình hóa hệ thống hàng đợi, cần đặc tả các thuộc tính cần kiểm chứng. Trong ví dụ này, ta muốn kiểm chứng các thuộc tính như: (1) Hàng đợi không bao giờ bị tràn. (2) Các item được tiêu thụ theo đúng thứ tự được tạo ra (FIFO). (3) Không có deadlock xảy ra. Các thuộc tính này có thể được đặc tả bằng Linear Temporal Logic (LTL) hoặc các đặc tả tùy chỉnh.

4.3. Kiểm chứng và Phân tích Kết quả

Sử dụng PAT để kiểm chứng rằng mô hình hệ thống hàng đợi đáp ứng các thuộc tính đã đặc tả. Nếu PAT tìm thấy một vi phạm, nó sẽ cung cấp một phản ví dụ cho thấy lý do tại sao mô hình không đáp ứng các thuộc tính. Phân tích phản ví dụ và sửa đổi mô hình để đảm bảo rằng nó đáp ứng các thuộc tính.

V. So sánh PAT với Các Công cụ Kiểm chứng Mô hình Khác

Có nhiều công cụ kiểm chứng mô hình khác nhau có sẵn, mỗi công cụ có điểm mạnh và điểm yếu riêng. PAT là một công cụ mạnh mẽ và linh hoạt, hỗ trợ nhiều kỹ thuật kiểm chứng và có thể được sử dụng để kiểm chứng các hệ thống tương tranh phức tạp. Tuy nhiên, PAT có thể khó học và sử dụng cho người mới bắt đầu.

Một số công cụ kiểm chứng mô hình phổ biến khác bao gồm SPIN, NuSMV, và UPPAAL. SPIN là một công cụ mạnh mẽ và hiệu quả, nhưng nó chỉ hỗ trợ một số ít ngôn ngữ mô hình hóa. NuSMV là một công cụ dễ sử dụng, nhưng nó không hỗ trợ nhiều kỹ thuật kiểm chứng như PAT. UPPAAL là một công cụ đặc biệt phù hợp để kiểm chứng các hệ thống thời gian thực. Theo tài liệu gốc, PAT và SPIN có thể được so sánh kết quả kiểm chứng.

5.1. Ưu điểm và Nhược điểm của PAT so với SPIN NuSMV UPPAAL

PAT có ưu điểm là hỗ trợ ngôn ngữ CSP#, có tính biểu đạt cao và phù hợp cho mô hình hóa các hệ thống tương tranh phức tạp. PAT cũng hỗ trợ nhiều kỹ thuật kiểm chứng khác nhau. Tuy nhiên, PAT có thể khó học và sử dụng cho người mới bắt đầu. SPIN, NuSMV, và UPPAAL có thể dễ sử dụng hơn PAT, nhưng chúng có thể không hỗ trợ ngôn ngữ CSP# hoặc các kỹ thuật kiểm chứng cần thiết.

5.2. Lựa chọn Công cụ Kiểm chứng Mô hình Phù hợp

Việc lựa chọn công cụ kiểm chứng mô hình phù hợp phụ thuộc vào nhiều yếu tố, bao gồm ngôn ngữ mô hình hóa được sử dụng, các thuộc tính cần kiểm chứng, và kinh nghiệm của người dùng. PAT là một lựa chọn tốt cho các hệ thống tương tranh phức tạp được mô hình hóa bằng CSP#. Tuy nhiên, SPIN, NuSMV, hoặc UPPAAL có thể là lựa chọn tốt hơn cho các hệ thống đơn giản hơn hoặc cho người mới bắt đầu.

VI. Kết luận và Hướng phát triển trong Kiểm chứng CSP bằng PAT

CSP# và PAT cung cấp một phương tiện mạnh mẽ để mô hình hóa và kiểm chứng các hệ thống tương tranh. Bằng cách sử dụng CSP# để mô hình hóa hệ thống và PAT để kiểm chứng các thuộc tính, ta có thể đảm bảo chất lượng phần mềm và phát hiện các lỗi tiềm ẩn trước khi chúng gây ra vấn đề trong thực tế.

Trong tương lai, có nhiều hướng phát triển cho kiểm chứng CSP# bằng PAT. Một hướng là phát triển các kỹ thuật kiểm chứng hiệu quả hơn để xử lý các hệ thống tương tranh phức tạp hơn. Một hướng khác là phát triển các công cụ hỗ trợ người dùng dễ sử dụng hơn để mô hình hóa và kiểm chứng các hệ thống tương tranh. Theo tài liệu gốc, cần tiếp tục phát triển cách tiếp cận trích xuất mô hình trực tiếp từ mã nguồn C# đối với phạm trù xử lý tương tranh trong lập trình đa luồng.

6.1. Tóm tắt các Lợi ích và Hạn chế của CSP và PAT

CSP# cung cấp tính biểu đạt cao cho mô hình hóa hệ thống tương tranh, và PAT cung cấp các kỹ thuật kiểm chứng mạnh mẽ. Tuy nhiên, CSP# có thể khó học, và PAT có thể khó sử dụng. Cần tiếp tục nghiên cứu để cải thiện cả hai công cụ và làm cho chúng dễ tiếp cận hơn cho người dùng.

6.2. Các Hướng Nghiên cứu và Phát triển Tiềm năng

Có nhiều hướng nghiên cứu và phát triển tiềm năng cho kiểm chứng CSP# bằng PAT. Một hướng là phát triển các kỹ thuật trừu tượng hóa tự động để giảm kích thước của các mô hình CSP# phức tạp. Một hướng khác là phát triển các kỹ thuật kiểm chứng hiệu quả hơn để xử lý các hệ thống tương tranh phức tạp hơn. Cần tiếp tục nghiên cứu để mở rộng phạm vi áp dụng của kiểm chứng CSP# bằng PAT.

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

Chương 1 Kiểm chứng mô hình Sự phụ thuộc của chúng ta vào các hệ thống công nghệ thông tin ngày càng gia tăng. Các hệ thống này ngày càng trở lên phức tạp, tham gia vào hầu hết các hoạt động hàng ngày thông qua Internet và các loại hệ thống nhúng như điện thoại di động, máy tính cầm tay, ô tô. Theo thống kê ngay từ những năm 1995, mỗi người tiếp xúc với khoảng 25 thiết bị công nghệ thông tin hàng ngày [3]. Các dịch vụ như ngân hàng điện tử, mua sắm trực tuyến trở lên phổ biến.

Lượng tiền hàng ngày lưu thông qua Internet là khoảng 1012 triệu đô la Mỹ [3]. Khoảng 20% chi phí phát triển các phương tiện giao thông hiện đại như xe hơi, xe lửa tốc độ cao và máy bay được dành cho các hệ thống xử lý thông tin [3]. Sự phụ thuộc của chúng ta vào các hệ thống nhúng khiến độ tin cậy của chúng có tầm quan trọng lớn trong xã hội hiện đại. Bên cạnh cung cấp hiệu suất tốt thông qua thời gian đáp ứng, năng lực xử lý thì không xảy ra lỗi là một tiêu chí quan trọng trong việc đánh giá chất lượng.

Nhiều lỗi phần mềm hoặc phần cứng không đe dọa trực tiếp cuộc sống của chúng ta nhưng có thể gây ra các hậu quả nghiêm trọng về mặt tài chính. Một số ví dụ nổi tiếng về hậu quả gây ra do lỗi phần mềm và phần cứng như trong [3]. Lỗi dấu phảy động trong bộ xử lý Intel Pentinum II đầu những năm 90 gây ra thiệt hại khoảng 475 triệu đô la Mỹ để thay thế các bộ vi xử lý lỗi, danh tiếng của Intel cũng bị ảnh hưởng nghiêm trọng. Lỗi phần mềm trong hệ thống xử lý hành lý đã trì hoãn việc mở cửa sân bay Denver trong 9 tháng, hãng này phải chịu lỗ 1.1 triệu đô la Mỹ mỗi ngày.

Đối với một số hệ thống, lỗi có thể gây ra thảm họa. Một ví dụ điển hình là lỗi trong phần mềm điều khiển của tàu vũ trụ Ariane-5 vào tháng 4 năm 1996, 36 giây kể từ khi ra khỏi bệ phóng tàu bị rơi chỉ do lỗi chuyển đổi số thực 32 bit sang số nguyên 16 bit (Hình 1. Tầm quan trọng của các hệ thống công nghệ thông tin ngày càng tăng dẫn tới nhu cầu cấp thiết là đảm bảo được tính đúng đắn của hệ thống. Các hệ thống công nghệ thông tin hiện nay không chỉ tồn tại độc lập mà còn được nhúng trong các hệ lớn, kết nối và tương tác với các thành phần thuộc hệ thống khác.

Các hệ thống như thế rất dễ xảy ra lỗi. Đặc biệt, mô hình tương tác giữa các thành phần trong một số hệ thống như hệ tương tranh, lựa chọn không đơn định rất khó để đảm bảo tính đúng đắn với các kỹ thuật tiêu chuẩn. Độ phức tạp ngày càng tăng, cùng với TIEU LUAN MOI download : skknchat@gmail.1: Tàu vũ trụ Ariane-5 vào tháng 4 năm 1996 [3] áp lực giảm thời gian phát triển hệ thống khiến việc cung cấp các hệ thống công nghệ thông tin ít khiếm khuyết là một công việc đầy khó khăn và thử thách. Kiểm chứng Kỹ thuật kiểm chứng được sử dụng trong quá trình thiết kế các hệ thống công nghệ thông tin theo nhiều cách khác nhau.

Về cơ bản, kỹ thuật này sẽ xác định một thiết kế hoặc sản phẩm dưới phạm trù cần xem xét có thỏa mãn các thuộc tính nhất định không. Các thuộc tính được kiểm chứng có thể khá đơn giản, ví dụ như hệ thống có bao giờ rơi vào trạng thái bế tắc (deadlock) không, và hầu hết các thuộc tính đều được lấy ra từ đặc tả của hệ thống. Đặc tả của hệ thống quy định những gì hệ thống phải làm và không được làm, do đó là cơ sở cho mọi hoạt động kiểm chứng. Một lỗi được tìm thấy khi hệ thống không thỏa mãn một thuộc tính trong đặc tả.

Một hệ thống được coi là đúng khi mọi thuộc tính trong đặc tả của nó được thỏa mãn. Do đó tính đúng đắn của hệ thống luôn liên quan đến đặc tả của hệ thống đó. Sơ đồ quy trình kiểm chứng được mô tả trong Hình 1. Đánh giá ngang hàng (peer reviewing) và kiểm thử (testing) là hai kỹ thuật phổ biến được sử dụng trong thực tế để đảm bảo chất lượng phần mềm.

Tuy nhiên, hai kỹ thuật này có chung một nhược điểm lớn là không thể xác định chính xác được tính đúng của hệ thống. Trong khi đánh giá ngang hàng là kỹ thuật chủ yếu dựa trên kinh nghiệm của người tham gia đánh giá thì kiểm thử chỉ có thể được tiến hành trên một số nhánh thực thi của hệ thống. Tiến hành kiểm thử trên đầy đủ các nhánh thực thi là không thể. Vì thế hai kỹ thuật này chỉ có khả năng phát hiện lỗi mà không thể khẳng định là hoàn toàn không còn lỗi trong hệ thống.

Đối với các hệ thống phần mềm phức tạp đòi hỏi độ tin cậy cao, sử dụng các kỹ thuật trên rõ ràng không đáp ứng được yêu cầu. Khi đó, các phương pháp kiểm chứng hình thức (formal verification) được coi là có nhiều tiềm năng. Bản chất của phương pháp kiểm chứng hình thức là áp dụng toán học vào việc mô hình hóa và phân tích các hệ thống công nghệ thông tin, đảm bảo tính đúng đắn cho hệ thống với sự chặt chẽ của toán học. Tiềm năng to lớn của phương pháp hình thức dẫn tới sự gia tăng nhanh chóng việc sử dụng phương pháp này trong kiểm chứng các hệ thống phức TIEU LUAN MOI download : [e-mail] 10 Đặc tả hệ thống (System specification) Thiết kế Thuộc tính (Design) (Properties ) Sản phẩm / bản thử (Product / Prototype) Tìm thấy lỗi Kiểm chứng (Verification) Không tìm thấy lỗi Hình 1.2: Sơ đồ quy trình kiểm chứng [3] tạp.

Theo thống kê, hiện nay các phương pháp hình thức được sử dụng ở một số dạng khác nhau, trong khoảng 10% đến 15% các dự án phần mềm [3]. Trong công nghệ phần mềm, kiểm chứng hình thức là khái niệm về việc sử dụng các phương pháp hình thức (formal methods) trong toán học để chứng minh hoặc phủ định tính đúng đắn của hệ thống dựa trên một đặc tả hình thức (formal specification) hoặc thuộc tính hình thức (formal property) của hệ thống đó. Quá trình kiểm chứng được tiến hành bằng các chứng minh trên một mô hình toán học trừu tượng của hệ thống, tính chính xác của mô hình toán học này phụ thuộc vào quá trình mô hình hóa. Một số dạng mô hình toán học thường được sử dụng để mô hình hóa hệ thống là: process algebra, máy trạng thái hữu hạn (finite state machines), hệ thống dịch chuyển nhãn (labelled transition systems), mạng Petri (petri nets).

Một cách tiếp cận sớm và đặc thù của kiểm chứng hình thức là kiểm chứng mô hình, quá trình kiểm chứng mô hình bao gồm các bước tiến hành để kiểm tra một cách toàn diện trên mô hình toán học của hệ thống. Nội dung luận văn tập trung vào các phương pháp mô hình hóa hệ thống để phục vụ kiểm chứng mô hình cho các hệ tương tranh. Các kỹ thuật như kiểm thử thường đem lại hiệu quả rất thấp vì lỗi trong hệ tương tranh thường không có xu hướng lặp lại [1]. Trong phát triển phần mềm, các khiếm khuyết của hệ thống được phát hiện càng sớm càng tốt vì chi phí sửa chữa lỗi trong giai đoạn bảo trì cao hơn trong giai đoạn thiết kế ban đầu khoảng 500 lần (Hình 1.

Do đó mục tiêu quan trọng của kiểm chứng mô hình là áp dụng sớm để kiểm chứng ngay trong giai đoạn thiết kế hệ thống. Trong giai đoạn này, mô hình toán học của hệ thống được xây dựng dựa TIEU LUAN MOI download : [e-mail] 11 trên nội dung bản thiết kế hệ thống và các thuộc tính cần kiểm tra được lấy ra từ đặc tả hoặc các yêu cầu thiết kế.3: Lỗi và chi phí sửa lỗi trong phát triển phần mềm [3] 1. Tổng quan về kiểm chứng mô hình Một vài năm trở lại đây, trong khoa học máy tính, kiểm chứng mô hình (model checking) bắt đầu được sử dụng rộng rãi trong kiểm định các hệ thống phần mềm và các hệ thống điều khiển điện tử [9]. Kiểm chứng mô hình là một nhóm các kỹ thuật kiểm định tự động một cách hình thức một mô hình với đặc tả các tính năng của mô hình đó [10].

Mô hình của một hệ thống bao gồm tập hợp các trạng thái và tập hợp các chuyển dịch giữa các trạng thái đó. Thông thường, một đặc tả hoặc một tính năng của hệ thống được viết dưới dạng công thức lôgic và thường được diễn tả bằng một ngôn ngữ lôgic thời gian [11, 14, 22]. Ý tưởng cơ bản là chứng minh xem một mô hình có thỏa mãn các tính năng đã mô tả trước đó về nó hay không bằng cách duyệt toàn bộ không gian trạng thái của mô hình đó. Nếu mô hình không thỏa mãn một tính năng nào đó, thuật toán cần phải đưa ra một phản ví dụ.

Phản ví dụ là một tập hợp các giá trị của biến đầu vào để chỉ ra rằng với một đầu vào như thế thì mô hình sẽ chạy không đúng như tính năng đã được mô tả. Các nghiên cứu đầu tiên về kiểm chứng mô hình được thực hiện bởi Edmund Melson Clarke và Ernest Allen Emerson cũng như Jean-Pierre Queille và Joseph Sifakis Jean-Pierre. Clarke, Emerson và Sifakis đã được nhận giải thưởng Turing năm 2007 cho các đóng góp của họ về kiểm chứng mô hình. Đặc tả thuộc tính quy định hệ thống phải làm gì và không được làm gì trong TIEU LUAN MOI download : [e-mail] 12 khi mô hình mô tả hành vi của hệ thống đó.

Hành vi của hệ thống được mô tả trên mô hình một cách rõ ràng, không mập mờ sử dụng lý thuyết toán học. Mô hình hệ thống thường được sinh tự động từ đặc tả mô hình (sử dụng các ngôn ngữ mô hình hóa). Do chỉ thực hiện dựa trên mô hình của hệ thống nên sự thiếu chính xác của mô hình có thể dẫn tới các kết quả không đầy đủ, không rõ ràng, và không nhất quán với đặc tả của hệ thống. Những vấn đề trên thường chỉ được phát hiện rất muộn sau giai đoạn thiết kế.

Mô hình hệ thống thường đi kèm các thuật toán để kiểm tra tất cả các trạng thái có trong mô hình đó để xem chúng có thỏa mãn một thuộc tính mong muốn nào đó không. Nếu bắt gặp một trạng thái vi phạm thuộc tính cần xem xét, bộ kiểm tra mô hình sẽ cung cấp một phản ví dụ để chỉ ra làm thế nào mô hình có thể đạt đến trạng thái đó.