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 vnu uet nghiên cứu phương pháp kiểm chứng mô hình phần mềm dựa trên sat, khảo sát thực trạng, phân tích nguyên nhân, đề xuất giải pháp cải thiện thực

• 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: Nghiên Cứu 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. Kiểm định trong phần cứng và phần mềm
• 1.3. Kiểm chứng mô hình
• 1.4. Các tiến trình trong kiểm chứng mô hình
• 1.5. Mặt mạnh và mặt yếu của kiểm chứng mô hình
• 1.6. Các kiến thức nền tảng
• 1.6.1. Hệ thống dịch chuyển
• 1.6.2. Logic thời gian
• 1.6.3. Logic thời gian tuyến tính (LTL) và logic tính toán cây (CTL)
• 1.6.4. Vấn đề bùng nổ trạng thái và cách giải quyết sử dụng BDD
• 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
• 2.2.1. Thuật toán điểm cố định
• 2.2.2. Kiểm chứng mô hình tương trưng với OBDDs
• 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. Giới thiệu về kiểm chứng mô hình phần mềm dựa trên SAT

Kiểm chứng mô hình phần mềm là một kỹ thuật quan trọng trong lĩnh vực công nghệ thông tin, giúp đảm bảo rằng các hệ thống phần mềm hoạt động đúng như mong đợi. Mô hình hóa và kiểm chứng mô hình dựa trên SAT (Boolean Satisfiability Problem) đã trở thành một phương pháp hiệu quả để giải quyết các vấn đề phức tạp trong kiểm chứng phần mềm. Việc áp dụng SAT trong kiểm chứng mô hình giúp giảm thiểu bùng nổ trạng thái, một thách thức lớn trong lĩnh vực này.

1.1. Khái niệm về kiểm chứng mô hình phần mềm

Kiểm chứng mô hình phần mềm là quá trình xác minh rằng mô hình phần mềm đáp ứng các yêu cầu đã được xác định. Kỹ thuật này giúp phát hiện lỗi sớm trong quá trình phát triển phần mềm, từ đó nâng cao độ tin cậy của hệ thống.

1.2. Tầm quan trọng của SAT trong kiểm chứng mô hình

SAT là một công cụ mạnh mẽ trong việc kiểm chứng mô hình phần mềm. Nó cho phép xác định tính đúng đắn của các thuộc tính hệ thống bằng cách kiểm tra tất cả các trạng thái có thể, từ đó phát hiện ra các lỗi tiềm ẩn.

II. Vấn đề bùng nổ trạng thái trong kiểm chứng mô hình phần mềm

Bùng nổ trạng thái là một trong những thách thức lớn nhất trong kiểm chứng mô hình phần mềm. Khi số lượng trạng thái tăng lên theo cấp số nhân, việc kiểm tra tất cả các trạng thái trở nên không khả thi. Điều này dẫn đến việc bỏ sót nhiều lỗi nghiêm trọng trong phần mềm. Việc áp dụng các phương pháp như BDD (Binary Decision Diagrams) và SAT giúp giảm thiểu vấn đề này.

2.1. Nguyên nhân gây ra bùng nổ trạng thái

Bùng nổ trạng thái xảy ra khi số lượng trạng thái trong mô hình phần mềm tăng lên nhanh chóng do sự phức tạp của các tương tác giữa các thành phần. Điều này làm cho việc kiểm chứng trở nên khó khăn và tốn kém.

2.2. Giải pháp giảm thiểu bùng nổ trạng thái

Sử dụng các kỹ thuật như BDD và SAT có thể giúp giảm thiểu bùng nổ trạng thái bằng cách tối ưu hóa không gian trạng thái và chỉ kiểm tra những trạng thái quan trọng nhất.

III. Phương pháp kiểm chứng mô hình phần mềm dựa trên SAT

Phương pháp kiểm chứng mô hình dựa trên SAT cho phép xác minh các thuộc tính của hệ thống phần mềm một cách hiệu quả. Bằng cách sử dụng SAT solver, các nhà phát triển có thể kiểm tra tính đúng đắn của mô hình mà không cần phải kiểm tra từng trạng thái một cách thủ công.

3.1. Cách thức hoạt động của SAT solver

