Đăng ký Đăng nhập
Trang chủ 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 ths. c...

Tài liệu 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 ths. công nghệ thông tin

.PDF
63
227
52

Mô tả:

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ĐINH QUANG ĐẠT 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Ĩ CÔNG NGHỆ THÔNG TIN Hà Nội – 2013 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ĐINH QUANG ĐẠT NGHIÊN CỨU PHƯƠNG PHÁP KIỂM CHỨNG MÔ HÌNH PHẦN MỀM DỰA TRÊN SAT Ngành: Công nghệ thông tin Chuyên ngành: Công nghệ phần mềm Mã số: 60 48 10 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Nguyễn Trường Thắng Hà Nội – 2013 Phụ lục 3: 2 Mục lục Lời cam đoan 1 Mục lục 2 Danh mục các hình vẽ 4 Danh mục các ký hiệu và chữ viết tắt 5 1 7 Kiểm chứng mô hình 1.1 Giới thiệu về kiểm chứng mô hình . . . . . . . . . . . . . . . . . . . .7 1.1.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 1.1.2 Kiểm định trong phần cứng và phần mềm . . . . . . . . . . . . .8 1.1.3 Kiểm chứng mô hình . . . . . . . . . . . . . . . . . . . . . . .9 1.1.4 Các tiến trình trong kiểm chứng mô hình . . . . . . . . . . . . 11 . 1.1.5 Mặt mạnh và mặt yếu của kiểm chứng mô hình . . . . . . . . . 12 . 1.2 Các kiến thức nền tảng . . . . . . . . . . . . . . . . . . . . . . . . . 13 . 1.2.1 Hệ thống dịch chuyển . . . . . . . . . . . . . . . . . . . . . . 13 . 1.2.2 Logic thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . 16 . 1.2.3 Logic thời gian tuyến tính (LTL) và logic tính toán cây (CTL) . 17 . 2 Vấn đề bùng nổ trạng thái và cách giải quyết sử dụng BDD 22 2.1 Vấn đề của bùng nổ trạng thái trong kiểm chứng mô hình . . . . . . . 22 . 2.2 Cách giải quyết theo hướng tiếp cận cổ điển . . . . . . . . . . . . . . 23 . 2.2.1 Thuật toán điểm cố định . . . . . . . . . . . . . . . . . . . . . 23 . 2.2.2 Kiểm chứng mô hình tương trưng với OBDDs . . . . . . . . . 25 . 3 Kiểm chứng mô hình giới hạn sử dụng bộ giải công cụ SAT 31 3.1 Các thuộc tính an toàn . . . . . . . . . . . . . . . . . . . . . . . . . 32 . 3.2 Giải công cụ SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 . 3 3.3 Xác định giới hạn . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 . 3.4 BMC cho các thuộc tính LTL . . . . . . . . . . . . . . . . . . . . . . 37 . 3.5 Giới thiệu về SMT . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 . 4 Ngôn ngữ SMV, công cụ NuSMV và thực nghiệm 43 4.1 Ngôn ngữ SMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 . 4.1.1 Kiểu dữ liệu trong SMV . . . . . . . . . . . . . . . . . . . . . 43 . 4.1.2 Phép toán trong SMV . . . . . . . . . . . . . . . . . . . . . . 44 . 4.2 Công cụ NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 . 4.3 Thực nghiệm sử dụng công cụ NuSMV . . . . . . . . . . . . . . . . 45 . Kết luận 60 Tài liệu tham khảo 61 4 Danh sách hình vẽ 1.1 Tàu vũ trụ Ariane-5 vào tháng 4 năm 1996 . . . . . . . . . . . . . . . .8 1.2 Sơ đồ kiểm định hệ thống . . . . . . . . . . . . . . . . . . . . . . . . .9 1.3 Sơ đồ tổng quan hướng tiếp cận kiểm chứng mô hình . . . . . . . . . 11 . 1.4 Một hệ thống dịch chuyển T mà T |= FGp nhưng T ̸|= AFAGp. . . . 21 . 2.1 Minh họa cho việc tính toán EFp . . . . . . . . . . . . . . . . . . . 25 . 2.2 Minh họa OBDD cho công thức (w ∧ x) ∨ (y ∧ z) . . . . . . . . . . . 26 . 2.3 Xây dựng dạng chính tắc OBDD từ một công thức (w ∧ x) ∨ (y ∧ z) . 28 . 3.1 Một đường dẫn dạng lasso. . . . . . . . . . . . . . . . . . . . . . . . 38 . 3.2 Chuyển dịch của J f UgKik . . . . . . . . . . . . . . . . . . . . . . . . 40 . 3.3 Chuyển dịch của l J f UGKik với vòng lặp . . . . . . . . . . . . . . . . . 40 . 4.1 Biểu đồ lớp các yêu cầu của hệ thống thư viện . . . . . . . . . . . . . 46 . 4.2 Kiểm chứng một thuộc tính với BMC . . . . . . . . . . . . . . . . . 59 . 5 DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT ICT Information and communications technology VHDL VHSIC Hardware Description Language LTL Linear Temporal Logic CTL Computation tree logic PTL Propositional Temporal Logic BDD Binary Decision Diagram BMC Bounded Model Checking SAT Boolean Satisfiability Problem SMT Satisfiability Modulo Theories OBDD Ordered binary decision diagrams DPLL Davis Putnam Logemann Loveland 6 LỜI MỞ ĐẦU Ngày nay, với tốc độ phát triển cực kỳ nhanh của lĩnh vực công nghệ thông tin tại Việt Nam và trên thế giới, nhất là đối với phần mềm đã thâm nhập vào hầu hết các lĩnh vực của đời sống như mua bán (mua hàng trực tuyến, các ứng dụng về kế toán, quản lý, . . . ), các lĩnh vực ngân hàng (quản lý tài khoản, giao dịch trực tuyến, . . . ), các lĩnh vực giải trí (trò chơi, phim ảnh, . . . ). Với sự bùng nổ về số lượng các phần mềm thì việc đảm bảo về chất lượng đang là những yêu cầu cấp bách trong hoàn cảnh hiện nay. Trên thế giới đã có rất nhiều bài báo, đề tài, công trình nghiên cứu về kiểm chứng mô hình, về các hướng khác nhau của kiểm chứng mô hình nhưng hướng nghiên cứu tập trung vào giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình luôn luôn là đề tài mang lại nhiều tranh luận, cảm hứng cũng như nghiên cứu nhất. Tác giả muốn nghiên cứu về vấn đề kiểm chứng mô hình liên quan tới vấn đề bùng nổ không gian trạng thái của kiểm chứng mô hình với một kỹ thuật mới nhất hiện nay đó là kiểm chứng mô hình giới hạn dựa trên SAT. Đồng thời dựa trên các kết quả đã được nghiên cứu tìm hiểu, tác giả cũng cài đặt thực nghiệm sử dụng kỹ thuật đã nghiên cứu, tìm hiểu. Bố cục của luận văn bao gồm 4 chương : • Chương 1: Giới thiệu về kiểm chứng mô hình và các kiến thức nền tảng của kiểm chứng mô hình. • Chương 2: Trình bày về 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. • Chương 3: Trình bày về SAT và cách giải bài toán bùng nổ không gian trạng thái sử dụng kiểm chứng mô hình giới hạn dựa trên SAT. • Chương 4: Trình bày về ngôn ngữ SMV, công cụ NuSMV và thực nghiêm sử dụng NuSMV. 7 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.1.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.1 triệu USD. 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ố 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). 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. 1.1.2. 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, 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.2. Đặc tả hệ thống (System specification ) Thiết kế (Design) Thuộc tính (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. 1.1.3. 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. 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 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.3). Yều cầu (Requirements) Hệ thống (System) Hình thức hóa (Formalizing ) Mô hình hóa (Modeling ) Đặc tả thuộc tính (Property specification ) Kiểm chứng mô hình (Model checking ) Mô hình hệ thống (System model ) Thỏa mãn (satisfied ) Vi phạm, phản ví dụ (Violated, counterexample ) Mô phỏng (Simulation) Định vị lỗi (Location error) 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. 1.1.4. 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 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. Mô hình hóa các đặc tính để kiểm tra sử dụng ngôn đặc tả các thuộc tính; Pha Thực thi chạy công cụ kiểm chứng để kiểm tra tính hợp lệ của thuộc tính trong mô hình hệ thống. Pha Phân tích kiểm tra xem thuộc tính có an toàn hay không? sau đó kiểm tra thuộc tính tiếp theo (nếu có thể); Thuộc tính có vi phạm hay không? nếu có thì phân tích phản ví dụ được sinh ra từ mô phỏng, làm mịn mô hình, thiết kế, và các thuộc tính và lặp lại toàn bộ thủ tục. Thoát ra khỏi bộ nhớ? sau đó Cố gắng làm giảm mô hình và thử lại. 1.1.5. Mặt mạnh và mặt yếu của kiểm chứng mô hình Kiểm chứng mô hình đã có rất nhiều ưu điểm tuy nhiên vẫn không thể tránh khỏi được những khuyết điểm. Một số ưu điểm và khuyết điểm của kiểm chứng mô hình có thể được thể hiện như sau. Về ưu điểm kiểm chứng mô hình hướng tiếp cận chung có thể áp dụng với một phạm vi rộng lớn các ứng dụng như các hệ thống nhúng, công nghệ phần mềm và thiết kế phần cứng. Kiểm chứng mô hình hỗ trợ kiểm chứng từng phần, các thuộc tính có thể được kiểm tra riêng lẻ, do đó cho phép tập trung vào những đặc tính quan trọng trước tiên. Không có đặc tả yêu cầu nào trọn vẹn là cần thiết. Tìm ra các lỗi khó bị phát hiện, điều này trái ngược với kiểm tra và mô phỏng nhằm mục đích tìm những khuyết điểm có thể xảy ra nhất. Kiểm chứng mô hình cung cấp các chuẩn đoán về thông tin trong trường hợp thuộc tính không có giá trị; điều này có ích trong việc hỗ trợ sửa lỗi. Việc sử dụng kiểm chứng mô hình yêu cầu không cần mức độ cao về sự tương tác của người dùng cũng không cần trình độ cao về chuyên môn. Kiểm chứng mô hình có được sự quan tâm, thu hút tăng lên nhanh chóng bởi ngành công nghiệp; Kiểm chứng mô hình có thể dễ dàng tích hợp trong vòng đời phát triển hiện có; Kiểm chứng mô hình dựa trên một nền tảng toán học vững chắc; Các khuyết điểm của kiểm chứng mô hình được thể hiện qua các điểm như sau, kiểm chứng mô hình chủ yếu thích hợp với các ứng dụng chuyên về điều khiển và chưa phù hợp với các ứng dụng chuyên về cơ sở dữ liệu. Các ứng dụng của kiểm chứng mô hình chinh phục các vấn đề có thể giải được; đối với hệ thống vô hạn trạng thái hoặc luận lý về kiểu dữ liệu trừu tượng (yêu các logic không giải được và giải được một nửa), kiểm chứng mô hình nói chung là tính toán không hiệu quả. Kiểm chứng mô hình chủ yếu kiểm chứng mô hình của hệ thống, và không kiểm chứng hệ thống thực sự (sản phẩm hoặc bản nguyên mẫu); và kết quả thu được tốt là do mô hình hệ thống. Các 13 kỹ thuật bổ xung, như kiểm tra, cần được tìm những sai lầm hư cấu (đối với phần cứng) hoặc những lỗi của mã nguồn (đối với phần mềm). Kiểm chứng mô hình chỉ kiểm tra những trạng thái yêu cầu. Không có đảm bảo nào là kiểm tra được hết các trạng thái. Các thuộc tính hợp lệ không được kiểm tra không thể được xem xét. Kiểm chứng mô hình vướng phải vấn đề bùng nổ không gian trạng thái. Số lượng các trạng thái cần của hệ thống thực có thể vượt quá bộ nhớ của máy tính. Cách sử dụng của kiểm chứng mô hình đòi hỏi phải có một số chuyên gia trong việc trừu tượng hóa hệ thống để có được mô hình hệ thống nhỏ hơn với ít thuộc tính trạng thái hơn. Kiểm chứng mô hình không đảm bảo mang lại kết quả chính xác, với bất kỳ công cụ nào, công cụ kiểm chứng mô hình có thể chứa các khiếm khuyết về phần mềm. Kiểm chứng mô hình không cho phép kiểm tra một cách tổng quát.// Mặc dù vẫn còn tồn tại những khuyết điểm như vậy nhưng kiểm chứng mô hình vần là một kỹ thuật tiềm năng để phát hiện ra những lỗi trong phần cứng và phần mềm. Tiếp theo luận văn sẽ đề cập đến các kiến thức nền tảng sẽ được sử dụng trong kiểm chứng mô hình. 1.2. Các kiến thức nền tảng 1.2.1. Hệ thống dịch chuyển Hệ thống dịch chuyển thường được sử dụng trong khoa học máy tính như các mô hình mô tả hành vi của hệ thống. Hệ thống dịch chuyển về cơ bản là các đồ thị có hướng với các nút thể hiện các trạng thái, các cạnh mô hình cho các chuyển dịch. Định nghĩa 1.2.1. Hệ thống dịch chuyển [3] Một hệ thống dịch chuyển TS là một bộ (S , Act, −→, I, AP, L) trong đó • S là tập hợp các trạng thái, • Act là tập hợp các hành động, • −→⊆ S × Act × S là một quan hệ dịch chuyển, • I ⊆ S là tập hợp các trạng thái khởi tạo, • AP là tập hợp những mệnh đề nguyên tử, và • L : S −→ 2AP là một nhãn của hàm. 14 T S được gọi là hữu hạn nếu S , Act, và AP là hữu hạn. α Viết s −→ − s′ thay cho (s, α, s′ ) ∈−→. Các hành động trực quan của hệ thống dịch chuyển có thể được mô tả như sau: hệ thống dịch chuyển bắt đầu tại một số trạng thái khởi tạo s0 ∈ I và tiến triển theo quan hệ dịch chuyển −→. Có nghĩa là, α nếu s là trạng thái hiện tại, sau đó một chuyển dịch s −→ − s′ bắt đầu từ s được chọn không đơn định và thực hiện, nghĩa là hành động α đươc thực thi và hệ thống dịch chuyển tiến triển từ trạng thái s tới trạng thái s′ . Thủ tục lựa chọn này được lặp đi lặp lại trong trạng thái s′ và kết thúc ở trạng thái mà không dịch chuyển được nữa. Nếu I là rỗng , thì hệ thống dịch chuyển không có hành vi nào và cũng không có trạng thái khởi tạo nào được chọn lựa. Nhãn của hàm L quan hệ với tập L(s) ∈ 2AP của các mệnh đề nguyên tử tới một vài trạng thái s. Cho Φ là một công thức logic mệnh đề, s thỏa mãn công thức Φ nếu sự ước lượng cảm ứng bởi L(s) làm cho công thức Φ true; nghĩa là: s |= Φ ⇔ L(s) |= Φ. Định nghĩa 1.2.2. Predecessors và Successors trực tiếp[3] Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. Với s ∈ S và α ∈ Act, tập hợp của α − successors được định nghĩa như sau: ∪ α Post(s, α) = {s′ ∈ S |s −→ − s′ }, Post(s) = Post(s, α). α∈Act Tập hợp của α − predecessors được định nghĩa bằng: ∪ α Pre(s, α) = {s′ ∈ S |s′ −→ − s}, Pre(s) = Pre(s, α). α∈Act Mỗi trạng thái s′ ∈ Post(s, α) được gọi là α − successor trực tiếp của s. Theo đó mỗi trạng thái s′ ∈ Post(s) được gọi là phần tử kế tiếp trực tiếp của s. Chú ý là tập hợp các phần tử kế tiếp trực tiếp được mở rộng tới các tập con của S theo cách hiển nhiên: cho C ⊆ S ,lấy Post(C, α) = ∪ s∈C Post(s, α), Post(C) = ∪ Post(s). s∈C Với Pre(C, α) và Pre(C) cũng được định nghĩa tương tự. Trạng thái kết thúc của một hệ thống dịch chuyển T S là các trạng thái không có bất kỳ chuyển dịch đi ra nào. Một khi hệ thống được mô tả bởi T S đạt được một trạng thái kết thúc, toàn bộ hệ thống sẽ dừng lại. 15 Định nghĩa 1.2.3. Trạng thái dừng[3] Trạng thái s trong hệ thống dịch chuyển T S gọi là dừng khi và chỉ khi Post(s) = ∅ Hệ thống dịch chuyển[3, 11? ] không đơn định được đề cập ở đây là cái cốt yếu cho việc mô hình các hệ thống máy tính. Tuy nhiên, rất tiện lợi để xem xét hệ thống với hành vi quan sát được là đơn định. Có hai hướng tiếp cận nói chung để hình thức hóa các hành vi thấy được của hệ thống dịch chuyển: một hướng dựa vào các hành động, một hướng dựa vào các nhãn của các trạng thái. Trong khi hướng tiếp cận dựa vào hành vi cho rằng chỉ có các hành động thực thi có thể quan sát từ bên ngoài, hướng tiếp cận dựa trên trạng thái bác bỏ hành động và dựa vào các mệnh đề nguyên tử chứa trạng thái hiện thời có thể nhìn thấy. Các hệ thống dịch chuyển đơn định theo quan điểm dựa vào hành vi có phần lớn có nhiều nhất một nhãn dịch chuyển đi ra với hành động α cho mỗi trạng thái, trong khi các hệ thống dịch chuyển đơn định theo quan điểm của các nhãn trạng thái, nghĩa là với bất kỳ nhãn trạng thái A ∈ 2AP và bất kỳ trạng thái nào có nhiều nhất một dịch chuyển đi ra dẫn tới một trạng thái với nhãn A. Trong cả hai quan điểm, đều yêu cầu có nhiều nhất một trạng thái khởi tạo. Định nghĩa 1.2.4. Hệ thống dịch chuyển đơn định[3] Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. 1. T S được gọi là action − deterministic (hành vi đơn định) nếu |I| ≤ 1 và |Post(s, α)| ≤ 1 với tất cả các trạng thái s và các hành động α. 2. T S được gọi là AP − deterministic nếu |I| ≤ 1 và |Post(s) ∩ {s′ ∈ S |L(s′ ) = A}| ≤ 1 với tất cả các trạng thái s và A ∈ 2AP . Cho đến nay, hành vi của hệ thống dịch chuyển đã được mô tả ở mức trực quan, và được hình thức hóa bằng cách sử dụng khái niệm executions (các sự thực thi). Một sự thực thi của một hệ thống dịch chuyển mô tả các hành vi có thể của hệ thống dịch chuyển: Định nghĩa 1.2.5. Đoạn thực thi[3] Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. Một đoạn thực thi hữu hạn ϱ của T S là một chuỗi xem kẽ của các trạng thái và các hành vi kết thúc với một trạng thái: αi+1 ϱ = s0 α1 s1 α2 ...αn sn sao cho si −−−→ si+1 với mọi 0 ≤ i < n, 16 với n ≥ 0. n là độ dài của đoạn thực thi ϱ. Một đoạn thực thi vô hạn ρ của T S là một chỗi vô hạn, xen kẽ của các trạng thái và các hành vi: αi+1 ρ = s0 α1 s1 α2 ... sao cho si −−−→ si+1 với mọi i ≥ 0. Các đoạn thực thi ϱ = s0 α1 ...αn sn và ρ = s0 α1 s1 α2 ... được viết tương ứng như sau: αn α1 α1 α2 ϱ = s0 −→ ... −→ sn và ρ = s0 −→ s1 −→ ... Một đoạn thực thi được gọi là tối đa khi không thể kéo dài thêm được nữa. Định nghĩa 1.2.6. Đoạn thực thi tối đa và đoạn thực thi khởi đầu[3] Một đoạn thực thi tối đa gồm cả đoạn thực thi hữu hạn kết thúc tại một trạng thái kết thúc, hoặc một đoan thực thi vô hạn. Một đoạn thực thi được gọi là khởi đầu nếu bắt đầu tại một trạng thái khởi tạo, nghĩa là s0 ∈ I Định nghĩa 1.2.7. Thực thi[3] Một thực thi của một hệ thống dịch chuyển T S là một đoạn thực thi khởi đầu và tối đa. Định nghĩa 1.2.8. Các trạng thái tới được[3] Cho T S = (S , Act, −→, I, AP, L) là một hệ thống dịch chuyển. Một trạng thái s ∈ S được gọi là tới được trong T S nếu tồn tại một đoạn thực thi khởi đầu và hữu hạn: α1 α2 αn s0 −→ s1 −→ ... −→ sn = s. Reach(T S ) biểu diễn tập hợp tất cả các trạng thái tới được trong T S . 1.2.2. Logic thời gian Đối với các hệ thống phản ứng, tính đúng đắn phụ thuộc vào sự thực thi của hệ thống, không chỉ là đầu vào và đầu ra của việc tính toán mà còn là vấn đề công bằng (fairness). Logic thời gian[4, 5, 8, 14] là một hình thức vượt trội để xử lý các vấn đề này. Logic thời gian mở rộng logic mệnh đề hoặc logic tân từ bằng cách cho phép chuyển tới hành vi vô hạn của một hệ thống phản ứng. Chúng cung cấp các ký hiệu một cách trực quan nhưng có một nền tảng toán học chính xác để diễn tả tính chất về mối quan hệ giữa các nhãn trạng thái trong thưc thi. Các hình thức 17 cơ bản của thời gian được thể hiện trong phần lớn các logic thời gian bao gồm hai toán hạng: ♢(hay còn được ký hiệu là F): cuối cùng trong tương lai. (hay còn được ký hiệu là G): bây giờ và sau này trong tương lai. Bản chất cơ bản của logic thời gian có thể là một trong hai loại tuyến tính (linear) hoặc phân nhánh (branching). Trong quan điểm của tuyến tính, ở mỗi thời điểm có một thời điểm kế tiếp, trong khi đó ở quan điểm của phân nhánh có cấu trúc như cây, nơi mà thời gian có thể phân thành các hướng khác nhau để lựa chọn. Năm 1977, Amir Pnueli đề xuất logic thời gian tuyến tính (LTL). Logic này được mở rộng từ logic mệnh đề với toán hạng thời gian G và F và khái niệm của tính công bằng (fairness) đảm bảo cho một đường dẫn ngữ nghĩa vô hạn. LTL đã được mở rộng sau đó gồm có toán hạng U (“until”: cho đến khi) được đưa ra bởi Kamp vào năm 1968 và toán hạng X (“next time”: thời gian tiếp theo) từ logic thời gian UB (hệ thống hợp nhất của thời gian phân nhánh). Vào năm 1981, Clarke và Emerson đã mở rộng UB, qua đó phát minh ra logic thời gian phân nhánh đặt tên là logic tính toán cây (CTL) và kiểm chứng mô hình CTL. Lichtenstein và Pnueli đã định nghĩa kiểm chứng mô hình cho LTL vào năm 1985. Hợp nhất giữa LTL và CTL, được gọi là CTL*, được định nghĩa bởi Emerson và Halpern vào năm 1986, mặc dù hiện tại vẫn không có công cụ kiểm chứng nào cho ngôn ngữ này. Vì cả hai kiểm chứng mô hình nói chung và kiểm chứng mô hình trừu tượng nói riêng ban đầu đều được định nghĩa cho CTL, và do đó, kiểm chứng mô hình LTL thường xuyên được định nghĩa trong các tài liệu liên quan tới kiểm chứng mô hình CTL. 1.2.3. Logic thời gian tuyến tính (LTL) và logic tính toán cây (CTL) Cho một hệ thống dịch chuyển T , chúng ta có thể đặt ra những câu hỏi như sau: - Có một vài trạng thái “không mong muốn” có thể truy cập ở trong T , chẳng hạn như trạng thái thể hiện deadlock, hoặc sự vi phạm của mutual exclusion, ...? - Có những hoạt động của T sao cho, từ một vài điểm trở về sau, một vài trạng thái “mong muốn” không bao giờ tới được hoặc một vài hành động không bao giờ được thực thi? Những hoạt động như vậy có thể tương trưng cho các 18 livelock, một ví dụ, một vài tiến trình bị ngăn chặn từ lúc đi vào phần then chốt của nó, mặc dù các thành phần khác của hệ thống có thể vẫn tiến hành. - Một vài trạng thái khởi tạo hệ thống của T có thể truy cập được từ mọi trạng thái? Nói cách khác, hệ thống có thể được thiết lập lại? Logic thời gian tuyến tính (LTL) Logic thời gian là một ngôn ngữ thuận tiện cho việc biểu thị hình thức các thuộc tính như vậy. Trước tiên chúng ta xem xét logic thời gian tuyến tính (LTL) với các công thức của nó biểu thị các thuộc tính của các hoạnh động trong các hệ thống dịch chuyển. Giả sử cho một tập hợp đếm được V của các mệnh đề nguyên tử, các mệnh đề nguyên tử thể hiện các thuộc tính của những trạng thái riêng lẻ. Lý luận của logic thời gian tuyến tính qua những dấu vết tuyến tính theo thời gian. Ở mỗi thời điểm, chỉ có một lịch trình trong tương lai thực sự xảy ra. Thông thường, lịch trình được định nghĩa như bắt đầu ở “hiện tại”, trong các bước thời gian hiện hành, và tiến triển vô hạn trong tương lai. Định nghĩa 1.2.9. Công thức của mệnh đề LTL[11] Những công thức của mệnh đề logic thời gian PTL trong thời gian tuyến tính được định nghĩa quy nạp như sau: - Mọi mệnh đề cơ bản v ∈ V là công thức. - Hợp của hai mệnh đề là một mệnh đề. - Nếu φ và ψ là các công thức thì Xφ và φUψ cũng là các công thức. Công thức PTL được diễn giải qua các hành vi. Chúng ta giả sử rằng mệnh đề cơ bản v ∈ V có thể đánh giá ở các trạng thái s ∈ S và viết s(V) để biểu diễn tập hợp của các mệnh đề đúng ở trạng thái s. Với hành vi σ = s0 s1 ..., lấy σi biểu diễn trạng thái si và σ|i hậu tố si si+1 ... của σ. Định nghĩa 1.2.10. Quan hệ nắm giữ LTL[11] Quan hệ σ |= φ (σ nắm giữ của φ) được định nghĩa quy nạp như sau: - σ |= v (với v ∈ V) khi và chỉ khi v ∈ σ0 (V). - Ngữ nghĩa của phép hợp được định nghĩa như bình thường. - σ |= Xφ khi và chỉ khi σ1 |= φ. 19 - σ |= φU khi và chỉ khi với một số k ≥ 0, σ|k |= ψ và σ| j |= φ nắm giữ với mọi 0 ≤ j ≤ k. Những công thức PTL hữu ích khác có thể được đưa ra như những từ viết tắt: Fφ (“cuối cùng φ”) được định nghĩa như true U φ; nó khẳng định rằng φ nắm giữ của một vài hậu tố. Công thức kép Gφ ≡ ¬F¬φ (“luôn luôn” φ) yêu cầu φ nắm giữ tất cả các hậu tố. Công thức φWψ (“φ chờ đợi ψ”,“φ trừ khi ψ”) được định nghĩa như (φUψ) ∨ Gφ và yêu cầu φ nắm giữ cho đến khi ψ không nắm giữ; không giống như φUψ, nó không yêu cầu ψ trở thành đúng ở sau cùng. Những công thức sau đây là những ví dụ điển hình khẳng định tính đúng đắn về quản lý tài nguyên của hai tiến trình. Chúng ta giả sử rằng reqi và ownsi là hai mệnh đề cơ bản đúng khi tiến trình được yêu cầu tài nguyên hoặc khi nó sở hữu tài nguyên. G¬(owns1 ∧ owns2 ): Không bao giờ trường hợp cả hai tiến trình đều sở hữu tài nguyên. Nói chung, các tính chất của hình thức Gp, cho các công thức không phải là thời gian p, biểu thị cho những bất biến của hệ thống (system invariants). G(req1 ⇒ Fowns1 ): Bất cứ khi nào tiến trình 1 yêu cầu tài nguyên, cuối cùng nó sẽ có được. Các công thức của hình thức này thường được gọi sụ phản hồi các thuộc tính (response properties). GF(req1 ∧ ¬(owns1 ∨ owns2 )) ⇒ GFowns1 : Nếu nó rất nhiều lần thường xảy ra trường hợp tiến trình 1 yêu cầu tài nguyên khi tài nguyên rảnh, sau đó tiến trình 1 rất nhiều lần thường sở hữu tài nguyên. Công thức này biểu thị tình trạng công bằng (mạnh) cho tiến trình 1. G(req1 ∧ req2 ⇒ (¬owns2 W(owns2 W(¬owns2 Wowns1 )))): Bất kì khi nào cả hai tiến trình cạnh trạnh tài nguyên, tiến trình 2 sẽ được cấp tài nguyên nhiều nhất một lần trước khi cấp cho tiến trình 1. Tính chất này là một ví dụ cho thuộc tính ưu tiên (precedence property). Cách tốt nhất được hiểu như sự khẳng định hiện hữu của cả 4, có thể trống hoặc được mở (right-open), những khoảng thời gian mà thỏa mãn những điều kiện tương ứng.
- Xem thêm -

Tài liệu liên quan