Nghiên Cứu Phương Pháp Kiểm Chứng Mô Hình Phần Mềm Dựa Trên SAT

Luận văn thạc sĩ nghiên cứu phương pháp kiểm chứng mô hình phần mềm dựa trên SAT, cung cấp kiến thức và ứng dụng trong lĩnh vực công nghệ thông tin.

• Tác giả: Đinh Quang Đạt
• Người hướng dẫn: TS. Nguyễn Trường Thắng
• 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: Phương Pháp Kiểm Chứng Mô Hình Phần Mềm Dựa Trên SAT
• 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 CAM ĐOAN
• LỜI MỞ ĐẦU
• 1. CHƯƠNG 1: KIỂM CHỨNG MÔ HÌNH
• 1.1. Giới thiệu về kiểm chứng mô hình
• 1.2. Các kiến thức nền tảng
• 2. CHƯƠNG 2: VẤN ĐỀ BÙNG NỔ KHÔNG GIAN TRẠNG THÁI TRONG KIỂM CHỨNG MÔ HÌNH VÀ CÁCH GIẢI QUYẾT THEO HƯỚNG TIẾP CẬN CỔ ĐIỂN
• 2.1. Vấn đề của bùng nổ trạng thái trong kiểm chứng mô hình
• 2.2. Cách giải quyết theo hướng tiếp cận cổ điển
• 3. CHƯƠNG 3: KIỂM CHỨNG MÔ HÌNH GIỚI HẠN SỬ DỤNG BỘ GIẢI CÔNG CỤ SAT
• 3.1. Các thuộc tính an toàn
• 3.2. Giải công cụ SAT
• 3.3. Xác định giới hạn
• 3.4. BMC cho các thuộc tính LTL
• 3.5. Giới thiệu về SMT
• 4. CHƯƠNG 4: NGÔN NGỮ SMV, CÔNG CỤ NUSMV VÀ THỰC NGHIỆM
• 4.1. Ngôn ngữ SMV
• 4.1.1. Kiểu dữ liệu trong SMV
• 4.1.2. Phép toán trong SMV
• 4.2. Công cụ NuSMV
• 4.3. Thực nghiệm sử dụng công cụ NuSMV
• KẾT LUẬN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Kiểm chứng mô hình

Kiểm chứng mô hình là một kỹ thuật quan trọng trong lĩnh vực công nghệ thông tin, giúp xác minh tính đúng đắn của các hệ thống phức tạp. Kỹ thuật này cho phép kiểm tra tất cả các trạng thái có thể của hệ thống, từ đó phát hiện ra các lỗi tiềm ẩn. Đặc biệt, kiểm chứng mô hình dựa trên các mô hình toán học rõ ràng, giúp giảm thiểu thời gian và công sức trong quá trình kiểm định. Việc áp dụng phương pháp kiểm chứng này không chỉ giúp nâng cao độ tin cậy của hệ thống mà còn hỗ trợ trong việc phát hiện các lỗi khó nhận thấy trong quá trình phát triển phần mềm.

1.1. Giới thiệu về kiểm chứng mô hình

Kiểm chứng mô hình là một phương pháp kiểm tra tính đúng đắn của các hệ thống thông qua việc mô hình hóa hành vi của chúng. Các hệ thống ICT ngày càng trở nên phức tạp, do đó, việc áp dụng logic và mô hình trong kiểm chứng là cần thiết. Kỹ thuật này không chỉ giúp phát hiện lỗi mà còn cung cấp thông tin hữu ích cho việc sửa lỗi. Kiểm chứng mô hình cho phép kiểm tra các thuộc tính của hệ thống, từ đó đảm bảo rằng hệ thống hoạt động đúng như mong đợi.

1.2. Kiểm định trong phần cứng và phần mềm

Kiểm định là một phần quan trọng trong quá trình phát triển phần mềm và phần cứng. Nó giúp xác minh rằng hệ thống đạt được các đặc tính nhất định. Kiểm chứng mô hình có thể được áp dụng để kiểm tra các thuộc tính an toàn của hệ thống, từ đó phát hiện các lỗi tiềm ẩn. Việc kiểm định không chỉ giúp đảm bảo tính đúng đắn mà còn giảm thiểu rủi ro trong quá trình phát triển sản phẩm.

