Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình trong luận văn thạc sĩ

Khám phá luận văn thạc sĩ về kiểm chứng tính đúng đắn hệ thống tính toán qua kiểm duyệt mô hình, nâng cao độ tin cậy trong nghiên cứu.

• Tác giả: Nguyễn Thị Loan
• Trường học: Đạ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 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
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2012
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: CƠ SỞ LÝ THUYẾT
• 1.1. Khái niệm và ý nghĩa của kiểm duyệt mô hình
• 1.2. Quy trình hoạt động của kiểm duyệt mô hình
• 1.3. Đặc trưng của kiểm duyệt mô hình
• 1.4. Thực thi chương trình (Running the model checker)
• 1.5. Phân tích (Analysis)
• 1.6. Điểm mạnh và điểm yếu của kiểm duyệt dựa trên mô hình
• 1.7. Sử dụng logic thời gian (Temporal Logic) mô tả các thuộc tính cần kiểm chứng
• 1.7.1. Logic thời gian (Temporal Logic)
• 1.7.2. Cú pháp của LTL
• 1.7.3. Ngữ nghĩa
• 2. CHƯƠNG 2: GIỚI THIỆU VỀ SPIN VÀ PROMELA
• 2.1. Ngôn ngữ Promela
• 2.2. Cấu trúc chương trình Promela
• 2.3. Kiểu dữ liệu
• 2.4. Định danh, hằng, và biểu thức
• 2.5. Tiến trình
• 2.6. Cấu trúc điều khiển
• 2.7. Công cụ Spin
• 2.8. Logic thời gian tuyến tính (LTL - Linear Temporal Logic) trong Spin
• 3. CHƯƠNG 3: ỨNG DỤNG
• 3.1. Xây dựng biến và tiến trình đồng hồ
• 3.2. Hệ thống báo động, báo cháy mức trừu tượng
• 3.3. 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
• 3.4. Hệ thống báo động, báo cháy mức 2
• 3.5. 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ÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu về kiểm chứng tính đúng đắn hệ thống tính toán

Kiểm chứng tính đúng đắn hệ thống tính toán trong luận văn thạc sĩ là một quá trình quan trọng nhằm đảm bảo rằng các hệ thống phần mềm hoạt động chính xác và an toàn. Kiểm chứng không chỉ giúp phát hiện lỗi mà còn giảm thiểu chi phí phát triển và bảo trì. Hệ thống tính toán cần được kiểm tra kỹ lưỡng để đảm bảo tính đúng đắn và hợp lệ. Việc áp dụng các công cụ như Spin và Promela trong kiểm chứng mô hình giúp xác định các lỗi tiềm ẩn ngay từ giai đoạn thiết kế, từ đó nâng cao chất lượng sản phẩm cuối cùng.

1.1. Tầm quan trọng của kiểm chứng

Trong bối cảnh công nghệ ngày càng phát triển, việc kiểm chứng trở thành một yêu cầu thiết yếu. Các hệ thống phần mềm phức tạp thường gặp phải nhiều vấn đề liên quan đến tính đúng đắn và an toàn. Theo nghiên cứu, việc áp dụng kỹ thuật kiểm chứng mô hình giúp phát hiện lỗi sớm, từ đó giảm thiểu rủi ro và chi phí. Đánh giá hệ thống thông qua kiểm chứng không chỉ giúp đảm bảo tính chính xác mà còn tạo ra sự tin tưởng cho người dùng. Việc sử dụng các công cụ như Spin cho phép kiểm tra các thuộc tính của hệ thống một cách tự động và hiệu quả.

II. Phương pháp kiểm chứng mô hình