SAT solver hoạt động bằng cách chuyển đổi các thuộc tính cần kiểm chứng thành các biểu thức logic và sau đó tìm kiếm các giá trị biến để xác định tính đúng đắn của mô hình.

3.2. Lợi ích của việc sử dụng SAT trong kiểm chứng

Việc sử dụng SAT trong kiểm chứng mô hình giúp tiết kiệm thời gian và nguồn lực, đồng thời tăng cường độ chính xác trong việc phát hiện lỗi.

IV. Ứng dụng thực tiễn của kiểm chứng mô hình phần mềm dựa trên SAT

Kiểm chứng mô hình phần mềm dựa trên SAT đã được áp dụng thành công trong nhiều lĩnh vực, từ hệ thống nhúng đến phần mềm thương mại. Các nghiên cứu cho thấy rằng việc áp dụng phương pháp này giúp giảm thiểu lỗi và nâng cao chất lượng sản phẩm.

4.1. Các lĩnh vực ứng dụng chính

Kiểm chứng mô hình phần mềm dựa trên SAT được áp dụng rộng rãi trong các lĩnh vực như ô tô, hàng không, và hệ thống tài chính, nơi mà độ tin cậy là rất quan trọng.

4.2. Kết quả nghiên cứu và thực nghiệm

Nhiều nghiên cứu đã chỉ ra rằng việc áp dụng kiểm chứng mô hình dựa trên SAT giúp phát hiện lỗi sớm và giảm thiểu chi phí phát triển phần mềm.

V. Kết luận và tương lai của kiểm chứng mô hình phần mềm dựa trên SAT

Kiểm chứng mô hình phần mềm dựa trên SAT là một kỹ thuật hứa hẹn trong việc nâng cao độ tin cậy của phần mềm. Với sự phát triển không ngừng của công nghệ, các phương pháp kiểm chứng sẽ ngày càng trở nên hiệu quả hơn, giúp giải quyết các thách thức trong kiểm chứng phần mềm.

5.1. Tương lai của kiểm chứng mô hình phần mềm

Tương lai của kiểm chứng mô hình phần mềm sẽ tập trung vào việc phát triển các công cụ và kỹ thuật mới, giúp cải thiện hiệu suất và độ chính xác trong kiểm chứng.

5.2. Những thách thức cần vượt qua

Mặc dù kiểm chứng mô hình phần mềm dựa trên SAT đã đạt được nhiều thành công, nhưng vẫn còn nhiều thách thức cần giải quyết, đặc biệt là trong việc xử lý các hệ thống phức tạp và vô hạn trạng thái.

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) toàn cầu và tại Việt Nam, 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, dòng tiền giao dịch qua Internet hàng ngày đạt khoảng 10 triệu đô la Mỹ, đồng thời chi phí dành cho các hệ thống xử lý thông tin trong các phương tiện giao thông hiện đại chiếm khoảng 20% tổng chi phí phát triển. 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 trăm 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 bài toá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à ứng dụng công cụ NuSMV tại Việt Nam trong năm 2013. Mục tiêu chính là phát triển và thực nghiệm phương pháp kiểm chứng mô hình giới hạn dựa trên SAT, từ đó nâng cao hiệu quả kiểm chứng và giảm thiểu chi phí phát triển phần mềm.

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, mệnh đề nguyên tử và nhãn trạng thái.

• 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, bao gồm các toán tử như "cuối cùng" (F), "luôn luôn" (G), "cho đến khi" (U), và các toán tử phân nhánh như "mọi khả năng" (A) và "tồn tại khả năng" (E).

• 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): Biểu diễn tập hợp trạng thái bằng cấu trúc đồ thị nhị phân có thứ tự, giúp giảm thiểu kích thước không gian trạng thái.

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

• Satisfiability Modulo Theories (SMT): Mở rộng SAT bằng cách kết hợp các lý thuyết toán học như số nguyên, số thực, mảng, giúp mô hình hóa hệ thống phức tạp hơn.

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, SAT, SMT, cùng với thực nghiệm trên công cụ NuSMV.