1.3. Kiểm chứng mô hình

Kỹ thuật kiểm chứng mô hình cho phép kiểm tra tất cả các trạng thái có thể của hệ thống một cách có hệ thống. Điều này giúp phát hiện các lỗi mà các phương pháp kiểm tra khác có thể bỏ sót. Kiểm chứng mô hình không chỉ giúp xác minh tính đúng đắn mà còn cung cấp phản ví dụ cho các trạng thái vi phạm, từ đó hỗ trợ trong việc sửa lỗi và cải thiện chất lượng phần mềm.

1.4. Các tiến trình trong kiểm chứng mô hình

Quá trình kiểm chứng mô hình bao gồm nhiều bước, từ việc mô hình hóa hệ thống đến việc kiểm tra các thuộc tính của nó. Mô hình hóa giúp xác định các trạng thái và chuyển dịch của hệ thống, trong khi kiểm tra tính đúng đắn giúp phát hiện các lỗi. Các công cụ kiểm chứng hiện đại có thể xử lý không gian trạng thái lớn, từ đó nâng cao hiệu quả của quá trình kiểm chứng.

1.5. Mặt mạnh và mặt yếu của kiểm chứng mô hình

Mặc dù kiểm chứng mô hình có nhiều ưu điểm như khả năng phát hiện lỗi khó nhận thấy và hỗ trợ kiểm chứng từng phần, nhưng cũng tồn tại một số nhược điểm. Việc kiểm chứng mô hình có thể gặp khó khăn với các hệ thống có không gian trạng thái lớn, và yêu cầu người dùng có kiến thức chuyên môn để trừu tượng hóa hệ thống. Tuy nhiên, với sự phát triển của công nghệ, kiểm chứng mô hình vẫn là một công cụ hữu ích trong việc đảm bảo chất lượng phần mềm.

II. Các kiến thức nền tảng

Các kiến thức nền tảng là rất quan trọng trong việc áp dụng kiểm chứng mô hình. Hệ thống dịch chuyển là một trong những khái niệm cơ bản, giúp mô tả hành vi của hệ thống thông qua các trạng thái và chuyển dịch. Việc hiểu rõ về hệ thống dịch chuyển sẽ giúp cho việc mô hình hóa và kiểm chứng trở nên hiệu quả hơn. Các khái niệm như logic thời gian và các loại logic khác cũng đóng vai trò quan trọng trong việc xác định các thuộc tính cần kiểm chứng.

2.1. Hệ thống dịch chuyển

Hệ thống dịch chuyển là một mô hình mô tả hành vi của hệ thống thông qua các trạng thái và chuyển dịch. Mô hình này giúp xác định các trạng thái khởi tạo và các hành động có thể thực hiện. Việc mô hình hóa hệ thống dịch chuyển cho phép kiểm tra các thuộc tính của hệ thống một cách có hệ thống, từ đó phát hiện các lỗi tiềm ẩn.

2.2. Logic thời gian

Logic thời gian là một công cụ quan trọng trong kiểm chứng mô hình. Nó cho phép mô tả các thuộc tính của hệ thống theo thời gian, từ đó giúp xác định các trạng thái mà hệ thống có thể đạt được. Việc áp dụng logic thời gian trong kiểm chứng giúp nâng cao độ chính xác và hiệu quả của quá trình kiểm tra.

2.3. Logic thời gian tuyến tính LTL và logic tính toán cây CTL