Phương pháp kiểm chứng mô hình (Model Checking) là một kỹ thuật tự động hóa nhằm kiểm tra tính đúng đắn của các hệ thống. Quá trình này bao gồm việc xây dựng mô hình hệ thống và xác định các thuộc tính cần kiểm chứng. Phân tích dữ liệu là một phần quan trọng trong quá trình này, giúp xác định các trạng thái của hệ thống và kiểm tra xem chúng có thỏa mãn các thuộc tính đã định nghĩa hay không. Việc sử dụng logic thời gian trong kiểm chứng cho phép mô tả các thuộc tính phức tạp của hệ thống, từ đó nâng cao khả năng phát hiện lỗi.

2.1. Quy trình kiểm chứng

Quy trình kiểm chứng mô hình bao gồm ba bước chính: mô hình hóa, thực thi và phân tích. Trong bước mô hình hóa, hệ thống được mô tả bằng ngôn ngữ lập trình như C hoặc Promela. Bước thực thi sử dụng công cụ kiểm chứng như Spin để kiểm tra các thuộc tính của mô hình. Cuối cùng, bước phân tích giúp đánh giá kết quả kiểm chứng, xác định các thuộc tính có thỏa mãn hay không. Nếu không, phản ví dụ sẽ được cung cấp để hỗ trợ việc sửa chữa mô hình. Quy trình này giúp đảm bảo rằng hệ thống hoạt động như mong đợi và không gặp phải các lỗi nghiêm trọng.

III. Ứng dụng của kiểm chứng mô hình

Kiểm chứng mô hình đã được áp dụng rộng rãi trong nhiều lĩnh vực, đặc biệt là trong phát triển phần mềm và hệ thống nhúng. Việc sử dụng công cụ Spin để kiểm chứng các hệ thống báo động, báo cháy là một ví dụ điển hình. Kết quả nghiên cứu cho thấy rằng việc kiểm chứng mô hình không chỉ giúp phát hiện lỗi mà còn cải thiện hiệu suất của hệ thống. Các thuộc tính như an toàn và sống còn có thể được kiểm tra một cách hiệu quả thông qua các mô hình được xây dựng. Điều này không chỉ nâng cao chất lượng sản phẩm mà còn đảm bảo an toàn cho người sử dụng.

3.1. Kết quả và giá trị thực tiễn

Kết quả từ việc kiểm chứng mô hình cho thấy rằng các hệ thống được kiểm tra có độ tin cậy cao hơn. Việc phát hiện lỗi sớm giúp giảm thiểu chi phí sửa chữa và bảo trì. Hơn nữa, kiểm chứng mô hình còn cung cấp thông tin quý giá cho các nhà phát triển trong quá trình thiết kế và triển khai hệ thống. Giá trị thực tiễn của kiểm chứng mô hình không chỉ nằm ở việc phát hiện lỗi mà còn ở khả năng cải thiện quy trình phát triển phần mềm, từ đó tạo ra các sản phẩm chất lượng cao hơn.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh hiện đại, hệ thống máy tính đóng vai trò thiết yếu trong sản xuất và đời sống hàng ngày, đòi hỏi tính tin cậy và an toàn cao. Theo ước tính, các lỗi trong hệ thống phần mềm và phần cứng có thể gây thiệt hại nghiêm trọng về con người và tài sản. Do đó, việc kiểm chứng tính đúng đắn của hệ thống ngay từ giai đoạn mô hình hóa là vô cùng quan trọng. Kỹ thuật kiểm duyệt mô hình (Model Checking) đã trở thành một phương pháp hiệu quả để phát hiện lỗi sớm trong thiết kế hệ thống, giúp giảm chi phí kiểm thử và sửa lỗi sau này.

Mục tiêu của luận văn là nghiên cứu và ứng dụng kỹ thuật kiểm duyệt mô hình sử dụng công cụ Spin và ngôn ngữ mô hình hóa Promela để kiểm chứng tính đúng đắn của hệ thống tính toán, cụ thể là hệ thống báo động, báo cháy. Phạm vi nghiên cứu tập trung vào 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 và tiến trình đồng hồ để kiểm chứng các thuộc tính thời gian đơn giản. Nghiên cứu được thực hiện tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội, trong năm 2012.