• 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, thuật toán DPLL cho SAT, và kỹ thuật BMC. Thực nghiệm mô hình hóa hệ thống thư viện bằng ngôn ngữ SMV, kiểm chứng các thuộc tính an toàn bằng NuSMV.

• Timeline nghiên cứu: Nghiên cứu lý thuyết và thuật toán trong 6 tháng đầu, phát triển và cài đặt thực nghiệm trong 3 tháng tiếp theo, đánh giá kết quả và hoàn thiện luận văn trong 3 tháng cuối năm 2013.

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 cho phép tì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, sử dụng bộ nhớ ít hơn và không yêu cầu sắp xếp biến phức tạp. Ví dụ, với hệ thống chuyển trạng thái 3-bit, BMC phát hiện phản ví dụ thuộc tính an toàn Gp chỉ trong vòng 3 bước dịch chuyển.

2. Giải quyết vấn đề bùng nổ không gian trạng thái: BMC giới hạn độ dài phản ví dụ giúp giảm đáng kể không gian trạng thái cần kiểm tra, trong khi BDD thường gặp khó khăn khi kích thước BDD tăng theo hàm mũ với số biến lớn.

3. Ứng dụng công cụ NuSMV: Thực nghiệm trên hệ thống quản lý thư viện với các module member, book, join, leave cho thấy NuSMV có thể kiểm chứng các thuộc tính an toàn phức tạp như: sách chỉ bị loại bỏ khi không được mượn hay đặt trước, thành viên chỉ rời khỏi khi trả hết sách mượn, đảm bảo tính nhất quán và an toàn của hệ thống.

4. Khả năng mở rộng và tích hợp: NuSMV hỗ trợ cả CTL và LTL, tích hợp kỹ thuật kiểm chứng dựa trên BDD và SAT, phù hợp với nhiều loại hệ thống hữu hạn trạng thái, tạo nền tảng cho nghiên cứu và ứng dụng trong công nghiệp.

Thảo luận kết quả

Nguyên nhân thành công của BMC dựa trên SAT là do khả năng mã hóa hiệu quả các trạng thái và chuyển dịch thành công thức Boolean, tận dụng sức mạnh của các bộ giải SAT hiện đại dựa trên thuật toán DPLL với các cải tiến như lan truyền đơn vị và loại bỏ literal thuần túy. 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 kích thước BDD và không cần lựa chọn sắp xếp biến phức tạp, giúp xử lý các hệ thống lớn hơn.

Kết quả thực nghiệm với NuSMV minh họa tính khả thi của phương pháp trong thực tế, đồng thời cho thấy các thuộc tính an toàn được kiểm chứng đầy đủ, phản ví dụ được cung cấp giúp định vị lỗi nhanh chóng. Tuy nhiên, BMC vẫn có hạn chế khi không thể kiểm chứng đầy đủ các thuộc tính phức tạp vô hạn trạng thái hoặc các thuộc tính không thể biểu diễn trong giới hạn độ dài phản ví dụ.

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 trên hệ thống thư viện.

Đề 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: Khuyến nghị các tổ chức phát triển phần mềm phức tạp tích hợp BMC trong quy trình kiểm thử để phát hiện lỗi sớm, giảm chi phí sửa chữa, với mục tiêu giảm tỷ lệ lỗi phần mềm xuống dưới 5% trong vòng 12 tháng.

2. Phát triển công cụ hỗ trợ tự động hóa: Đầu tư phát triển các công cụ tự động chuyển đổi mô hình hệ thống sang ngôn ngữ SMV và tự động hóa kiểm chứng, nhằm rút ngắn thời gian chuẩn bị mô hình và tăng độ chính xác, hoàn thành trong 6 tháng tới.

3. Đào tạo chuyên gia kiểm chứng mô hình: Tổ chức các khóa đào tạo chuyên sâu về kiểm chứng mô hình, SAT, SMT cho kỹ sư phần mềm và nhà nghiên cứu, nâng cao năng lực chuyên môn, dự kiến triển khai trong năm học tiếp theo.

4. Nghiên cứu mở rộng sang SMT: Khuyến khích nghiên cứu và ứng dụng SMT để kiểm chứng các hệ thống vô hạn trạng thái hoặc có dữ liệu phức tạp, nhằm mở rộng phạm vi áp dụng kiểm chứng mô hình, với lộ trình nghiên cứu 2 năm.