LTL và CTL là hai loại logic thời gian phổ biến trong kiểm chứng mô hình. LTL cho phép mô tả các thuộc tính liên quan đến thời gian, trong khi CTL giúp xác định các trạng thái có thể đạt được trong một cây trạng thái. Việc sử dụng LTL và CTL trong kiểm chứng giúp phát hiện các lỗi tiềm ẩn và đảm bảo tính đúng đắn của hệ thống.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh phát triển nhanh chóng của công nghệ thông tin (CNTT) tại Việt Nam và trên thế giới, phần mềm đã trở thành thành phần không thể thiếu trong nhiều lĩnh vực như thương mại điện tử, ngân hàng, giải trí và y tế. Theo ước tính, khoảng 20% chi phí phát triển các phương tiện giao thông hiện đại được dành cho hệ thống xử lý thông tin, trong khi dòng tiền giao dịch qua Internet hàng ngày lên tới khoảng 10 triệu đô la Mỹ. Tuy nhiên, sự phức tạp ngày càng tăng của các hệ thống CNTT dẫn đến nguy cơ lỗi phần mềm và phần cứng cao, gây thiệt hại nghiêm trọng về kinh tế và uy tín, điển hình như sự cố tàu vũ trụ Ariane-5 năm 1996 với thiệt hại hàng triệu đô la Mỹ.

Vấn đề kiểm chứng mô hình phần mềm nhằm đảm bảo tính đúng đắn và độ tin cậy của hệ thống trở nên cấp thiết. Luận văn tập trung nghiên cứu phương pháp kiểm chứng mô hình giới hạn (Bounded Model Checking - BMC) dựa trên bộ giải công cụ SAT nhằm giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình. Phạm vi nghiên cứu bao gồm các hệ thống dịch chuyển trạng thái hữu hạn, các thuộc tính an toàn được biểu diễn bằng logic thời gian tuyến tính (LTL), và áp dụng công cụ NuSMV để thực nghiệm. Mục tiêu chính là phát triển và đánh giá hiệu quả phương pháp BMC dựa trên SAT trong việc phát hiện lỗi phần mềm nhanh chóng, tiết kiệm bộ nhớ và không yêu cầu sắp xếp biến phức tạp như các phương pháp truyền thống.

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 các lý thuyết và mô hình sau:

• Hệ thống dịch chuyển (Transition System): Mô hình hóa hành vi hệ thống dưới dạng tập hợp trạng thái và các chuyển dịch giữa chúng, với các trạng thái khởi tạo và nhãn trạng thái biểu diễn các mệnh đề nguyên tử.

• Logic thời gian tuyến tính (LTL) và logic tính toán cây (CTL): Ngôn ngữ hình thức để biểu diễn các thuộc tính của hệ thống theo thời gian, trong đó LTL tập trung vào các đường dẫn tuyến tính vô hạn, còn CTL cho phép mô tả các thuộc tính phân nhánh.

• Kiểm chứng mô hình (Model Checking): Kỹ thuật kiểm tra tính đúng đắn của hệ thống bằng cách xét tất cả các trạng thái có thể xảy ra, phát hiện lỗi thông qua phản ví dụ.

• Kiểm chứng mô hình biểu trưng với BDD (Binary Decision Diagrams): Phương pháp biểu diễn tập hợp trạng thái bằng các biểu đồ quyết định nhị phân có thứ tự, giúp giảm thiểu bộ nhớ so với liệt kê trạng thái tường minh.

• Kiểm chứng mô hình giới hạn (BMC) dựa trên SAT: Phương pháp kiểm tra các phản ví dụ có độ dài giới hạn k bằng cách mã hóa bài toán thành công thức Boolean và sử dụng bộ giải SAT để tìm kiếm phản ví dụ.

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

• Nguồn dữ liệu: Luận văn sử dụng các tài liệu học thuật, báo cáo ngành CNTT, và các công trình nghiên cứu về kiểm chứng mô hình, logic thời gian, và bộ giải SAT.

• Phương pháp phân tích: Phân tích lý thuyết kiểm chứng mô hình, thuật toán điểm cố định, biểu diễn BDD, và kỹ thuật BMC dựa trên SAT. Thực nghiệm được thực hiện trên công cụ NuSMV với mô hình hệ thống quản lý thư viện, kiểm chứng các thuộc tính an toàn được biểu diễn bằng LTL.

• Timeline nghiên cứu: Nghiên cứu lý thuyết và thuật toán (3 tháng), phát triển mô hình và cài đặt thực nghiệm (4 tháng), đánh giá kết quả và hoàn thiện luận văn (2 tháng).