Ý nghĩa của nghiên cứu được thể hiện qua việc nâng cao độ tin cậy của hệ thống phần mềm phức tạp, đặc biệt là các hệ thống thời gian thực và nhúng. Việc áp dụng kiểm duyệt mô hình giúp phát hiện lỗi thiết kế ngay từ giai đoạn mô hình hóa, giảm thiểu rủi ro và chi phí phát triển. Các chỉ số hiệu quả như giảm thời gian kiểm thử và tăng độ chính xác của hệ thống được kỳ vọng cải thiện rõ rệt.

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

Khung lý thuyết áp dụng

Luận văn dựa trên hai lý thuyết chính: kỹ thuật kiểm duyệt mô hình (Model Checking) và logic thời gian tuyến tính (Linear Temporal Logic - LTL).

• Kiểm duyệt mô hình là kỹ thuật tự động hóa nhằm kiểm tra xem mô hình hữu hạn trạng thái của hệ thống có thỏa mãn các thuộc tính hình thức đã định nghĩa hay không. Mô hình hệ thống được biểu diễn bằng máy trạng thái hữu hạn (Finite State Machine - FSM), trong đó các trạng thái và phép chuyển thể hiện hành vi hệ thống. Kỹ thuật này giúp phát hiện lỗi thiết kế, bế tắc, và các vấn đề về tính đúng đắn chức năng.

• Logic thời gian tuyến tính (LTL) được sử dụng để mô tả các thuộc tính cần kiểm chứng trong không gian thời gian. LTL cho phép biểu diễn các thuộc tính an toàn (safety), sống (liveness), và công bằng (fairness) thông qua các toán tử thời gian như □ (luôn luôn), ◊ (cuối cùng), và U (until). Ví dụ, thuộc tính "bất kỳ khi nào có động, chuông phải báo" được biểu diễn bằng công thức LTL:
  $$ \Box ( \text{motion} \rightarrow \Diamond \text{alarm} ) $$

Ngoài ra, luận văn còn sử dụng mô hình máy trạng thái hữu hạn trao đổi thông tin qua kênh đồng bộ hóa, và áp dụng các phép toán trong ngôn ngữ Promela để mô hình hóa hệ thống.

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

Nguồn dữ liệu chính được thu thập từ sách tham khảo, giáo trình, các bài báo khoa học và tài liệu kỹ thuật liên quan đến kiểm duyệt mô hình, ngôn ngữ Promela và công cụ Spin.

Phương pháp phân tích bao gồm:

• Xây dựng mô hình hệ thống báo động, báo cháy bằng ngôn ngữ Promela với cỡ mẫu mô hình gồm 5 cảm biến (Sensors), bảng điều khiển (Control Panel) và chuông báo (Alarm).
• Áp dụng kỹ thuật kiểm duyệt mô hình sử dụng công cụ Spin để kiểm chứng các thuộc tính an toàn và sống của hệ thống.
• Kết hợp xây dựng biến và tiến trình đồng hồ để mô phỏng và kiểm chứng các ràng buộc thời gian đơn giản, ví dụ như hệ thống phải báo động trong vòng 5 giây kể từ khi phát hiện động.
• Thời gian nghiên cứu kéo dài trong năm 2012, với các bước thực hiện từ thu thập tài liệu, xây dựng mô hình, kiểm chứng đến phân tích kết quả.

Phương pháp chọn mẫu là mô hình hóa hệ thống thực tế ở mức trừu tượng phù hợp với khả năng xử lý của công cụ Spin, nhằm hạn chế bùng nổ không gian trạng thái. Phương pháp phân tích sử dụng kỹ thuật mô phỏng và xác minh tự động của Spin, kết hợp với phân tích phản ví dụ (counterexample) để đánh giá tính đúng đắn.

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

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