Đố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, SAT, SMT, và ứng dụng thực tiễn qua công cụ NuSMV, phục vụ cho nghiên cứu và luận văn.

2. Kỹ sư phát triển phần mềm phức tạp: Á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, giảm thiểu lỗi phần mềm trong các hệ thống nhúng, tài chính, và giao dịch trực tuyến.

3. Chuyên gia kiểm thử phần mềm: Tích hợp kỹ thuật kiểm chứng mô hình vào quy trình kiểm thử tự động, tăng hiệu quả phát hiện lỗi và giảm thời gian kiểm thử.

4. Nhà quản lý dự án CNTT: Hiểu rõ tầm quan trọng của kiểm chứng mô hình trong quản lý rủi ro dự án, từ đó đầu tư hợp lý cho công tác đảm bảo chất lượng phần mềm.

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

1. Kiểm chứng mô hình là gì và tại sao quan trọng?
   Kiểm chứng mô hình là kỹ thuật xác minh 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. Nó giúp phát hiện lỗi sớm, giảm thiệt hại kinh tế và nâng cao độ tin cậy phần mềm, đặc biệt quan trọng với các hệ thống phức tạp và nhạy cảm.

2. Bùng nổ không gian trạng thái là gì?
   Là hiện tượng số lượng trạng thái của hệ thống tăng theo hàm mũ khi số lượng thành phần hoặc biến tăng, gây khó khăn cho việc kiểm chứng toàn diện. Ví dụ, hệ thống với n tiến trình mỗi tiến trình m trạng thái có thể có tới m^n trạng thái.

3. Phương pháp kiểm chứng mô hình giới hạn (BMC) hoạt động như thế nào?
   BMC giới hạn độ dài phản ví dụ cần tìm, mã hóa bài toán thành công thức Boolean và sử dụng bộ giải SAT để tìm phản ví dụ trong giới hạn đó. Nếu không tìm thấy, tăng giới hạn và lặp lại, giúp giảm thiểu không gian trạng thái cần kiểm tra.

4. Ưu điểm của BMC so với kiểm chứng mô hình biểu trưng với BDD?
   BMC sử dụng ít bộ nhớ hơn, không cần lựa chọn sắp xếp biến phức tạp, tìm phản ví dụ nhanh hơn và dễ dàng mở rộng cho các hệ thống lớn hơn, trong khi BDD có thể bị quá tải bộ nhớ và khó tối ưu.

5. Công cụ NuSMV hỗ trợ những tính năng gì?
   NuSMV hỗ trợ mô hình hóa hệ thống hữu hạn trạng thái bằng ngôn ngữ SMV, kiểm chứng các thuộc tính LTL và CTL, sử dụng kỹ thuật kiểm chứng dựa trên BDD và SAT, cung cấp phản ví dụ chi tiết giúp định vị lỗi hiệu quả.

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ả để giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng phần mềm.
• Phương pháp này giúp phát hiện lỗi nhanh chóng, sử dụng bộ nhớ tiết kiệm và không yêu cầu sắp xếp biến phức tạp như BDD.
• Công cụ NuSMV hỗ trợ thực nghiệm thành công các thuộc tính an toàn phức tạp trong hệ thống quản lý thư viện.
• Nghiên cứu mở ra hướng phát triển ứng dụng SMT để kiểm chứng các hệ thống vô hạn trạng thái trong tương lai.
• Đề xuất áp dụng rộng rãi BMC trong công nghiệp phần mềm, đồng thời đào tạo chuyên gia và phát triển công cụ hỗ trợ tự động hóa.

Các tổ chức và nhà nghiên cứu nên triển khai phương pháp BMC trong quy trình phát triển phần mềm, đồng thời tiếp tục nghiên cứu mở rộng ứng dụng SMT để nâng cao hiệu quả kiểm chứng mô hình.

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ố LUAN VAN CHAT LUONG download : add [e-mail] 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, LUAN VAN CHAT LUONG download : add [e-mail] 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. LUAN VAN CHAT LUONG download : add [e-mail] 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 LUAN VAN CHAT LUONG download : add [e-mail] 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.