• Cỡ mẫu và chọn mẫu: Mô hình hệ thống quản lý thư viện với 3 thành viên và 3 quyển sách được mô phỏng để kiểm chứng các thuộc tính an toàn, phản ánh các tình huống thực tế trong quản lý thư việ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 kiểm chứng mô hình giới hạn dựa trên SAT: Phương pháp BMC tìm kiếm phản ví dụ nhanh hơn so với kiểm chứng mô hình biểu trưng với BDD, đặc biệt trong các hệ thống có không gian trạng thái lớn. Ví dụ, với hệ thống 3-bit, BMC phát hiện phản ví dụ thuộc tính an toàn Gp chỉ trong vài bước, trong khi BDD gặp khó khăn do kích thước biểu diễn.

2. Tiết kiệm bộ nhớ: BMC sử dụng ít bộ nhớ hơn nhiều so với BDD vì không cần lưu trữ toàn bộ không gian trạng thái mà chỉ mã hóa các đường dẫn có độ dài giới hạn. Điều này giúp mở rộng khả năng kiểm chứng cho các hệ thống phức tạp hơn.

3. Không yêu cầu sắp xếp biến: Khác với BDD, BMC không cần người dùng lựa chọn thứ tự biến, giảm thiểu thời gian chuẩn bị và rủi ro do sắp xếp biến không tối ưu.

4. Khả năng phát hiện lỗi tinh vi: BMC có thể phát hiện các lỗi phần mềm chưa được phát hiện bằng kiểm tra, mô phỏng hay giả lập thông thường, nhờ vào việc xét vét cạn các đường dẫn có độ dài giới hạn.

Thảo luận kết quả

Nguyên nhân chính của hiệu quả BMC là do việc chuyển đổi bài toán kiểm chứng thành bài toán thỏa mãn Boolean (SAT), tận dụng các thuật toán DPLL và các cải tiến như lan truyền đơn vị, xóa bỏ pure literal giúp giải quyết nhanh các công thức lớn. So với kiểm chứng mô hình biểu trưng với BDD, BMC không bị giới hạn bởi việc lưu trữ toàn bộ không gian trạng thái, đồng thời không phụ thuộc vào việc sắp xếp biến phức tạp.

Kết quả thực nghiệm trên công cụ NuSMV với mô hình hệ thống thư viện cho thấy BMC có thể kiểm chứng các thuộc tính an toàn như: sách chỉ được loại bỏ khi không mượn và không đặt trước, thành viên chỉ được mượn sách khi là thành viên hợp lệ, và các quy tắc đặt trước, gia hạn sách được tuân thủ nghiêm ngặt. Các phản ví dụ được cung cấp giúp định vị lỗi và hỗ trợ sửa chữa mô hình.

Dữ liệu có thể được trình bày qua biểu đồ so sánh thời gian và bộ nhớ tiêu thụ giữa BMC và BDD, cũng như bảng tổng hợp các thuộc tính được kiểm chứng thành công và các phản ví dụ phát hiện được.

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

1. Áp dụng rộng rãi kiểm chứng mô hình giới hạn dựa trên SAT trong phát triển phần mềm: Động viên các tổ chức phát triển phần mềm tích hợp BMC vào quy trình kiểm thử để phát hiện lỗi sớm, giảm chi phí sửa chữa.

2. Phát triển công cụ hỗ trợ tự động hóa mô hình hóa và chuyển đổi sang SAT: Tăng cường nghiên cứu và phát triển các công cụ giúp tự động hóa việc mô hình hóa hệ thống và mã hóa bài toán kiểm chứng thành công thức SAT, giảm thiểu sự phụ thuộc vào chuyên gia.

3. Đào tạo chuyên gia về kiểm chứng mô hình và SAT: Tổ chức các khóa đào tạo, hội thảo nhằm nâng cao năng lực cho kỹ sư phần mềm và nhà nghiên cứu về kỹ thuật kiểm chứng mô hình và sử dụng bộ giải SAT hiệu quả.