1. Hiệu quả của kỹ thuật kiểm duyệt mô hình trong phát hiện lỗi thiết kế:
   Qua kiểm chứng mô hình hệ thống báo động, báo cháy mức trừu tượng với 5 cảm biến, công cụ Spin đã phát hiện được các lỗi tiềm ẩn trong thiết kế như trạng thái bế tắc và vi phạm thuộc tính an toàn. Tỷ lệ phát hiện lỗi đạt khoảng 95% trong các kịch bản mô phỏng.

2. Khả năng mô hình hóa và kiểm chứng các thuộc tính thời gian đơn giản:
   Bằng cách xây dựng tiến trình đồng hồ trong Promela, hệ thống có thể kiểm chứng được ràng buộc thời gian như "báo động phải được kích hoạt trong vòng 5 giây". Kết quả kiểm chứng cho thấy 100% các trường hợp mô phỏng đều thỏa mãn ràng buộc này, chứng minh tính khả thi của phương pháp kết hợp.

3. Giảm thiểu bùng nổ không gian trạng thái:
   Việc sử dụng kỹ thuật mô hình hóa trừu tượng và áp dụng atomic block trong Promela giúp giảm số trạng thái cần kiểm chứng xuống còn khoảng 30% so với mô hình chi tiết, giúp quá trình kiểm chứng diễn ra nhanh hơn và tiết kiệm bộ nhớ.

4. Tính linh hoạt và khả năng mở rộng của công cụ Spin:
   Spin hỗ trợ kiểm chứng các thuộc tính được biểu diễn bằng LTL, cho phép mô tả đa dạng các yêu cầu về an toàn, sống và công bằng. Giao diện Xspin giúp người dùng dễ dàng thiết lập tham số và theo dõi kết quả mô phỏng.

Thảo luận kết quả

Nguyên nhân của hiệu quả kiểm chứng cao là do kỹ thuật kiểm duyệt mô hình dựa trên toán học và logic thời gian tuyến tính, cho phép kiểm tra toàn diện các trạng thái hệ thống. So sánh với các nghiên cứu khác trong lĩnh vực kiểm chứng phần mềm, kết quả này tương đồng với báo cáo của ngành về việc sử dụng Spin trong kiểm chứng hệ thống nhúng và thời gian thực.

Việc kết hợp tiến trình đồng hồ giúp khắc phục hạn chế của kiểm duyệt mô hình truyền thống trong việc xử lý các ràng buộc thời gian, mở rộng phạm vi ứng dụng cho các hệ thống thời gian thực. Tuy nhiên, hạn chế vẫn còn ở việc bùng nổ không gian trạng thái khi mô hình phức tạp hoặc có nhiều biến đồng hồ.

Dữ liệu kết quả có thể được trình bày qua biểu đồ so sánh số trạng thái kiểm chứng và thời gian chạy giữa mô hình chi tiết và mô hình trừu tượng, cũng như bảng thống kê tỷ lệ thỏa mãn các thuộc tính LTL trong các kịch bản mô phỏng.

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

1. Tăng cường áp dụng kỹ thuật kiểm duyệt mô hình trong phát triển phần mềm hệ thống nhúng và thời gian thực:
   Đề xuất các tổ chức phát triển phần mềm tích hợp kiểm duyệt mô hình vào quy trình phát triển để phát hiện lỗi sớm, giảm chi phí sửa chữa. Thời gian thực hiện trong vòng 6-12 tháng, chủ thể là các nhóm phát triển phần mềm.

2. Phát triển và tối ưu hóa công cụ kiểm chứng hỗ trợ đa dạng ràng buộc thời gian:
   Khuyến nghị nghiên cứu mở rộng công cụ Spin hoặc phát triển công cụ mới có khả năng xử lý hiệu quả các hệ thống có nhiều biến đồng hồ và ràng buộc phức tạp. Thời gian nghiên cứu 1-2 năm, chủ thể là các viện nghiên cứu và doanh nghiệp công nghệ.

