I. Tổng Quan Kiểm Định Mô Hình Hệ Thống Thông Tin UTT
Ngày nay, chúng ta phụ thuộc rất nhiều vào hệ thống máy tính (phần cứng và phần mềm) 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. Hơn nữa việc áp dụng kỹ thuật kiểm chứng hệ thống qua mô hình hệ thống sẽ làm tăng hiệu quả kinh tế bởi nhờ có kiểm chứng mô hình mà nhà sản xuất có thể xác định sớm các lỗi trong hệ thống nên chi phí vào quá trình kiểm thử hoặc khắc phục lỗi sẽ giảm đáng kể. Kỹ thuật kiểm định mô hình hệ thống thông tin đã được sử dụng để kiểm chứng cho các mô hình hệ thống trong thực tế.
1.1. Khái niệm và ý nghĩa của kiểm duyệt mô hình
Theo Clarke và Emerson – 1981, kiểm duyệt mô hình được định nghĩa: “Kiểm duyệt mô hình 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]. Trong giai đoạn thiết kế phần mềm và phần cứng của các hệ thống phức tạp hiện nay, các chuyên gia dành rất nhiều thời gian cho việc kiểm chứng hơn là việc xây dựng hệ thống. Có rất nhiều kỹ thuật đã được tìm ra để làm tăng phạm vi ứng dụng của kiểm chứng. Các phương pháp hình thức là một trong những kỹ thuật đó. Nó được tích hợp vào việc kiểm chứng trong quá trình thiết kế, để đưa ra những kỹ thuật kiểm chứng hiệu quả và làm giảm thời gian kiểm chứng hệ thống. Một trong những phương pháp hình thức mạnh mẽ nhất là kiểm duyệt mô hình [1, 2].
1.2. Quy trình hoạt động của 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. Sự đặc tả thuộc tính yêu cầu những gì hệ thống nên làm và những gì không nên làm trong khi mô hình mô tả hệ thống hoạt động như thế nào? Kiểm duyệt mô hình sẽ kiểm tra tất cả các trạng thái hệ thống liên quan xem có thỏa mãn không, nếu không thỏa mãn sẽ đưa ra một phản ví dụ - một trạng thái của hệ thống không thỏa mãn - cho thấy cách đạt đến trạng thái không thỏa mãn, sử dụng phản ví dụ cùng với sự mô phỏng ta sẽ có được những thông tin gỡ lỗi và từ đó sẽ có được mô hình phù hợp.
II. Cách Xác Định Vấn Đề Trong Hệ Thống Thông Tin UTT
Để phát huy được hết hiệu quả của kỹ thuật kiểm định mô hình hệ thống thông tin, cần có công cụ kiểm chứng đi kèm để hỗ trợ quá trình kiểm chứng. Các công cụ kiểm chứng hiện nay hay dùng như Spin, Kronos, NuSMV,… Công cụ Spin mặc dù rất đơn giản, gọn nhẹ nhưng có tầm ảnh hưởng lớn trong phát triển phần mềm cho các hệ thống phức tạp như hệ thời gian thực, hệ thống nhúng, hệ tương tác, … Từ thực tiễn đó, chúng tôi chọn đề 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” nhằm mục đích là tiếp cận, nghiên cứu phương pháp kiểm chứng mô hình, dùng công cụ kiểm chứng Spin và ngôn ngữ mô hình hóa Promela để kiểm chứng tính đúng đắn của hệ thống.
2.1. Đặ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): Xây dựng mô hình cho hệ thống bằng các mô hình hóa hệ thống sử dụng ngôn ngữ mô tả mô hình của công cụ kiểm duyệt. Sau đó kiểm tra sự đúng đắn và đánh giá nhanh mô hình bằng sự mô phỏng. Hình thức hóa thuộc tính cần được kiểm duyệt sử dụng ngôn ngữ đặc tả thuộc tính. Pha thực thi (Running): Sử dụng chương trình kiểm duyệt để kiểm tra tính hợp lệ của thuộc tính trên mô hình hệ thống vừa xây dựng. Nếu thuộc tính bị vi phạm thì tiến hành phân tích phản ví dụ bằng sự mô phỏng; Tinh chỉnh mô hình, bản thiết kế, hoặc thuộc tính; Lặp lại toàn bộ các pha. Nếu tràn bộ nhớ thì cố gắng giảm bớt mô hình và thử lại.
2.2. Các thuộc tính điển hình kiểm tra bằng kiểm duyệt mô hình
Các thuộc tính điển hình có thể được kiểm tra bằng kiểm duyệt mô hình thông thường là: Kết quả sinh ra có đúng không?, hệ thống có lâm vào trạng thái bế tắc không?. Thậm chí các thuộc tính trên thời gian cũng có thể được kiểm tra như: có thể xảy ra bế tắc trong vòng 1 giờ sau khi hệ thống khởi động lại? Hoặc sự phản hồi có được nhận lại trong vòng 10 phút? … Mô hình của hệ thống thông thường được sinh ra tự động từ một sự mô tả mô hình được đặc tả trên các ngôn ngữ lập trình như C, Java hoặc ngôn ngữ mô tả phần cứng như Verilog.
III. Phương Pháp Kiểm Định Mô Hình Hệ Thống Thông Tin
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ó. Phương pháp nghiên cứu: Phương pháp thu thập tài liệu: Các thông tin sử dụng trong luận văn được thu thập từ các nguồn: Sách tham khảo, giáo trình, giáo án, các bài báo.
3.1. Sử dụng Logic thời gian mô tả thuộc tính cần kiểm chứng
Các biểu thức temporal logic không chỉ xét đến những dãy trạng thái đơn, mà còn xét đến những dãy trạng thái phức tạp trong đó từ một trạng thái có thể có nhiều trạng thái ngay tiếp sau nó. Trong các nghiên cứu về kiểm duyệt mô hình, có hai loại logic thời gian hay được xem xét là LTL (Linear Temporal Logic) và CTL (Branching Temporal Logic) [2]. LTL (Linear Temporal Logic): Logic thời gian tuyến tính. Thời gian có cấu trúc tuyến tính, mỗi trạng thái chỉ có một trạng thái ngay tiếp sau nó. CTL (Branching Temporal Logic): Logic thời gian rẽ nhánh. Thời gian có cấu trúc tuyến tính, mỗi trạng thái có nhiều trạng thái ngay tiếp sau nó.
3.2. Ngữ nghĩa công thức LTL thể hiện thuộc tính của đường
Ngữ nghĩa công thức LTL thể hiện cho các thuộc tính của đường - path (hay truy vết của chúng). Tức là một đường có thể thỏa mãn một công thức LTL hoặc không. Ngữ nghĩa của công thức LTL φ được định nghĩa như là một ngôn ngữ Words(φ) bao gồm mọi dãy vô hạn trên tập chữ cái mà thỏa mãn φ. Mọi công thức LTL liên kết các thuộc tính LT đơn. Ngữ nghĩa của nó được mở rộng để giải thích các đường và các trạng thái của hệ thống truyền.
IV. Ứng Dụng Thực Tế Kiểm Định Mô Hình Tại UTT Hà Nội
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 trung 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. Quá trình kiểm duyệt sau không ảnh hưởng đến các lỗi đã được phát hiện trước đó. Cung cấp các thông tin có ý nghĩa cho việc gỡ lỗi khi phát hiện một thuộc tính không thỏa mãn.
4.1. Điểm mạnh của kiểm duyệt dựa trên mô hình
Kiểm duyệt mô hình là tiềm năng của công nghệ “push – button”, sử dụng kiểm duyệt mô hình làm tăng mức độ tương tác người dùng và chuyên môn. Kiểm duyệt mô hình dễ dàng tích hợp trong chu kỳ phát triển phần mềm, làm giảm thời gian phát triển phần mềm. 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.
4.2. Điểm yếu của kiểm duyệt dựa trên mô hình
Kiểm duyệt mô hình chủ yếu phù hợp với các ứng dụng điều khiển, không phù hợp với các ứng dụng hướng dữ liệu do khối lượng dữ liệu thường tăng vô hạn. 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 thế tạo (trong phần cứng) và lỗi lập trình (phần mềm). Kiểm duyệt mô hình chỉ kiểm chứng những thuộc tính được đặc tả.
V. Kết Luận và Hướng Phát Triển Kiểm Định Mô Hình UTT
Mặc dù có những hạn chế nhất định trên nhưng kiểm duyệt mô hình vẫn là kỹ thuật hiệu quả để tìm ra lỗi thiết kế nhằm tạo ra hệ thống hoàn chỉnh nhất. Các biểu thức temporal logic không chỉ xét đến những dãy trạng thái đơn, mà còn xét đến những dãy trạng thái phức tạp trong đó từ một trạng thái có thể có nhiều trạng thái ngay tiếp sau nó. Trong các nghiên cứu về kiểm duyệt mô hình, có hai loại logic thời gian hay được xem xét là LTL (Linear Temporal Logic) và CTL (Branching Temporal Logic) [2].
5.1. Tương lai của kiểm định mô hình hệ thống thông tin
Với sự phát triển của công nghệ và các phương pháp mới, kiểm định mô hình hệ thống thông tin sẽ ngày càng trở nên quan trọng và được ứng dụng rộng rãi hơn trong nhiều lĩnh vực. Việc nghiên cứu và phát triển các công cụ, kỹ thuật mới sẽ giúp nâng cao hiệu quả và độ tin cậy của các hệ thống thông tin.
5.2. Hướng phát triển kiểm định mô hình tại UTT
Trường Đại học Giao thông Vận tải Hà Nội (UTT) có thể tập trung vào việc đào tạo nguồn nhân lực chất lượng cao trong lĩnh vực kiểm định mô hình hệ thống thông tin, đồng thời đẩy mạnh hợp tác với các doanh nghiệp và tổ chức nghiên cứu để ứng dụng các kết quả nghiên cứu vào thực tiễn.