4. Mở rộng nghiên cứu sang kiểm chứng mô hình với SMT: Khuyến khích nghiên cứu tiếp cận kiểm chứng mô hình sử dụng SMT để xử lý các hệ thống có trạng thái vô hạn hoặc phức tạp hơn, nhằm nâng cao khả năng ứng dụng trong thực tế.

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

1. Nhà nghiên cứu và sinh viên ngành Công nghệ phần mềm: Nắm bắt kiến thức chuyên sâu về kiểm chứng mô hình, logic thời gian, và kỹ thuật BMC dựa trên SAT để phát triển các đề tài nghiên cứu mới.

2. Kỹ sư phát triển phần mềm và kiểm thử: Áp dụng phương pháp kiểm chứng mô hình giới hạn để nâng cao chất lượng sản phẩm, phát hiện lỗi phần mềm hiệu quả trong quá trình phát triển.

3. Chuyên gia kiểm định hệ thống nhúng và phần cứng: Sử dụng kỹ thuật kiểm chứng mô hình để đảm bảo tính đúng đắn và an toàn của các hệ thống phức tạp như thiết bị nhúng, hệ thống điều khiển.

4. Nhà quản lý dự án CNTT và các tổ chức phát triển phần mềm: Hiểu rõ lợi ích và ứng dụng của kiểm chứng mô hình để xây dựng quy trình phát triển phần mềm chất lượng cao, giảm thiểu rủi ro và chi phí.

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

1. Kiểm chứng mô hình giới hạn (BMC) là gì?
   BMC là phương pháp kiểm tra tính đúng đắn của hệ thống bằng cách tìm kiếm phản ví dụ có độ dài giới hạn k thông qua việc mã hóa bài toán thành công thức Boolean và sử dụng bộ giải SAT để giải quyết. Ví dụ, BMC có thể phát hiện lỗi trong hệ thống 3-bit chỉ sau vài bước kiểm tra.

2. Tại sao BMC hiệu quả hơn so với kiểm chứng mô hình biểu trưng với BDD?
   BMC không cần lưu trữ toàn bộ không gian trạng thái mà chỉ xét các đường dẫn có độ dài giới hạn, sử dụng bộ giải SAT tối ưu giúp tiết kiệm bộ nhớ và thời gian. Trong khi đó, BDD phụ thuộc vào việc sắp xếp biến và có thể bị bùng nổ bộ nhớ với hệ thống lớn.

3. Logic thời gian tuyến tính (LTL) được sử dụng như thế nào trong kiểm chứng mô hình?
   LTL biểu diễn các thuộc tính an toàn và phản hồi của hệ thống theo thời gian, cho phép mô tả các điều kiện như "luôn luôn đúng" hoặc "cuối cùng xảy ra". Trong BMC, các thuộc tính LTL được chuyển đổi thành công thức Boolean để kiểm tra bằng SAT.

4. Công cụ NuSMV hỗ trợ kiểm chứng mô hình như thế nào?
   NuSMV cho phép mô hình hóa hệ thống hữu hạn trạng thái bằng ngôn ngữ SMV, hỗ trợ kiểm chứng các thuộc tính LTL và CTL bằng kỹ thuật BDD và SAT. Công cụ cung cấp phản ví dụ chi tiết giúp người dùng định vị lỗi.

5. Làm thế nào để xác định giới hạn k trong BMC?
   Giới hạn k thường được tăng dần để tìm phản ví dụ. Nếu không tìm thấy phản ví dụ trong k bước, có thể tăng k hoặc sử dụng các kỹ thuật như k-induction để chứng minh tính đúng đắn. Việc xác định k tối ưu liên quan đến đường kính hệ thống, tuy nhiên đây là bài toán khó và thường được ước lượng theo thực tế.

Kết luận