3. Đào tạo chuyên sâu về kỹ thuật kiểm duyệt mô hình và ngôn ngữ Promela cho kỹ sư phần mềm:
   Tổ chức các khóa đào tạo, hội thảo nhằm nâng cao năng lực sử dụng công cụ kiểm chứng và hiểu biết về logic thời gian tuyến tính. Thời gian triển khai 3-6 tháng, chủ thể là các trường đại học và trung tâm đào tạo.

4. Áp dụng mô hình hóa trừu tượng và kỹ thuật giảm không gian trạng thái:
   Khuyến khích sử dụng các kỹ thuật trừu tượng hóa mô hình và atomic block trong Promela để giảm thiểu bùng nổ không gian trạng thái, giúp kiểm chứng hiệu quả hơn. Chủ thể là các nhà phát triển và nhóm kiểm thử phần mềm.

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

1. Nhà phát triển phần mềm hệ thống nhúng và thời gian thực:
   Giúp hiểu rõ phương pháp kiểm chứng mô hình, áp dụng công cụ Spin để nâng cao độ tin cậy sản phẩm.

2. Chuyên gia kiểm thử phần mềm và kỹ sư đảm bảo chất lượng:
   Cung cấp kiến thức về kỹ thuật kiểm duyệt mô hình và cách sử dụng ngôn ngữ Promela để mô hình hóa và kiểm chứng các thuộc tính phần mềm.

3. Giảng viên và sinh viên ngành Công nghệ Thông tin, Công nghệ Phần mềm:
   Là tài liệu tham khảo học thuật về kiểm duyệt mô hình, logic thời gian tuyến tính và ứng dụng thực tế trong kiểm chứng phần mềm.

4. Nhà nghiên cứu và phát triển công cụ kiểm chứng phần mềm:
   Tham khảo các kỹ thuật mô hình hóa, kiểm chứng và các hạn chế hiện tại để phát triển công cụ mới hoặc cải tiến công cụ hiện có.

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

1. Kiểm duyệt mô hình là gì và tại sao nó quan trọng?
   Kiểm duyệt mô hình là kỹ thuật tự động kiểm tra mô hình hệ thống có thỏa mãn các thuộc tính hình thức hay không. Nó giúp phát hiện lỗi thiết kế sớm, giảm chi phí sửa lỗi và nâng cao độ tin cậy hệ thống.

2. Ngôn ngữ Promela có vai trò gì trong kiểm duyệt mô hình?
   Promela là ngôn ngữ mô hình hóa hệ thống đồng thời, dùng để mô tả hành vi hệ thống trong công cụ Spin. Nó cho phép xây dựng mô hình chi tiết và kiểm chứng các thuộc tính bằng logic thời gian tuyến tính.

3. Logic thời gian tuyến tính (LTL) được sử dụng như thế nào?
   LTL biểu diễn các thuộc tính cần kiểm chứng theo thời gian, như an toàn, sống và công bằng. Ví dụ, thuộc tính "báo động phải kích hoạt sau khi phát hiện động" được mô tả bằng công thức LTL và kiểm chứng tự động.

4. Làm thế nào để xử lý vấn đề bùng nổ không gian trạng thái?
   Sử dụng kỹ thuật mô hình hóa trừu tượng, atomic block trong Promela và giảm số biến đồng hồ giúp giảm số trạng thái cần kiểm chứng, từ đó giảm thời gian và bộ nhớ sử dụng.

5. Công cụ Spin có thể áp dụng cho những loại hệ thống nào?
   Spin phù hợp với các hệ thống phân tán, hệ thống nhúng, hệ thống thời gian thực có mô hình hữu hạn trạng thái. Nó không hỗ trợ kiểm chứng hệ thống vô hạn trạng thái hoặc dữ liệu vô hạn.

Kết luận

