Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình bằng kiểm duyệt mô hình

- Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình bằng kiểm duyệt mô hình.
- Trình bày về cơ sở lý thuyết của kiểm duyệt mô hình (Model checking): khái niệm và ý nghĩa của kiểm duyệt mô hình, quy trình hoạt động của kiểm duyệt mô hình, đặc trưng của kiểm duyệt mô hình, điểm mạnh và điểm yếu của kiểm duyệt dựa trên mô hình sử dụng logic thời gian (Temporal Logic) mô tả các thuộc tính cần kiểm chứng.
- Nghiên cứu về công cụ Spin, giao diện Xspin, và ngôn ngữ mô hình hóa Promela, máy trạng thái hữu hạn.
- Tiến hành xây dựng tiến trình đồng hồ, mô hình hóa hệ thống báo động, báo cháy, kết hợp tiến trình đồng hồ với kỹ thuật kiểm duyệt mô hình để kiểm chứng tính đúng đắn của hệ thống đó..
- Hệ thống tính toán.
- Kiểm chứng mô hình Content..
- Ngày nay chúng ta phụ thuộc rất nhiều vào hệ thống máy tính cả trong sản xuất lẫn đời sống hàng ngày.
- Các hệ thống này cần phải đảm bảo sự tin cậy và an toàn khi sử dụng.
- Do đó chúng cần phải được kiểm duyệt kỹ càng ngay từ mô hình của hệ thống để đảm bảo hệ thống hoạt động chính xác tránh gây thiệt hại cả về con người lẫn tiền của..
- Kỹ thuật kiểm chứng mô hình đã được sử dụng để kiểm chứng cho các mô hình hệ thống trong thực tế.
- Nội dung đề tài nghiên cứu về kỹ thuật kiểm chứng mô hình (Model Checking), dùng công cụ Spin để thực hiện kiểm chứng mô hình hệ thống báo động, báo cháy, sử dụng ngôn ngữ mô hình hóa Promela để mô hình hóa hệ thống báo động, báo cháy, và mô tả các thuộc tính cần kiểm chứng qua Logic thời gian tuyến tính để kiểm chứng tính đúng đắn của hệ thống báo động, báo cháy qua mô hình của nó..
- Chương 1 trình bày về cơ sở lý thuyết của kiểm duyệt mô hình (Model checking)..
- Chương 2 trình bày về công cụ Spin, giao diện Xspin, và ngôn ngữ mô hình hóa Promela..
- Chương 3 xây dựng tiến trình đồng hồ, kết hợp kỹ thuật kiểm duyệt mô hình và tiến trình đồng hồ để kiểm chứng tính đúng đắn của hệ thống báo động, báo cháy.
- Khái niệm và ý nghĩa của kiểm duyệt mô hình.
- “Kiểm duyệt mô hình (Model checking) là một kỹ thuật được tự động hóa nhằm đưa ra mô hình hữu hạn trạng thái của hệ thống và thuộc tính hình thức, kỹ thuật này sẽ kiểm tra có hay không thuộc tính được thõa mãn bởi mô hình của hệ thống” [5]..
- Kiểm duyệt mô hình cho phép kiểm duyệt phần mềm không còn lỗi và thực hiện đúng chức năng đặt ra.
- Nó kiểm tra mọi khả năng có thể của trạng thái hệ thống..
- Quy trình hoạt động của kiểm duyệt mô hình.
- Hình 1.1: Hoạt động của phương pháp kiểm duyệt mô hình.
- Mô hình của hệ thống được xây dựng từ đặc tả của hệ thống.
- Mô hình này thể hiện hành vi của hệ thống và có thể được viết bởi ngôn ngữ C, Java, hay các ngôn ngữ mô tả phần cứng..
- Đặc trƣng của kiểm duyệt mô hình.
- Quá trình kiểm duyệt một mô hình có thể chia thành những pha như sau:.
- Pha mô hình hóa (Modeling)..
- Điểm mạnh và điểm yếu của kiểm duyệt dựa trên mô hình Kiểm duyệt mô hình có một vài điểm mạnh như [2]:.
- Là phương pháp kiểm chứng tổng quan được áp dụng cho các ứng dụng trong phạm vi lớn như hệ thống nhúng, công nghệ phần mềm, thiết kế phần cứng,….
- Hỗ trợ kiểm duyệt cục bộ, các thuộc tính có thể được kiểm tra riêng lẻ, từ đó tập chung kiểm duyệt các thuộc tính quan trọng trước mà không cần thiết đặc tả hệ thống hoàn chỉnh..
- Kiểm duyệt mô hình có nền tảng của toán học, nó dựa trên lý thuyết thuật toán đồ thị, cấu trúc dữ liệu và logic..
- Bên cạnh những ưu điểm trên, phương pháp kiểm duyệt mô hình cũng có những yếu điểm như [2]:.
- Kiểm duyệt mô hình kiểm chứng mô hình của hệ thống chứ không phải bản thân hệ thống, mọi kết quả đạt được là về mặt mô hình hệ thống, do đó cần có những kỹ thuật khác hỗ trợ như kiểm duyệt để tìm ra lỗi chế tạo (trong phần cứng) và lỗi lập trình (phần mềm)..
- Có rất nhiều mô hình được sử dụng trong kiểm chứng phần mềm, trong đó có mô hình máy hữu hạn trạng thái – Finite State Machines (FSM)..
- Mô hình máy hữu hạn trạng thái FSM được sử dụng để mô tả hoạt động của nhiều hệ thống trong thực tế..
- Promela là ngôn ngữ mô hình hóa dùng để mô tả hệ thống đồng thời [3].
- Chẳng hạn như hệ thống điện thoại, chương trình giao tiếp đa luồng, giao thức mạng,… Nó là ngôn ngữ không tất định, có cú pháp và ngữ nghĩa tương tự ngôn ngữ C [9]..
- Tiến trình.
- Việc sử dụng atomic nhằm giảm sự phức tạp của mô hình cần kiểm duyệt..
- Spin (Simple Promela Interpreter) là một công cụ kiểm chứng, nó hỗ trỡ ngôn ngữ đặc tả hệ thống Promela.
- Spin được dùng để theo dõi những lỗi logic ở trong những bản thiết kế của hệ thống phân tán như hệ điều hành, giao thức truyền thông dữ liệu, thuật toán song song, giao thức báo hiệu tàu điện,...Ta có thể sử dụng Spin mà không cần phải dựng lên mô hình dưới dạng đồ thị trạng thái [5]..
- Ngôn ngữ đặc tả Promela được sử dụng để diễn tả mô hình hệ thống và thuộc tính của nó để kiểm chứng mô hình..
- Spin có thể mô phỏng sự thực thi của hệ thống..
- Việc sử dụng Spin rất đơn giản, hiệu quả cao, và nó phù hợp để kiểm chứng hệ thống phân tán..
- Spin không hỗ trợ kiểm chứng hệ thống vô hạn trạng thái..
- Mô hình hệ thống trong SPIN.
- Các hệ thống được mô hình hóa trong Spin như là một tập các tiến trình (mạng các Automata), được chạy song song theo chế độ đan xen và giao tiếp với nhau qua các thông điệp hay qua chia sẻ các biến..
- Kiểm chứng (Verify).
- Khi sử dụng assertion bị hạn chế trong việc biểu diễn tính chất của mô hình.
- Từ đó cần dùng đến logic thời gian tuyến tính LTL, LTL mạnh mẽ hơn trong việc biểu diễn tính chất của mô hình hệ thống..
- Biểu diễn tính chất bất biến của hệ thống bằng LTL.
- Trong nhiều trường hợp, hệ thống xây dựng phải thỏa mãn một tính chất bất biến nào đó.
- Có những tính chất mà ta mong muốn nó không bao giờ được xuất hiện trong hệ thống.
- Trong Spin ta chỉ cần biểu diễn tính chất của hệ thống dưới dạng một biểu thức LTL sau đó đưa vào Spin, Spin sẽ tự động chuyển biểu thức LTL sang cấu trúc never claim của Promela dùng vào việc kiểm chứng..
- Bàn về kỹ thuật kiểm duyệt mô hình cho hệ thống không có ràng buộc thời gian và có ràng buộc thời gian, có thể đưa ra nhận xét: Với kỹ thuật kiểm duyệt mô hình để kiểm duyệt hệ thống có ràng buộc thời gian thường phức tạp, tốn thời gian nghiên cứu.
- Ngoài ra nó còn đòi hỏi thời gian chạy lâu và chỉ áp dụng cho những hệ thống nhỏ, bởi hệ thống càng lớn thì số trạng thái càng tăng dẫn tới việc bùng nổ không gian trạng thái.
- Với kỹ thuật kiểm duyệt mô hình để kiểm duyệt hệ thống không có ràng buộc thời gian dễ tìm hiểu hơn, và hạn chế được phần nào vấn đề bùng nổ không gian trạng thái.
- Hơn nữa, các kỹ thuật kiểm chứng trợ giúp việc kiểm chứng các tính chất thời gian tổng quát, trong khi các hệ thống có ràng buộc thời gian thực tế thường chỉ đòi hỏi kiểm chứng các tính chất đơn giản ở dạng deadline.
- Từ đó có thể sử dụng kỹ thuật kiểm duyệt mô hình cho hệ thống không có ràng buộc thời gian.
- kết hợp với kỹ thuật xây dựng biến, tiến trình đồng hồ để kiểm chứng hệ thống có ràng buộc thời gian, cụ thể là hệ thống báo động, báo cháy..
- Để có thể kiểm chứng hệ thống thời gian thực cần kết hợp kỹ thuật kiểm duyệt mô hình cho hệ thống không có ràng buộc thời gian với tiến trình đồng hồ.
- Tiến trình đồng hồ được xây dựng bởi ngôn ngữ mô hình hóa Promela như sau:.
- Với tiến trình đồng hồ được xây dựng như trên, khi áp dụng vào mô hình hệ thống báo động, báo cháy có ràng buộc thời gian thực là “hệ thống phải báo động sau 5 giây kể từ khi nhận được thông báo động”.
- Hệ thống báo động, báo cháy mức trừu tƣợng 3.2.1.
- Mô tả hệ thống mức trừu tƣợng.
- Hệ thống báo động bao gồm các Sensors để phát hiện động (từ môi trường), bảng điều khiển Control Panel, và chuông báo Alarm.
- Hệ thống này không chỉ có mục đích báo động mà còn báo cháy..
- Thuộc tính cần kiểm chứng ở đây là bất cứ khi nào có động thì hệ thống phải báo.
- Kiến trúc trừu tượng của hệ thống báo động, báo cháy:.
- Hình 3.1: Kiến trúc mức 1 của hệ thống báo động, báo cháy.
- Mô hình Promela cho hệ thống báo động, báo cháy mức trừu tƣợng và kiểm chứng thuộc tính đơn giản.
- Mô hình cho hệ thống bằng ngôn ngữ Promela áp dụng cho hệ thống có 5 Sensors bao gồm: Các tiến trình environment.
- Hệ thống có mục đích báo động, báo cháy tương ứng với hai sự kiện breaker (trộm) và fire (cháy).
- Hình 3.2: Kết quả khi mô phỏng mô hình hệ thống báo động, báo cháy mức trừu tượng.
- Sau khi chạy mô phỏng chương trình như trên, cần kiểm tra tính chất mà hệ thống phải thỏa mãn bằng việc chạy verify.
- Tính chất cần kiểm chứng của hệ thống báo động, báo cháy mức trừu tượng là:.
- “bất cứ khi nào có động, hệ thống đều phải báo”.
- Kết quả chạy verify cho thấy không có lỗi vi phạm do vậy hệ thống thỏa mãn tính chất cần kiểm tra..
- Hình 3.3: Kết quả kiểm chứng mô hình hệ thống báo động, báo cháy Phân tích kết quả trên thấy errors: 0 nên mô hình đưa ra thỏa mãn thuộc tính đã nêu..
- Hệ thống báo động, báo cháy mức 2 3.3.1.
- Mô tả hệ thống mức 2.
- Hệ thống báo động, báo cháy mức 2 là sự mở rộng của mức trừu tượng.
- Ở mức 2 của hệ thống được xây dựng thêm tiến trình đồng hồ (clock).
- Nói cách khác, nhờ xây dựng tiến trình đồng hồ (clock) và biến đồng hồ (time) ta có thể đưa ràng buộc thời gian thực vào hệ thống báo động, báo cháy qua assertion.
- Từ mô tả hệ thống như trên ta có thể đưa ra kiến trúc hệ thống như sau:.
- Hình 3.4: Kiến trúc mức 2 của hệ thống báo động, báo cháy.
- Mô hình Promela cho hệ thống báo động, báo cháy mức 2 và kiểm chứng thuộc tính đơn giản.
- Từ mô tả hệ thống như trên, ta xây dựng mô hình cho hệ thống bằng ngôn ngữ Promela áp dụng cho hệ thống có 5 Sensors bao gồm các biến và tiến trình như ở mức trừu tượng và được bổ sung thêm một vài biến, các thành phần trong các tiến trình ở mức trừu tượng, và tiến trình clock..
- Hình 3.5: Kết quả khi mô phỏng mô hình hệ thống báo động, báo cháy mức trừu tượng Thuộc tính cần kiểm chứng ở đây là: “bất cứ khi nào có động, hệ thống đều phải báo.
- Và hệ thống cần đảm bảo “thời gian từ khi có động đến khi chuông phát báo động không được vượt quá 5 giây.
- Hình 3.6: Kết quả kiểm chứng mô hình hệ thống báo động, báo cháy Phân tích kết quả trên thấy errors: 0 nên mô hình đưa ra thỏa mãn các thuộc tính đã nêu..
- Với mục tiêu ban đầu của đề tài: “Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình bằng kiểm duyệt mô hình”, tác giả đã nghiên cứu về kỹ thuật kiểm duyệt mô hình (Model Checking), tìm hiểu về công cụ kiểm chứng Spin, ngôn ngữ mô hình hóa Promela, xây dựng tiến trình đồng hồ (clock), đồng thời đã xây dựng mô hình và kiểm duyệt cho hệ thống báo động, báo cháy, đến nay đã đạt được một số kết quả như sau:.
- Nghiên cứu về kỹ thuật kiểm duyệt mô hình (Model Checking)..
- Tìm hiểu về công cụ kiểm chứng Spin cũng như giao diện Xspin và ngôn ngữ mô hình hóa Promela..
- Xây dựng biến đồng hồ (time) và tiến trình đồng hồ (clock) để đo thời gian khi cần thiết, bằng cách này tác giả đã kết hợp tiến trình đồng hồ với kỹ thuật kiểm duyệt mô hình dành cho hệ thống không có ràng buộc thời gian để kiểm chứng hệ thống có ràng buộc thời gian..
- Xây dựng mô hình cho hệ thống báo động, báo cháy bằng ngôn ngữ Promela theo hướng chi tiết hóa dần (incremental)..
- Sử dụng kỹ thuật kiểm duyệt mô hình kết hợp tiến trình đồng hồ xây dựng được để kiểm duyệt tính đúng đắn của hệ thống báo động, báo cháy sử dụng công cụ kiểm chứng Spin..
- Quá trình kiểm chứng tác giả đã đưa vào hệ thống 2 thuộc tính cần kiểm chứng là: “bất cứ khi nào có động, hệ thống đều phải báo” và “thời gian từ khi có động tới khi báo động không được vượt quá 5 giây”..
- Tuy nhiên trong luận văn còn chưa thực hiện được việc mô hình hóa hệ thống báo động, báo cháy ở mức chi tiết nhất, và chương trình xây dựng được chưa có giao diện.
- Mô hình hóa hệ thống báo động, báo cháy ở mức chi tiết hơn để hệ thống gần sát với hệ thống thực tế..
- Kiểm duyệt mọi trường hợp có thể của hệ thống để đảm bảo hệ thống hoạt động được đầy đủ chức năng..
- Nghiên cứu phương pháp kiểm tra tính đúng đắn của việc xây dựng mô hình từ mô tả của hệ thống.