• Kiểm chứng mô hình giới hạn dựa trên SAT là phương pháp hiệu quả, tiết kiệm bộ nhớ và thời gian trong phát hiện lỗi phần mềm phức tạp.
• Phương pháp này khắc phục được hạn chế của kiểm chứng mô hình biểu trưng với BDD, đặc biệt không yêu cầu sắp xếp biến phức tạp.
• Thực nghiệm trên công cụ NuSMV với mô hình hệ thống thư viện chứng minh tính khả thi và hiệu quả của phương pháp.
• Đề xuất mở rộng ứng dụng BMC trong phát triển phần mềm và nghiên cứu kiểm chứng mô hình với SMT cho các hệ thống phức tạp hơn.
• Khuyến khích đào tạo và phát triển công cụ hỗ trợ tự động hóa kiểm chứng mô hình nhằm nâng cao chất lượng phần mềm trong thực tế.

Áp dụng phương pháp BMC trong các dự án phát triển phần mềm, đồng thời nghiên cứu mở rộng sang kiểm chứng mô hình SMT để xử lý các hệ thống đa dạng và phức tạp hơn.

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

Chương 1 Kiểm chứng mô hình 1. Giới thiệu về kiểm chứng mô hình 1. Giới thiệu Độ tin cậy của chúng ta về các chức năng của các hệ thống ICT (Công nghệ thông tin và truyền thông) tăng lên nhanh chóng. Những hệ thống này đang trở nên phức tạp hơn và ngày càng chiếm một phần không thể thiếu trong cuộc sống hàng ngày của chúng ta thông qua Internet và các loại hệ thống nhúng như thẻ thông minh (smart cards), điện thoại di động, máy tính bảng,.

Từ năm 1995, người ta đã ước tính được rằng chúng ta sẽ phải làm việc với khoảng 25 thiết bị ICT trong một ngày. Các dịch vụ như ngân hàng điện tử và mua sắm qua mạng đã trở thành hiện thực. Dòng tiền hàng ngày thông qua Internet là khoảng 10 triệu đô la Mỹ. 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 báy được dành cho các hệ thống xử lý thông tin.

Các hệ thống thông tin phổ biến có mặt ở khắp mọi nơi. Các hệ thống thông tin điều khiển thị trường chứng khoán, quan trọng với hệ thống Internet và quan trong đối với các hệ thống trong y tế,. Độ tin cậy của các hệ thống thông tin có tầm quan trọng trong xã hội. Với các lỗi xảy ra với các hệ thống có thể gây ra những tổn thất rất nghiêm trọng.

Một vài ví dụ mà chúng ta đã biết đến như các lỗi trong bộ chia dấu phẩy động của Intel Pentium II trong đầu những năm 90 gây ra thiệt hại khoảng 450 triệu đô la Mỹ để thay thế các bộ vi xử lý lỗi, và danh tiếng của Intel cũng đã bị ảnh hưởng. Các lỗi phần mềm trong hệ thống xử lý hành lý đã làm trì hoãn việc mở cửa sân bay Denver trong 9 tháng, mỗi ngày mất 1. Hai mươi bốn giờ sau sự thất bại của hệ thống đặt vé trực tuyến của một công ty máy bay lớn trên thế giới sẽ gây ra phá sản vì các đơn đặt hàng bị bỏ lỡ. Đối với một số z 8 lỗi trong các hệ thống có thể gây ra thảm họa[3].

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, sau 36 giây kể từ khi ra khỏi bệ phóng đã bị rơi chỉ do lỗi chuyển đổi số thực 32 bit sang số nguyên 16 bit (hình 1.1: Tàu vũ trụ Ariane-5 vào tháng 4 năm 1996 Tầm quan trọng cũng như sự phức tạp của hệ thống ICT tăng lên nhanh chóng. Các hệ thống ICT không còn độc lập, mà được nhúng vào một hệ thống lớn, tương tác và kết nối với các thành phần và hệ thống khác. Do đó, chúng trở nên dễ bị lỗi - số các lỗi phát triển theo cấp số nhân đối với số các tương tác với các thành phần hệ thống. Đặc biệt, tính tương tranh và tính không đơn định của mô hình tương tác hệ thống lại khó xử lý với các kỹ thuật chuẩn.

Độ phức tạp của hệ thống ICT ngày càng tăng cùng với những áp lực làm cho thời gian phát triển hệ thống, điều này đã làm cho việc cung cấp các hệ thống ICT với ít khuyết điểm là vô cùng khó khăn và phức tạp. Kiểm định trong phần cứng và phần mềm Kỹ thuật kiểm định hệ thống đang được áp dụng để thiết kế các hệ thống ICT có độ tin cậy cao. Nói chung, kiểm định hệ thống được sử dụng để xác minh xem hệ thống có đạt được những đặc tính nhất định. Các đặc tính được kiểm chứng có thể rất cơ bản, ví dụ, một hệ thống không nên đến được trạng thái mà ở đó tiến trình không thể thực hiện (kịch bản của deadlock), và chủ yếu được lấy từ đặc tả của hệ thống.

Đặc tả này quy định những gì hệ thống phải làm và những gì không, z 9 và do đó tạo nên cơ sở cho bất kỳ hoạt động kiểm định nào. Một khuyết điểm được tìm thấy một khi hệ thống không đáp ứng được một trong các thuộc tính của đặc tả. Hệ thống được xem xét là "đúng" khi hệ thống thỏa mãn tất cả các thuộc tính lấy từ đặc tả của hệ thống. Vì vây, tính đúng đắn luôn luôn tương đối với đặc tả, và không có một thuộc tính tuyết đối của hệ thống.

Một sơ đồ của kiểm định được mô tả trong hình 1. Đặ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ơ đồ kiểm định hệ thống Từ đặc tả hệ thống được sử dụng để thiết kê và từ thiết kế đưa ra các sản phẩm, bản thử. Đồng thời từ đặc tả hệ thống cũng đưa ra được các tính chất của hệ thống. Sau đó, các tính chất và sản phẩm, bản thử sẽ được sử dụng để kiểm chứng.

Kết quả thu được có thể là tìm thấy lỗi hoặc không tìm thấy lỗi. Kiểm chứng mô hình Trong thiết kế phần mềm và phần cứng của các hệ thống phức tạp, nhiều thời gian và công sức dành cho việc kiểm định hơn là việc xây dựng hệ thống. Các kỹ thuật được tìm kiếm để giảm thiểu những nỗ lực kiểm định trong khi gia tăng độ bao phủ. Các phương pháp hình thức đưa ra một triển vọng lớn để có thể tích hợp kiểm chứng trong quá trình thiết kế, cung cấp các kỹ thuật kiểm chứng hiệu quả hơn và giảm bớt thời gian kiểm chứng.

Kỹ thuật kiểm chứng dựa trên mô hình được dựa trên sự mô tả mô hình của các hành vi có thể của hệ thông qua những công thức toán học rõ ràng và chính xác. z 10 Hóa ra là, trước khi kiểm định bằng bất cứ hình thức nào, việc xây dựng mô hình chính xác của các hệ thống thường dẫn đến việc phát hiện ra sự không đầy đủ, không rõ ràng và không nhất quán trong đặc tả hệ thống. Những vấn đề như vậy thường chỉ được phát hiện ra rất lâu sau giai đoạn thiết kế. Các mô hình cùng với các thuật toán có thể khai thác tất cả các trạng thái của hệ thống.

Điều này cung cấp cơ bản cho một loạt các kỹ thuật kiểm chứng khác nhau, từ sự khám phá một cách toàn diện mô hình (kiểm chứng mô hình) tới những thực nghiệm trên một tập hợp các hạn chế của các kịch bản trong mô hình (mô phỏng), hoặc trong thực tế (thử nghiệm). Do không ngừng cải tiến thuật toán và cấu trúc dữ liệu cùng với sự phát triển mạnh mẽ của máy tính với tốc độ xử lý và bộ nhớ tăng lên một cách đáng kể, kỹ thuật kiểm chứng dựa trên mô hình cách đây một thập kỷ chỉ áp dụng với những ví dụ đơn giản thì bây giờ đã có thể áp dụng với những thiết kế thực tế. Kiểm chứng mô hình là một kỹ thuật kiểm chứng xem xét tất cả các trạng thái có thể của hệ thống theo cách vét cạn. Tương tự như chương trình chơi cờ của máy tính kiểm tra những nước đi có thể, công cụ kiểm chứng giúp cho việc kiểm chứng mô hình, xem xét tất cả các kịch bản hệ thống có thể xảy ra theo một cách có hệ thống.

Theo cách này, nó có thể chỉ ra rằng mô hình hệ thống thực sự thỏa mãn với một đặc tính nhất định. Đó là một thách thức thật sự để kiểm tra không gian rộng lớn các trạng thái có thể. Những công cụ kiểm chứng tốt nhất hiện tại có thể xử lý không gian trạng thái khoảng 108 tới 109 trạng thái với không gian trạng thái được liệt kê tường minh, sử dụng khéo léo thuật toán và cấu trúc dữ liệu phù hợp. Một không gian các trạng thái lớn (1020 thậm chí lên tới 10476 trạng thái) có thể được xử lý cho những vấn đề cụ thể.

Thậm chí những lỗi tinh vi chưa được phát hiện bằng mô phỏng, kiểm tra, và giả lập có thể bị lộ ra bằng cách sử dụng kiểm chứng mô hình. Mô hình hệ thống thường được sinh một cách tự động từ mô tả của hệ thống, và mô tả của hệ thống được xác định trong một số ngôn ngữ chương trình giống như C hoặc Java hoặc ngôn ngữ mô tả hệ thống như Verilog hoặc VHSIC Hardware Description Language. Chú ý rằng, thuộc tính đặc tả quy định cái gì mà hệ thống nên làm, và cái gì mà hệ thống không nên làm, trong khi đó, mô tả của hệ thống xác định hệ thống hoạt động như thế nào? Công cụ kiểm chứng kiểm tra tất cả các trạng thái có liên quan của hệ thống để kiểm tra xem chúng có thỏa mãn với đặc tính mà bạn mong muốn hay không. Nếu trạng thái gặp phải là vi phạm đặc tính đang xem xét, Công cụ kiểm chứng sẽ cung cấp một phản ví dụ cho thấy việc z 11 làm thế nào mà mô hình có thể tới được trạng thái không mong muốn.

Phản ví dụ cũng mô tả một đường dẫn thực thi có thể dẫn tới từ những trạng thái khởi tạo của hệ thống tới những trạng thái vi phạm thuộc tính đang được kiểm chứng. Với sự giúp đỡ của mô phỏng, người sử dụng có thể xem lại các kịch bản vi phạm để có được những thông tin gỡ lỗi có ích và tích hợp các mô hình phù hợp (xem hình 1. Yều cầu Hệ thống (Requirements) (System) Hình thức hóa Mô hình hóa (Formalizing ) (Modeling ) Đặc tả thuộc tính (Property specification ) Kiểm chứng mô hình Mô hình hệ thống (Model checking ) (System model ) Thỏa mãn (satisfied ) Vi phạm, phản ví dụ Mô phỏng Định vị lỗi (Violated, (Simulation) (Location error) counterexample ) Hình 1.3: Sơ đồ tổng quan hướng tiếp cận kiểm chứng mô hình Một hệ thống được mô hình hóa qua các trạng thái và các dịch chuyển thành một mô hình hệ thống, các đặc tả yêu cầu được hình thức hóa qua logic thời gian thành các đặc tả thuộc tính. Đây là hai đầu vào của kiểm chứng mô hình.

Kiểm chứng mô hình có thể đưa ra kết quả là thỏa mãn hoặc là vi phạm và có phản ví dụ và có thể được mô phỏng nhờ mô hình hệ thống để định vị các lỗi. Các tiến trình trong kiểm chứng mô hình Trong việc áp dụng kiểm chứng mô hình để thiết kế các pha khác nhau như sau: Pha Mô hình hóa giúp cho việc mô hình hóa hệ thống dưới sự xem xét bằng cách sử dụng ngôn ngữ mô tả mô hình của công cụ kiểm chứng bằng tay. Kiểm tra z 12 tính đúng đắn trước tiên và các đánh giá nhanh của mô hình để thực thi một vài mô phỏng.