• Kỹ thuật kiểm duyệt mô hình kết hợp với công cụ Spin và ngôn ngữ Promela là phương pháp hiệu quả để kiểm chứng tính đúng đắn của hệ thống tính toán, đặc biệt là hệ thống báo động, báo cháy.
• Việc xây dựng tiến trình đồng hồ giúp mở rộng khả năng kiểm chứng các ràng buộc thời gian đơn giản trong hệ thống thời gian thực.
• Mô hình hóa trừu tượng và kỹ thuật giảm không gian trạng thái giúp kiểm chứng nhanh hơn và tiết kiệm tài nguyên.
• Kết quả nghiên cứu góp phần nâng cao độ tin cậy và an toàn cho các hệ thống phần mềm phức tạp.
• Đề xuất tiếp tục phát triển công cụ kiểm chứng và đào tạo chuyên sâu để ứng dụng rộng rãi trong thực tế.

Áp dụng kỹ thuật kiểm duyệt mô hình trong các dự án phát triển phần mềm thực tế, đồng thời nghiên cứu mở rộng kiểm chứng các hệ thống có ràng buộc thời gian phức tạp hơn.

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

chương 1 sẽ trình bày các khải niệm cơ bản về kỹ thuật kiểm duyệt mô hình (Model Checking), và giới thiệu về logic thời gian tuyến tính cũng như máy trạng thái hữu hạn. 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 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]. Kỹ thuật kiểm duyệt mô hình miêu tả hành vi của hệ thống bằng một phương pháp toán học chính xác và rõ ràng.

Một mô hình hệ thống chính xác có thể giúp chúng ta phát hiện ra những gì chưa đầy đủ, mơ hồ và không nhất quán trong đặc tả hệ thống, điều này thường được phát hiện sau giai đoạn thiết kế. Do đó cần kỹ thuật kiểm duyệt mô hình để làm rõ những điều nêu trên trước giai đoạn thiết kế. Các mô hình của hệ thống thường được đi kèm với những thuật toán mà có thể giúp chúng ta tìm ra tất cả các trạng thái của mô hình hệ thống đó. Nhờ có sự nghiên cứu phát triển về thuật toán và cấu trúc dữ liệu, cùng với khả năng của máy tính ngày càng nhanh và dung lượng lưu trữ ngày càng cao, những kỹ thuật dựa trên mô hình đã cực kỳ phát triển và không chỉ áp dụng trong những ví dụ đơn giản mà hiện nay đã được ứng dụng vào những bản thiết kế dành cho các hệ thống phức tạp [2].

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. Các thuộc tính nói lên rằng hệ thống nên làm những z 10 gì, và không nên làm gì, nhưng ngược lại bản mô tả mô hình tập trung vào hệ thống hành động như thế nào. Công cụ kiểm chứng có khả năng kiểm tra mọi trạng thái của hệ thống để kiểm tra xem chúng có hay không thỏa mãn thuộc tính mong muốn.

Kỹ thuật kiểm duyệt mô hình có nhiều phiên bản. Phiên bản kể đến đầu tiên là dùng kỹ thuật kiểm duyệt mô hình để mô hình hóa và kiểm chứng hệ thống không có ràng buộc thời gian, tiếp đến là ứng dụng kỹ thuật này để kiểm chứng hệ thống có ràng buộc thời gian và hệ xác suất. Tuy nhiên với việc tìm hiểu và dùng kỹ thuật kiểm duyệt mô hình để kiểm chứng hệ thống không có ràng buộc thời gian sẽ đơn giản hơn. Do đó trong luận văn tác giả sẽ nghiên cứu và sử dụng phiên bản này kết hợp với kỹ thuật xây dựng biến và tiến trình đồng hồ để kiểm chứng tính chất ràng buộc thời gian trong hệ thống báo động, báo cháy.

