Tài liệu Phương pháp tạo giả định tối thiểu áp dụng để kiểm chứng phần mềm hướng thành phẩm

1 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HIẾU PHƯƠNG PHÁP TẠO GIẢ ĐỊNH TỐI THIỂU ÁP DỤNG ĐỂ KIỂM CHỨNG PHẦN MỀM HƯỚNG THÀNH PHẦN LUẬN VĂN THẠC SĨ Hà Nội – 2009 2 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HIẾU PHƯƠNG PHÁP TẠO GIẢ ĐỊNH TỐI THIỂU ÁP DỤNG ĐỂ KIỂM CHỨNG PHẦN MỀM HƯỚNG THÀNH PHẦN Ngành: Công nghệ phần mềm Mã số : 6020611 LUẬN VĂN THẠC SĨ NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Lê Anh Cường Hà Nội – 2009 1 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HIẾU PHƯƠNG PHÁP TẠO GIẢ ĐỊNH TỐI THIỂU ÁP DỤNG ĐỂ KIỂM CHỨNG PHẦN MỀM HƯỚNG THÀNH PHẦN LUẬN VĂN THẠC SĨ Hà Nội – 2009 2 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HIẾU PHƯƠNG PHÁP TẠO GIẢ ĐỊNH TỐI THIỂU ÁP DỤNG ĐỂ KIỂM CHỨNG PHẦN MỀM HƯỚNG THÀNH PHẦN Ngành: Công nghệ phần mềm Mã số : 6020611 LUẬN VĂN THẠC SĨ NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Lê Anh Cường Hà Nội – 2009 1 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HIẾU PHƯƠNG PHÁP TẠO GIẢ ĐỊNH TỐI THIỂU ÁP DỤNG ĐỂ KIỂM CHỨNG PHẦN MỀM HƯỚNG THÀNH PHẦN LUẬN VĂN THẠC SĨ Hà Nội – 2009 2 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN HIẾU PHƯƠNG PHÁP TẠO GIẢ ĐỊNH TỐI THIỂU ÁP DỤNG ĐỂ KIỂM CHỨNG PHẦN MỀM HƯỚNG THÀNH PHẦN Ngành: Công nghệ phần mềm Mã số : 6020611 LUẬN VĂN THẠC SĨ NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Lê Anh Cường Hà Nội – 2009 1 MỤC LỤC MỤC LỤC ................................................................................................................... 1 DANH MỤC CÁC HÌNH VẼ ...................................................................................... 2 DANH MỤC CÁC CHỮ VIẾT TẮT ........................................................................... 3 MỞ ĐẦU ..................................................................................................................... 4 CHƢƠNG 1: TỔNG QUAN VỀ KIỂM CHỨNG PHẦN MỀM HƢỚNG THÀNH PHẦN .......................................................................................................................... 6 1.1 Giới thiệu ........................................................................................................... 6 1.2 Các khái niệm cơ bản ........................................................................................ 9 1.2.1 Labeled Transition System(LTS) ................................................................. 9 1.2.2 Dẫn xuất(Traces)........................................................................................ 10 1.2.3 Ghép nối song song(Parallel Composition) ................................................ 11 1.2.3 Safety LTSs, Safety Property, error LTS .................................................... 13 1.2.4 Sự thoả mãn(satisfying) ............................................................................. 14 1.2.5 Ôtomat đơn định hữu hạn trạng thái (Deterministic Finite State Automata) 14 1.3 Về vần đề đảm bảo giả định ............................................................................ 15 CHƢƠNG 2: TẠO GIẢ ĐỊNH SỬ DỤNG THUẬT TOÁN HỌC L* ........................ 18 2.1 Thuật toán học L* ............................................................................................. 18 2.2 Tạo giả định sử dụng thuật toán học L*............................................................. 21 CHƢƠNG 3: GIẢI THUẬT TẠO GIẢ ĐỊNH TỐI THIỂU ....................................... 25 3.1 Giới thiệu ......................................................................................................... 25 3.2 Định nghĩa giả định tối thiểu ............................................................................ 25 3.3 Giải thuật tạo giả định tối thiểu ........................................................................ 27 3.3.1 Tƣ tƣởng của giải thuật .............................................................................. 27 3.3.2 Chi tiết giải thuật tạo giả định tối thiểu....................................................... 28 3.3 Tính dừng và đúng đắn của giải thuật tạo giả định tối thiểu .............................. 31 3.3.1 Đặc điểm không gian tìm kiếm .................................................................. 31 3.3.2 Tính dừng và tính đúng đắn của giải thuật .................................................. 32 3.4 Ví dụ tạo giả định tối thiểu ............................................................................. 33 CHƢƠNG 4: THỰC NGHIỆM ................................................................................. 43 KẾT LUẬN ............................................................................................................... 53 TÀI LIỆU THAM KHẢO.......................................................................................... 55 PHỤ LỤC .................................................................................................................. 58 Phụ lục A ............................................................................................................... 58 Phụ lục B ............................................................................................................... 61 2 DANH MỤC CÁC HÌNH VẼ Hình 1.1: Ví dụ về LTS.............................................................................................. 10 Hình 1.2: Minh hoạ phép ghép nối song song ............................................................ 13 Hình 1.3: Phép ghép nối CLIENT || SERVER........................................................... 13 Hình 1.4: Minh hoạ tạo LTS an toàn từ một DFA. ..................................................... 15 Hình 1.5: Bài toán và tƣ tƣởng chính của cách tiếp cận xác minh đảm bảo giả định. .. 16 Hình 2.1: Minh hoạ mối quan hệ giữa Teacher và L* learner. .................................... 19 Hình 2.2: Giải thuật L*. ............................................................................................. 20 Hình 2.3: Một sơ đồ khối để tạo giả định sử dụng giải thuật L* [4, 8]. ....................... 22 Hình 3.1: Các thành phần của hệ thống trong ví dụ đƣợc xét ..................................... 26 Hình 3.2: Giả định đƣợc tạo ra sau khi sử dụng giải thuật L* ..................................... 26 Hình 3.3: Giả định đƣợc tạo ra bởi giải thuật tạo giả định tối thiểu. ........................... 26 Hình 3.4: Thủ tục để tìm giả định tối thiểu ................................................................. 30 Hình 3.5: Bảng quan sát ban đầu ................................................................................ 34 Hình 3.6: Hệ thống ghép nối Input || Ordererr.............................................................. 34 Hình 3.7: Mô hình cây tìm kiếm của các bảng quan sát. ............................................. 36 Hình 3.8: Hệ thống ghép nối A1.2.1 || Input|| Ordererr ................................................... 38 Hình 3.9: Hệ thống ghép nối Output || A1.2.1err ......................................................... 39 Hình 3.10: Cây tìm kiếm sau khi duyệt đến bảng quan sát 1.2.1................................. 40 Hình 3.11: Giả định kết quả ....................................................................................... 42 Bảng 4.1. Kết quả thực nghiệm .................................................................................. 43 Hình 4.1: FSPs và LTSs của hệ thống minh hoạ trong LTSA. .................................... 49 Hình 4.2: FSP và LTS của giả định tạo bởi giải thuật trong [1] và kết quả kiểm tra giả định bởi LTSA. .......................................................................................................... 50 Hình 4.3: FSP và LTS của giả định tạo bởi giải thuật tạo giả định tối thiểu và kết quả kiểm tra giả định bởi LTSA. ...................................................................................... 51 3 DANH MỤC CÁC CHỮ VIẾT TẮT CBSD Component-Based Software Development CBS FSP Component-Based Software Finite State Proces LTSA Labelled Transition Systems Analyzed 4 MỞ ĐẦU Phát triển phần mềm hƣớng thành phần (Component-Based Software Development - CBSD) là một trong những công nghệ quan trọng nhất trong kỹ nghệ phần mềm. Hệ thống phần mềm hƣớng thành phần đƣợc xây dựng dựa trên quá trình lựa chọn và ghép nối các thành phần riêng biệt thành một hệ thống hoàn chỉnh. Với cách tiếp cận này, phát triển phần mềm hƣớng thành phần đã góp phần rút ngắn thời gian thực hiện dự án, nâng cao chất lƣợng và độ tin cậy của sản phầm. Vì những ƣu điểm này mà công nghệ này đã đƣợc áp dụng rộng rãi trong quá trình phát triển các dự án phần mềm hiện nay. Tuy nhiên, một trong những hạn chế của CBSD là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với nhau vì các thành phần có thể đƣợc phát triển một cách độc lập hoặc đƣợc đặt mua từ các công ty thứ 3 (third parties). Hiện tại, các công nghệ hỗ trợ phát triển phần mềm hƣớng thành phần nhƣ CORBA (OMG), COM/DCOM or .NET (Microsoft), Java and JavaBeans (Sun), … vv chỉ hỗ trợ việc ghép nối các thành phần (component plugging). Chúng không có cơ chế kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với nhau hay không. Điều này có nghĩa là cơ chế “plug-and-play” không đƣợc đảm bảo. Một trong những giải pháp phổ biến để giải quyết vấn đề nêu trên là sử dụng các phƣơng pháp kiểm chứng mô hình (Model checking). Tuy nhiên, một trong những hạn chế lớn nhất của kiểm chứng mô hình là vấn đề bùng nổ không gian trạng thái khi kiểm chứng các phần mềm có kích thƣớc lớn. Một trong những cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần (modular verification - MV). Thay vì tiến hành kiểm chứng trên toàn bộ hệ thống gồm các thành phần đƣợc ghép nối với nhau, cách tiếp cận này tiến hành kiểm chứng trên từng thành phần riêng biệt. Với cách tiếp cận này, vấn đề bùng nổ không gian trạng thái hứa hẹn sẽ đƣợc giải quyết. Một trong những phƣơng pháp kiểm chứng hỗ trợ ý tƣởng này là phƣơng pháp kiểm chứng đảm bảo giả định (Assume-Guarantee Verification - AGV). Sử dụng tƣ tƣởng của chiến lƣợc “chia để trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhƣng kích thƣớc nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách riêng biệt. AVG đƣợc đánh giá là một phƣơng pháp hứa hẹn để kiểm chứng phần mềm hƣớng thành phần thông qua phƣơng pháp kiểm chứng mô hình. AVG không những thích hợp cho phần mềm hƣớng thành phần mà còn có khả 5 năng giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình. Trong phƣơng pháp này, các giả định (assumptions) (có vai trò nhƣ là môi trƣờng của các thành phần) sẽ đƣợc tạo lập. Việc tạo lập các giả định chính là bài toán quan trọng nhất trong phƣơng pháp này. Kích thƣớc của các giả định này (số lƣợng trạng thái) nên đƣợc cực tiểu hóa bởi vì chi phí cho quá trình kiểm chứng mô hình của phƣơng pháp này phụ thuộc chính vào thông số này. Đây chính là mục tiêu nghiên cứu của luận văn này. Với mục tiêu này, chúng tôi đề xuất một phƣơng pháp tạo giả định tối thiểu (có kích thƣớc nhỏ nhất) nhƣ là một cải tiến của phƣơng pháp kiểm chứng đảm bảo giả định nhƣ đã trình bày ở trên. Ý tƣởng chính của phƣơng pháp đề xuất là tìm kiếm giả định tối thiểu trên toàn bộ không gian tìm kiếm của các ứng cử viên giả định (candidate assumptions). Giả định tối thiểu sau khi tạo lập bằng phƣơng pháp đề xuất sẽ đƣợc sử dụng để kiểm chứng lại hệ thống với chi phí thấp hơn. Một số ví dụ minh họa và kết quả thực nghiệm cũng đƣợc trình bày trong luận văn này. Bố cục của luận văn đƣợc trình bày nhƣ sau: Chƣơng 1: Giới thiệu tổng quan phần mềm hƣớng thành phần, các khái niệm cơ bản, cách tiếp cận để kiểm chứng phần mềm hƣớng thành phần. Chƣơng 2: Trình bày chi tiết thuật toán học L*, giải thuật tạo giả định sử dụng thuật toán học L*. Chƣơng 3: Chƣơng này trình bày giải thuật tạo giả định tối thiểu. Trong chƣơng này chúng tôi sẽ đƣa ra một phản ví dụ để minh hoạ rằng: giả định đƣợc tạo ra bởi giải thuật sử dụng thuật toán học L* chƣa phải là giả định tối thiểu. Chúng tôi cũng sẽ trình bày một ví dụ cụ thể để minh hoạ cho thuật toán tạo giả định tối thiểu. Chƣơng 4: Thực nghiệm. Chúng tôi sử dụng bộ công cụ LTSA để xác minh một số hệ thống đơn giản nhằm so sánh về thời gian cũng nhƣ bộ nhớ sử dụng của giải pháp cũ và giải pháp đƣợc đƣa ra trong luận văn. Phần kết luận của luận văn tổng kết các kết quả đã đạt đƣợc, kết luận và đƣa ra một số hƣớng nghiên cứu tiếp theo. 6 CHƢƠNG 1: TỔNG QUAN VỀ KIỂM CHỨNG PHẦN MỀM HƢỚNG THÀNH PHẦN 1.1 Giới thiệu Quá trình phát triển phần mềm hƣớng thành phần đƣợc biết đến là sự phát triển phần mềm bằng cách ghép nối các phần độc lập. Đây là một trong những kỹ thuật quan trọng nhất trong kỹ nghệ phần mềm. Cách tiếp cận này vẫn đang thu hút sự chú ý trong cộng đồng kỹ nghệ phần mềm và đƣợc xem là một cách tiếp cận mở, hiệu quả, giảm thời gian và chi phí phát triển đồng thời tăng chất lƣợng của phần mềm. Đã có rất nhiều khái niệm, kỹ thuật đề xuất nhằm phát triển cho ý tƣởng này. Tuy nhiên, một trong những hạn chế của phát triển phần mềm hƣớng thành phần là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với nhau vì các thành phần có thể đƣợc phát triển một cách độc lập hoặc đƣợc đặt mua từ các công ty thứ 3 (third parties). Hiện tại, các công nghệ hỗ trợ phát triển phần mềm hƣớng thành phần nhƣ CORBA (OMG), COM/DCOM or .NET (Microsoft), Java and JavaBeans (Sun), … vv chỉ hỗ trợ việc ghép nối các thành phần (component plugging). Chúng không có cơ chế kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với nhau hay không. Điều này có nghĩa là cơ chế “plug-and-play” không đƣợc đảm bảo.. Một giải pháp phổ biến hiện nay để giải quyết cho vấn đề trên là áp dụng kiểm chứng mô hình (model checking - MC) [5]. Kiểm chứng mô hình là một cách tiếp cận quan trọng để giải quyết bài toán chứng minh độ tin cậy của phần mềm. Nó cũng tạo ra một không gian trạng thái chi tiết có thể bao phủ đƣợc các hệ thống đang đƣợc kiểm tra đồng thời đạt đƣợc hiệu quả đặc biệt trong quá trình dò các lỗi tổng hợp khá phức tạp mà nguyên nhân chủ yếu do quá trình ghép nối các thành phần gây nên. Tuy nhiên, một trong những hạn chế lớn nhất của kiểm chứng mô hình là “vấn đề bùng nổ không gian trạng thái” khi kiểm chứng các phần mềm có kích thƣớc lớn. Một trong những cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần (modular model checking - MMC) [10, 11]. Thay vì tiến hành kiểm chứng trên toàn bộ hệ thống gồm các thành phần đƣợc ghép nối với nhau, cách tiếp cận này tiến hành kiểm chứng trên từng thành phần riêng biệt. Với cách tiếp cận này, vấn đề bùng nổ không gian trạng thái hứa hẹn sẽ đƣợc giải quyết. Một trong những phƣơng pháp kiểm chứng hỗ trợ ý tƣởng này là phƣơng pháp kiểm chứng đảm bảo giả định (Assume- 7 Guarantee Verification - AGV) [2, 4, 7, 8] . Sử dụng tƣ tƣởng của chiến lƣợc “chia để trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhƣng kích thƣớc nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách riêng biệt. AVG đƣợc đánh giá là một phƣơng pháp hứa hẹn để kiểm chứng phần mềm hƣớng thành phần thông qua phƣơng pháp kiểm chứng mô hình. AVG không những thích hợp cho phần mềm hƣớng thành phần mà còn có khả năng giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình. Trong phƣơng pháp này, các giả định (assumptions) (có vai trò nhƣ là môi trƣờng của các thành phần) sẽ đƣợc tạo lập. Việc tạo lập các giả định chính là bài toán quan trọng nhất trong phƣơng pháp này. Mục tiêu chính của cách tiếp cận này là nhằm kết hợp tốt nhất giữa lợi thế của hai phần: kiểm chứng mô hình và phát triển hƣớng thành phần. Hiện nay, đã có nhiều nghiên cứu về kiểm chứng mô hình từng phần cho phần mềm hƣớng thành phần (modular verification of component based software) [2, 4, 7, 8, 10, 11, 22]. Mỗi khi thêm một thành phần nào đó vào hệ thống, thì toàn bộ hệ thống gồm các thành phần đang tồn tại và thành phần mới phải đƣợc kiểm chứng lại. Vì thế, đối với những phần mềm phức tạp, vấn đề “bùng nổ không gian trạng thái” có thể xảy ra khi ấp dụng các phƣơng pháp trong các nghiên cứu này. Cách tiếp cận trong [2, 4, 7, 8] đề xuất phƣơng pháp kiểm chứng đảm bảo giả định nhƣ đã trình bày ở trên. Xét một hệ thống đơn giản gồm hai phần M1 và M2. Mục đích của cách tiếp cận này là kiểm chứng hệ thống này thoả mãn một thuộc tính p mà không cần đến việc ghép nối giữa các thành phần với nhau. Dựa trên tƣ tƣởng này, AGV tìm ra một giả định A sao cho nó đủ mạnh cho M1 thoả mãn p và đủ yếu để nó đƣợc thỏa mãn bởi M2. Nếu tìm đƣợc một giả định A thỏa mãn các điều kiện trên thì hệ thống khi ghép nối M1||M2 sẽ thoả mãn thuộc tính p. Tuy nhiên, cách tiếp cận này không đề cập đến việc kiếm chứng hệ thống trong ngữ cảnh của tiến hóa thành phần phền mềm. Nếu một thành phần bị tiến hóa sau khi thực hiện một vài thay đổi, khi đó giải pháp này sẽ phải thực hiện kiểm chứng hệ thống nhƣ một hệ thống mới. Trong khi đó việc thay đổi chỉ xảy ra ở một vài thành phần nên việc chạy lại trên toàn bộ hệ thống là không cần thiết. Để giải quyết hạn chế này, giải pháp trong [25] đã đề xuất một cách tiếp nhằm tạo lại giả định nhanh hơn trong ngữ cảnh các thành phần bị tiến hóa (thay đổi). Giả sử tồn tại một thành phần M1 có trƣớc (thành phần này không đƣợc phép thay đổi) và một phần mở rộng M2 (thành phần này đƣợc phép thay đổi). Phần mở rộng M2 đƣợc ghép nối với 8 thành phần M1 bởi một vài cơ chế nào đó. Đầu tiên, chúng ta giả thiết rằng hệ thống chứa M1 và M2 thoả mãn thuộc tính p (tức là, M1||M2╞ p). Tiếp theo, phần M2 đƣợc biến đổi thành một thành phần mới M’2 bằng cách thêm các hành vi (behavior) mới vào thành phần M2. Hệ thống mới chứa M1 và thành phần mới M’2 sẽ phải đƣợc kiểm chứng lại xem liệu nó có tiếp tục thoả mãn thuộc tính p hay không (tức là, M1||M’2╞ p?). Với tƣ tƣởng này, kỹ thuật đƣợc đề xuất chỉ cần kiểm tra liệu M’2 có thỏa mãn giả đinh hiện tại A(p) hay không, trong đó A(p) là một giả định giữa hai thành phần; M1 và M2 sao cho nó đủ mạnh để cho M1 thoả mãn điều kiện p nhƣng đủ yếu để nó đƣợc thỏa mãn bởi M2. Giả định A(p) đƣợc tạo ra bằng việc sử dụng một giải thuật học có tên là L* [1, 24]. Trong kỹ thuật này, các thành phần (M1, M2, và M’2), thuộc tính p, và các giả định đều đƣợc biểu diễn bởi LTS. Nếu M’2 thỏa mãn A(p) thì khi đó hệ thống mới M1||M’2 vẫn thỏa mãn thuộc tính p. Ngƣợc lại, một phản ví dụ để minh chứng cho kết quả này. Trong trƣờng hợp này, phƣơng pháp này sẽ thực hiện phân tích để xác định xem có phải thuộc tính p bị vi phạm trong hệ thống mới hay là giả định A(p) quá mạnh để M’2 thoả mãn. Nếu giả định A(p) là quá mạnh, khi đó một giả định mới Anew(p) sẽ đƣợc tạo lại giữa M1 và thành phần mới M’2. Việc tạo lại giả định này không cần phải chạy lại toàn bộ các phần từ ban đầu, mà sử dụng lại kết quả của quá trình kiểm chứng trƣớc đó (sử dụng lai A(p)) nhằm giảm bớt độ phức tạp cho quá trình tạo lại giả định. Chi tiết của giải thuật tham khảo trong [25]. Cách tiếp cận này là giải pháp tiềm năng cho việc kiểm chứng hệ thống hƣớng thành phần trong ngữ cảnh của tiến hóa phần mềm. Nhƣ chúng ta đã biết, vấn đề quan trọng và cũng hết sức khó khăn của cách tiếp cận đảm bảo giả định là làm sao để xác định đƣợc giả định A. Bên cạnh đó, kích thƣớc của giả định cũng đóng vai trò quyết định đến chi phí cho quá trình kiểm chứng hệ thống hƣớng thành phần. Hiện tại có hai giải pháp đã đƣợc đề xuất để tạo giả định A thoả mãn các yêu cầu của AGR (Assume-Guarantee Reasoning). Giải pháp thứ nhất, nhằm tìm ra giả định yếu nhất Aw (kích thƣớc lớn nhất) [7]. Giải pháp này sẽ gặp khó khăn nếu hệ thống phức tạp với không gian trạng thái quá lớn, quá trình chạy có thể dẫn đến hết không gian bộ nhớ và không thu lại kết quả nhƣ mong muốn. Nhƣ vậy, chúng ta cần phải giảm kích thƣớc của giả định, bên cạnh đó, AGR chỉ có ý nghĩa khi thời gian tính toán của A||M1 << M1||M2. Cách tiếp cần thứ hai [4] tạo ra một giả định có kích thƣớc nhỏ hơn so với cách thứ nhất bằng cách sử dụng thuật toán học có tên là 9 L*. Thuật toán này gồm nhiều bƣớc lặp, bắt đầu từ giả định rỗng để đạt đƣợc giả định thoả mãn yêu cầu của AGR. Tại mỗi bƣớc lặp, thuật toán sẽ sinh ra một ứng cử viên cho giả định. Sau đó, giải thuật sẽ kiểm tra xem ứng cử viên đó có thoả mãn các yêu cầu của AGR hay không? Nếu thoả mãn, thuật toán sẽ dừng và ứng cử viên đó chính là giả định cần tìm. Nếu yêu cầu của AGR không đƣợc thoả mãn, quá trình kiểm tra sẽ đƣa ra một phản ví dụ giúp cho thuật toán sẽ xác định các ứng cử viên tiếp theo tốt hơn. Quá trình trên sẽ đƣợc lặp đi lặp lại cho đến khi tìm đƣợc giả định hoặc chỉ ra một phản ví dụ chứng tỏ hệ thống không thỏa mãn thuộc tính p. Tuy nhiên, giả định (nếu có) đƣợc đƣa ra bởi cách tiếp cận này chƣa phải là giả định tối thiểu, minh chứng cho điều này sẽ đƣợc trình bày chi tiết qua một phản ví dụ trong chƣơng 3. Trong phƣơng pháp này, các giả định (assumptions) (có vai trò nhƣ là môi trƣờng của các thành phần) sẽ đƣợc tạo lập. Việc tạo lập các giả định chính là bài toán quan trọng nhất trong phƣơng pháp này. Kích thƣớc của các giả định này (số lƣợng trạng thái) nên đƣợc cực tiểu hóa bởi vì chi phí cho quá trình kiểm chứng mô hình của phƣơng pháp này phụ thuộc chính vào thông số này. Đây chính là mục tiêu nghiên cứu của luận văn này. 1.2 Các khái niệm cơ bản 1.2.1 Labeled Transition System(LTS) Bộ ứng dụng LTSA sử dụng LTSs [9] để mô hình hoá các đặc tính giao tiếp giữa các thành phần trong một hệ thống. Trong luận văn chúng tôi cũng sử dụng LTS để thể hiện các đặc tính của các thành phần của hệ thống và thuộc tính. Một LTS đƣợc xem nhƣ là một đồ thị định hƣớng với các cạnh đƣợc gán nhãn. Thêm vào đó, tập trạng thái, các phép biến đổi và tập các nhãn đƣợc kết hợp với nhau tạo nên một hệ thống. Đặt Act là tập các hành động có thể kiểm soát đƣợc, và τ là một hành động cục bộ nào đó khó kiểm soát trong môi trƣờng của thành phần. Chúng ta sử dụng π để ký hiệu một trạng thái lỗi cụ thể, để thể hiện sự vi phạm trong hệ thống ghép nối. Một LTS M là mộ bộ bốn Q,  M , , q , trong đó: 0  Q là một tập các trạng thái không rỗng.  αM  Act là tập các hành động có thể kiểm soát được gọi là bảng chữ cái của M. 10  q0  Q là trạng thái ban đầu.    Q   M     Q là hàm chuyển. Chúng ta sử dụng  để ký hiệu cho LTS {p},Act, Æ, p . Một LTS M= Q,  M , , q đƣợc gọi là LTS không đơn định nếu nó có phép biến đổi τ hoặc tồn 0 tại (q, a, q’), (q, a, q’’)  δ trong đó q’ ≠ q’’. Ngƣợc lại M đƣợc gọi là đơn định (deterministic). Giả sử có hai LTS: M  Q,  M , , q 0 và M '  Q' ,  M ' , ' , q0' . Chúng ta nói LTS M biến đổi thành M’ qua hành động a, ký hiệu M a M ' nếu và chỉ nếu (q0, a, q’0)  δ và αM = αM’ và δ = δ’. Hình 2.1 biểu diễn đồ thị cho hai LTS CLIENT và SERVER. a b c Hình 1.1: Ví dụ về LTS 1.2.2 Dẫn xuất(Traces) Một dẫn xuất [2, 4] t của một LTS M là một chuỗi các hành động có thể kiểm soát đƣợc, hay nói một cách khác nó là chuỗi các hành động để thu đƣợc M xuất phát từ một trạng thái ban đầu. Giả sử Σ  Act, ký hiệu t↑Σ ký hiệu một dẫn xuất thu đƣợc bằng cách loại bỏ khỏi t tất cả các hành động a mà a  Σ. Tập tất cả các dẫn xuất của M đƣợc gọi là ngôn ngữ đoán nhận M, ký hiệu L(M). 11 Hình 1.1 đƣa ra biểu diễn đồ hoạ của hai LTS: CLIENT và SERVER. Trạng thái ban đầu của LTS CLIENT trong ví dụ là trạng thái 0, còn của LTS SERVER là trạng thái a. LTS CLIENT thực hiện một yêu cầu cần xử lý khi hành động request xảy ra, khi đó nó sẽ thực hiện yêu cầu LTS SERVER để thực hiện yêu cầu bằng hành động Call. Sau khi yêu cầu đƣợc gửi lên LTS SERVER, server sẽ xử lý và đƣa ra ra kết quả bằng việc sử dụng hành động Service, sau đó thực hiện trả lại kết quả và kết thúc bởi hành động reply. Tại thời điểm này, cả hai LTS cùng trả lại trạng thái ban đầu của nó, và một tiến trình mới lại có thể đƣợc lặp lại. Trong minh hoạ này, , , là các dẫn xuất của LTS SERVER . 1.2.3 Ghép nối song song(Parallel Composition) Ghép nối song song || [9] là thao tác thực hiện hai hành động thay thế và kết hợp trong đó, việc kết hợp các đặc tính của hai thành phần bằng cách đồng bộ hoá các hành động chung tƣơng ứng với bảng chữ cái, và chèn thêm các hành động còn lại. Xét hai LTSs, M1  Q1 ,  M1 , 1 , q01 và M1  Q2 ,  M 2 ,  2 , q02 . Quá trình ghép nối song song giữa M1 và M2, ký hiệu M1 || M2, đƣợc định nghĩa nhƣ sau:  Nếu M1 =  hoặc M2 =  , khi đó M1|| M2 =  .  M1|| M2 là một LTS M  Q,  M , , q0 trong đó, Q = Q1 x Q2, αM = αM1 U αM2, q0  q01  q02 , và phép biến đổi quan hệ δ đƣợc xác định nhƣ sau: i) ii) iii) Ví dụ:    M1   M 2 ,  p,  , p '  1 ,  q,  , q '   2 (( p, q),  , ( p ' , q ' ))     M1 \  M 2 ,  p,  , p '  1 (( p, q),  , ( p ' , q))     M 2 \  M1 ,  q,  , q '   2 (( p, q),  , ( p, q ' ))  (3.1) (3.2) (3.3) 12 Xuất phát từ tập các hành động Tại mỗi hành động, ta sẽ xét xem với hành động đó sẽ biến đổi cặp trạng thái nào thành cặp trạng thái nào: Áp dụng ví dụ trên ta có: Request: do Request  CLIENT nên ta có: ((0,a), request, (1, a)), ((0, b), request, (1,b)), ((0,c), request, (1,c)). Service: do service  SERVER, nên ta có: ((0,b), service , (0,c)),((1,b), service , (1,c)), ((2,b), service , (2,c)). call: do call  Input, và call  Output, nên ta có ((0,a), call ,(1, b)). Kết hợp các hành động và các cặp trạng thái, ta thu đƣợc kết quả nhƣ sau: 13 Hình 1.2: Minh hoạ phép ghép nối song song Bằng việc loại bỏ tất cả các trạng thái không thể tới khi xuất phát từ trạng thái ban đầu (0, a) và tất cả các biến đổi đến các trạng thái này, ta sẽ thu đƣợc kết quả của phép ghép nối song song CLIENT || SERVER: Hình 1.3: Phép ghép nối CLIENT || SERVER. 1.2.3 Safety LTSs, Safety Property, error LTS Một Safety LTS là một LTS hữu hạn không chứa bất kỳ một trạng thái lỗi π nào. Một thuộc tính an toàn(Safety Property) đƣợc xác định nhƣ là một LTS an toàn p trong đó ngôn ngữ L(p) xác định tập tất cả các thuộc tính chấp nhận đƣợc. Một error LTS, ký hiệu perr phát sinh trong quá trình kiểm thử LTS M thoả mãn thuộc tính p. Về 14 cơ bản, error LTS của một thuộc tính p  Q,  p,  , q0 là perr  Q   ,  perr ,  ' , q0 , trong đó αperr = αp và  '     q, a,   | a  p and  q'  Q : (q, a, q' )    . 1.2.4 Sự thoả mãn(satisfying) Cho một LTS M, ta nói M thoả mãn thuộc tính p, ký hiệu M╞ p, nếu và chỉ nếu   L  M  :    p   L( p) . Để kiểm chứng một thành phần M thoả mãn một thuộc tính p, khi đó cả M và perr phải đƣợc biểu diễn dƣới dạng của LTS an toàn(Safety LTS), sau đó thực hiện phép toán ghép nối song song M||perr. Nếu LTS thu đƣợc sau phép ghép nối tồn tại một dẫn xuất có thể tới trạng thái π, khi đó ta nói thành phần M vi phạm thuộc tính p. Ngƣợc lại, M thoả mãn thuộc tính p. 1.2.5 Ôtomat đơn định hữu hạn trạng thái (Deterministic Finite State Automata) Cách tiếp cận trong luận văn này sử dụng thuật toán học L* [1, 24] để tạo giả định từ hai thành phần. Toàn bộ quá trình tạo giả định sẽ đƣợc trình bày trong chƣơng 3. Trong quá trình này, tại bƣớc lặp thứ i, bộ huấn luyện đƣa ra một Deterministic Finite State Automata (DFA) M i là tối thiểu và duy nhất và L(Mi) = L(AW), trong đó AW là giả định yếu nhất khi F thoả mãn thuộc tính p [7]. DFA Mi sau đó sẽ đƣợc biến đổi thành giả định ứng cử viên Ai, trong đó Ai đƣợc thể hiện nhƣ là một LTS an toàn. Deterministic Finite State Automata đƣợc định nghĩa nhƣ sau: Otomat hữu hạn có thể xem nhƣ “máy trừu tƣợng” để đoán nhận ngôn ngữ. Otomat hữu hạn là bộ M = , trong đó:  Q, αM, δ, qo đƣợc định nghĩa nhƣ trong định nghĩa của các LTS hữu hạn.  F  Q là tập các trạng thái kết thúc. Cho một DFA M và một chuỗi σ, ký hiệu δ(q, σ) là trạng thái kết quả sau khi M đọc chuỗi σ bắt đầu tại trạng thái q. Ta nói DFA M đoán nhận chuỗi σ hay chuỗi σ đƣợc đoán nhận bởi Otomat hữu hạn M nếu δ(q0, σ)  F. Tập L(M) = {σ | δ(q0, σ)  F} đƣợc gọi là ngôn ngữ đƣợc đoán nhận bởi Otomat M. Cho một DFA M, chúng ta cũng dễ dàng thu đƣợc một LTS an toàn A từ M bằng cách loại bỏ tất cả các trạng thái không phải là trạng thái kết thúc và các biến đổi liên quan đến trạng thái này bên trong M. Hình 1.4 mô tả một ví dụ để biến đổi một DFA thành một LTS an toàn: