- 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. - Đại học Quốc gia Hà Nội Luận văn ThS. - Trình bày các vấn đề cấp thiết trong kiểm chứng để xác định tính đúng đắn của hệ thống phần mềm, nhất là đối với các hệ thống tương tranh và lựa chọn cách tiếp cận kiểm chứng mô hình. - Đi sâu vào hai vấn đề chính trong kiểm chứng mô hình là mô hình hóa hệ thống và đặc tả các thuộc tính của hệ thống. - Hiện nay có nhiều phương pháp giúp mô hình hóa cũng như đặc tả các thuộc tính của hệ thống, nhưng luận văn lựa trình bày hai phương pháp cơ sở là sử dụng hệ dịch chuyển để mô hình hóa và lôgic thời gian tuyến tính để đặc tả các thuộc tính của hệ thống. - Trình bày nội dung về hệ tương tranh: khái niệm, các thuộc tính, mô hình tương tác và các khó khăn khi muốn xác định tính đúng đắn. - Một số cơ chế thực thi, tương tác trong hệ tương tranh và cách mô hình hóa các cơ chế đó bằng hệ dịch chuyển cũng được trình bày trong chương này. - Cụ thể luận văn xem xét các cơ chế thực thi, tương tác sau: Xử lý đan xen (Interleaving). - Xử lý song song đồng bộ (Synchronous Parallelism). - Trình bày về một ngôn ngữ đặc tả mô hình hệ tương tranh là CSP#, ngôn ngữ này được tích hợp vào trong bộ công cụ hỗ trợ kiểm chứng PAT. - Với các nội dung tìm hiểu về ngôn ngữ CSP# luận văn đề xuất một cách tiếp cận trích xuất mô hình từ mã nguồn C# cho bài toán xử lý tương tranh trong lập trình đa luồng. - Tiến hành thử nghiệm kiểm chứng mô hình một hệ thống sử dụng ngôn ngữ đặc tả mô hình CSP# và công cụ hỗ trợ PAT, so sánh kết quả kiểm chứng của PAT với SPIN qua một số bài toán... - Kỹ thuật kiểm chứng. - Kiểm chứng mô hình. - Hệ thống tương tranh. - Ngôn ngữ đặc tả. - Để đem lại hiệu quả công việc cao nhất và tiết kiệm thời gian, chi phí cho doanh nghiệp, các hệ thống phần mềm khi đưa vào ứng dụng phải đảm bảo các yêu cầu nghiêm ngặt về hiệu năng xử lý và tiết kiệm năng lượng. - Một giải pháp là sử dụng các hệ thống xử lý tương tranh giúp tận dụng tối đa tài nguyên phần cứng, cho phép thực hiện nhiều tác vụ cùng lúc.. - Tuy nhiên, trong phát triển phần mềm, việc xác định tính đúng đắn cho các hệ thống xử lý tương tranh như vậy thường 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 trong hệ thống xử lý tương tranh 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ử, khi đó sử dụng các kỹ thuật kiểm chứng hình thức là cần thiết. - Nội dung của luận văn sẽ tập trung giới thiệu hướng tiếp cận kiểm chứng mô hình cho hệ xử lý tương tranh, đi sâu vào phương pháp mô hình hóa hệ thống. - Một ngôn ngữ mô hình hóa cụ thể được giới thiệu trong luận văn là Communicating Sequential Processes Sharp (CSP. - các mô hình đặc tả bằng ngôn ngữ này được sử dụng trong phần kiểm chứng thử nghiệm với bộ công cụ Process Analysis Toolkit (PAT).. - Chương 1 của luận văn giới thiệu tổng quan về kiểm chứng mô hình, các phương pháp mô hình hóa và đặc tả thuộc tính của hệ thống (sử dụng hệ dịch chuyển và logic thời gian tuyến tính).. - Trong chương 2 luận văn tiếp tục giới thiệu tổng quan về hệ thống tương tranh, các cơ chế thực thi, tương tác trong hệ tương tranh, mô hình hóa các cơ chế thực thi, tương tác trên bằng hệ dịch chuyển để phục vụ kiểm chứng mô hình. - Tuy nhiên trong thực tế, 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. - Chương 3 sẽ trình bày về ngôn ngữ mô hình hóa CSP. - một ngôn ngữ phù hợp để đặc tả mô hình các hệ xử lý tương tranh.. - Trong chương 3 luận văn cũng đề xuất một cách tiếp cận trích xuất mô hình trực tiếp từ mã nguồn C Sharp (C#) đối với phạm trù xử lý tương tranh trong lập trình đa luồng.. - Kết quả của quá trình trích xuất là mô hình xử lý tương tranh trong mã nguồn dưới dạng đặc tả bằng CSP#. - Đề xuất này nhằm phục vụ mục tiêu kiểm chứng mô hình trực tiếp trên mã nguồn C#. - Phần cuối của luận văn ở chương 4 tiến hành thử nghiệm mô hình hóa và kiểm chứng một hệ tương tranh, sử dụng ngôn ngữ mô hình hóa CSP# và công cụ hỗ trợ kiểm chứng PAT.. - Kowalewski Model checking c source code for embed- ded systems", International Journal on Software Tools for Technology Trans- fer (STTT), vol. - Concretizing the convergence of model checking and program analysis", In Conf. - "Bounded Model Checking Using Satisfiability Solving", Formal Methods in System Design 19(1), pp. - Visser Addressing dynamic issues of program model checking", Proceedings of the 8th international SPIN workshop on Model checking of software, Toronto, Ontario, Canada: Springer-Verlag New York, Inc., pp. - [13] G.Barrett Model checking in practice: The T9000 Virtual Chan- nel Processor", IEEE Transactions on Software Engineering . - [17] Jun Sun, Yang Liu, Jin Song Dong Model Checking CSP Revisited:. - Pressburger Model checking java programs us- ing java pathfinder", International Journal on Software Tools for Technology Transfer (STTT), vol. - [25] Yang Liu Model Checking Concurrent and Real-time Systems: the PAT Approach", PhD thesis.