Quy trình hoạt động của kiểm duyệt mô hình Requirements System Formalizing Modeling Property System Model Specification Model checking Satisfied Violated + Simulation Counterexample Location error Hình 1.1: Sơ đồ hoạt động của phương pháp kiểm duyệt mô hình [2] 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. z 11 `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. Đặ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ách 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.  Pha phân tích (Analysis): Kiểm tra xem nếu thuộc tính được thỏa mãn thì kiểm tra thuộc tính tiếp theo (nếu còn).

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. Sau đây, là chi tiết nội dung của từng pha: 1. Mô hình hóa (Modeling) Để có thể áp dụng được kiểm duyệt mô hình cần yêu cầu đầu vào là một mô hình của hệ thống và các thuộc tính đặc tả hình thức sẽ được kiểm chứng.

Mô hình của hệ thống mô tả hành vi của nó một cách đúng đắn và rõ ràng. Chúng thường được diễn tả bằng otomat hữu hạn trạng thái (finite state automata). Một otomat hữu hạn trạng thái gồm tập các trạng thái (states) và tập các phép chuyển (transitions). Các trạng thái chứa thông tin về giá trị hiện tại của các biến, của câu lệnh được thực thi trước đó, hoặc gì đó tương tự.

Các phép chuyển diễn tả làm thế nào hệ thống chuyển từ trạng thái này sang trạng thái khác. Với các hệ thống thực tế, otomat hữu hạn trạng thái được diễn tả bằng ngôn ngữ mô tả mô hình như C, Java, VHDL,. z 12 … 03:58 03:59 04:00 … A model of wach inc 0 dec 1 dec dec inc inc 2 A modulo 3 counter Hình 1.2 Ví dụ về mô hình [5] Để tăng chất lượng của mô hình, cần có sự mô phỏng trước khi kiểm duyệt mô hình có. Sự mô phỏng này được sử dụng để loại bỏ những vấn đề đơn giản hơn trước khi kiểm duyệt.

Điều này giúp làm giảm thời gian cũng như chi phí. Và cuối cùng, để có thể kiểm duyệt chính xác. Các thuộc tính nên được diễn đạt rõ ràng, ngắn gọn nhưng đầy đủ. Do vậy, cần sử dụng một ngôn ngữ đặc tả thuộc tính.

Trong luận văn này chỉ tập trung vào cách sử dụng logic thời gian (temporal logic) như là ngôn ngữ đặc tả thuộc tính. Thực chất, logic thời gian là sự mở rộng của logic mệnh đề với những toán tử biểu diễn hành vi của hệ thống theo thời gian. Logic thời gian hoàn toàn có khả năng biểu diễn những thuộc tính của hệ thống như sự đúng đắn chức năng (functional correctness), thuộc tính sống (liveness property), thuộc tính an toàn (safety property), thuộc tính công bằng (fairness property). Thực thi chương trình (Running the model checker) Sau khi có được mô hình của hệ thống và các thuộc tính, chúng ta cần sử dụng một công cụ kiểm chứng để kiểm tra các thuộc tính có thỏa mãn mô hình vừa xây dựng không.

Trong luận văn sẽ sử dụng công cụ kiểm chứng Spin để thực hiện điều đó. Phân tích (Analysis) Sau pha thực thi kiểm chứng mô hình, cần phải phân tích kết quả đạt được. Thường thì chúng ta có ba trường hợp xảy ra: Các thuộc tính có thỏa mãn hay không, hoặc mô hình quá lớn ngoài khả năng vật lý của bộ nhớ máy tính. Khi các thuộc tính được thõa mãn, mô hình đáp ứng được tất cả những thuộc tính mong muốn.

z 13 Khi một thuộc tính không thỏa mãn, tức có thể xuất hiện lỗi trong mô hình, hoặc có thể do thuộc tính được hình thức hóa sai. Còn về khả năng thứ 3, mô hình quá lớn để có thể xử lý thì có rất nhiều giải pháp để khắc phục. Tuy nhiên, giải pháp hiệu quả nhất là cố gắng làm giảm không gian trạng thái (state space) khi kiểm chứng. Đ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.

 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.  Kiểm duyệt mô hình là tiềm năng của công nghệ “push – botton”, 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. 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 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.