Khóa luận Nghiên cứu về kiểm chứng phần mềm sử dụng công cụ spin

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Trần Thị Vân Dung NGHIÊN CỨU VỀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG CÔNG CỤ SPIN KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công Nghệ Thông Tin HÀ NỘI - 2010 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Trần Thị Vân Dung NGHIÊN CỨU VỀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG CÔNG CỤ SPIN KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công Nghệ Thông Tin Cán bộ hướng dẫn: PGS. TS. Nguyễn Việt Hà Cán bộ đồng hướng dẫn: TS. Phạm Ngọc Hùng HÀ NỘI - 2010 Lời cảm ơn Lời đầu tiên, em xin đƣợc bày tỏ lòng biết ơn sâu sắc tới thầy TS. Nguyễn Việt Hà và thầy TS. Phạm Ngọc Hùng đã tận tình giúp đỡ em làm và hoàn thiện khóa luận trong suốt năm học vừa qua. Em xin đƣợc bày tỏ lòng biết ơn tới các thầy, cô trong khoa Công Nghệ Thông Tin, trƣờng Đại Học Công Nghệ, ĐHQGHN. Các thầy cô đã nhiệt tình dạy bảo và tạo mọi điều kiện học tập tốt nhất cho chúng em trong những năm học tập tại ĐHCN, đặc biệt là trong thời gian thực hiện khóa luận tốt nghiệp. Tôi xin cảm ơn các bạn sinh viên lớp K51CC và K51CNPM Trƣờng Đại học Công nghệ, những ngƣời bạn đã cùng tôi học tập và rèn luyện trong suốt những năm học đại học. Cuối cùng con xin gửi tới Bố Mẹ và gia đình tình thƣơng yêu và lòng biết ơn. Bố Mẹ đã nuôi dƣỡng và luôn là chỗ dựa tinh thần cho con. Hà Nội, ngày 18 tháng 5 năm 2010 Trần Thị Vân Dung 1 Tóm tắt nội dung Kiểm chứng mô hình (model checking) là một phƣơng pháp hình thức dùng cho việc kiểm chứng hệ thống. Kiểm chứng mô hình khảo sát tất cả các trạng thái có thể của hệ thống và kiểm tra rằng chúng chứa sự đúng đắn đã đƣợc đặc tả. Việc sinh ra các trạng thái và kiểm tra có thể đƣợc thực hiện một cách tự động bằng phần mềm và Spin là một trong những bộ kiểm chứng (model checker) đƣợc sử dụng rộng rãi. Các bộ kiểm chứng không kiểm tra trực tiếp chƣơng trình mà kiểm tra một mô hình là thể hiện mức cao của hệ thống. Mô hình này mô tả hành vi của hệ thống. Để áp dụng đƣợc các công cụ kiểm chứng mô hình, việc đầu tiên là phải xây dựng mô hình của hệ thống. Các mô hình này cùng với đặc tả của thuộc tính cần kiểm tra là đầu vào của các bộ kiểm chứng. Khóa luận nghiên cứu việc kiểm chứng phần mềm sử dụng Spin, cụ thể là việc kiểm chứng mô hình máy hữu hạn trạng thái, sau đó đƣa ra một công cụ chuyển một mô tả ban đầu của hệ thống ở dạng máy hữu hạn trạng thái (chứa trong 1 tệp .txt) thành mô hình và kiểm chứng bằng Spin. MỤC LỤC 2 Mục Lục 1 Mở đầu 1.1. Đặt vấn đề ....................................................................................................... 6 1.2. Mục tiêu và phạm vi của đề tài ........................................................................ 7 1.3. Cấu trúc khóa luận .......................................................................................... 7 2 Sơ lược về Model Checking 2.1. Kiểm chứng hệ thống ...................................................................................... 8 2.2. Model Checking.............................................................................................. 9 2.2.1. Phƣơng pháp hình thức và Model Checking............................................ 9 2.2.2. Hoạt động của Model Checking .............................................................. 9 2.2.3. Ƣu nhƣợc điểm của Model Checking .................................................... ..10 3 Ngôn ngữ Promela 3.1. Kiểu dữ liệu và toán tử cơ bản ...................................................................... ..13 3.1.1. Kiểu dữ liệu cơ bản ............................................................................... ..13 3.1.2. Toán tử cơ bản ....................................................................................... ..13 3.2. Dữ liệu kiểu kênh trong Promela ................................................................... ..14 3.2.1.Cú pháp ............................................................................................... ..14 3.2.2. Kênh gặp (rendezvous channel) ......................................................... ..15 3.3. Các cú pháp .................................................................................................. ..15 3.3.1. Lệnh printf() ................................................................................ ..15 3.3.2. Lệnh lựa chọn if ............................................................................... ..15 3.3.3. Lệnh lặp do ....................................................................................... ..16 3.3.4. Lệnh nhảy goto .............................................................................. ..16 MỤC LỤC 3 3.3.5. Lệnh define ..................................................................................... ..16 3.4. run và atomic ............................................................................................ ..17 3.4.1. run và tiến trình init() ................................................................. ..17 3.4.2. atomic ............................................................................................. ..17 4 Kiểm chứng chương trình trong Spin 4.1. Kiểm chứng chƣơng trình trong Spin ............................................................ ..20 4.1.1. Giả lập ngẫu nhiên .............................................................................. ..20 4.1.2. Verify ................................................................................................ ..22 4.2. Logic thời gian tuyến tính (LTL)................................................................... ..24 4.2.1. Cú pháp.............................................................................................. ..25 4.2.2. Biểu diễn tính chất bất biến của hệ thống bằng LTL ........................... ..26 4.3. Cấu trúc Never Claim ................................................................................. ..26 5 Thực nghiệm 5.1.Mô hình máy hữu hạn trạng thái ..................................................................... ..28 5.1.1.Mô hình máy hữu hạn trạng thái .......................................................... ..28 5.1.2.Ví dụ về mô hình máy hữu hạn trạng thái ............................................. ..28 5.2.Thực nghiệm ................................................................................................... ..31 5.2.1.Áp dụng kiểm chứng mô hình hệ thống đèn ......................................... ..32 5.2.2.Áp dụng kiểm chứng mô hình không đáp ứng thuộc tính ..................... ..33 6 Kết luận 6.1. Kết quả của khóa luận ................................................................................... ..36 6.2. Hƣớng nghiên cứu tiếp theo .......................................................................... ..36 Phụ lục Phụ lục A: Tệp lampcode.txt ................................................................................. 37 MỤC LỤC 4 Phụ lục B: Tệp lampcode.pml khi chạy verify trong Spin ................................. ..38 Phụ lục C: Tệp lamp2code.txt ............................................................................... ..40 Phụ lục D: Tệp lamp2code.pml khi chạy verify trong Spin ................................... ..41 Phụ lục E: Mã nguồn của chƣơng trình ................................................................. ..43 Tài liệu tham khảo.................................................................................................... ..47 5 Danh sách hình vẽ 2.1 Sơ đồ việc kiểm chứng hệ thống ............................................................................... 8 2.2. Sơ đồ hoạt động của phƣơng pháp model checking ................................................ ..10 5.1. Mô hình máy hữu hạn trạng thái mô tả hoạt động của đèn ...................................... ..29 5.2. Kết quả khi chạy giả lập mô hình hệ thống đèn ở hình 5.1 ..................................... ..31 5.3. Kết quả kiểm chứng mô hình 5.1 của hệ thống đèn ................................................ ..33 5.4. Mô hình sai của hệ thống đèn ................................................................................. ..34 5.5. Kết quả kiểm chứng mô hình 5.4 của hệ thống đèn ................................................ ..35 CHƢƠNG 1: MỞ ĐẦU 6 Chương 1 Mở đầu 1.1.Đặt vấn đề Hiện nay chúng ta ngày càng phụ thuộc vào các hệ thống máy tính và phần mềm chuyên dụng hỗ trợ mọi mặt trong sản xuất và đời sống hằng ngày. Bất kỳ một lập trình viên nào đều hiểu một điều rằng chƣơng trình hầu nhƣ không thể chạy từ lần biên dịch đầu tiên và chƣa thể hoàn hảo ngay từ lần biên dịch thành công đầu tiên. Chƣơng trình trông có vẻ đúng luôn có thể tiềm ẩn lỗi ở đâu đó. Các phần mềm đƣợc phát triển trong 1 quy trình chuyên nghiệp luôn có thể chứa lỗi mà chỉ đƣợc phát hiện sau khi đã đƣợc phân phối và đƣa vào sử dụng. Trong thiết kế phần cứng và phần mềm, nỗ lực và thời gian của chúng ta tiêu tốn rất nhiều vào việc kiểm chứng và đôi khi nhiều hơn cả thời gian và nỗ lực dành cho việc xây dựng. Bên cạnh đó có những trƣờng hợp chúng ta không thể chấp nhận những ứng dụng có thể có lỗi dù là nhỏ nhất, đó là những ứng dụng mà sự trục trặc có thể dẫn đến tử vong, tổn thất nặng nề hay ảnh hƣởng đến môi trƣờng sống. Kỹ nghệ phần mềm dành cho các hệ thống này là vô cùng khó khăn. Cách giải quyết luôn là phân tích, lập trình cẩn thận, kiểm tra lại, kiểm thử. Bên cạnh đó, chúng ta luôn tìm kiếm các công nghệ và kĩ thuật giúp cho việc kiểm chứng các phần mềm trở nên nhẹ nhàng hơn trong khi tăng sự bao quát và chính xác của nó [1]. Công cụ Spin chạy kỹ thuật model checking nhận mô hình của hệ thống và khảo sát tất cả các trạng thái có thể của hệ thống theo kiểu vét cạn. Công việc chủ yếu là phát triển một mô hình đủ chi tiết để biểu diễn hệ thống một cách chính xác nhƣng cũng đủ đơn giản để Spin có thể chạy việc kiểm tra (với giới hạn về tài nguyên và bộ nhớ). Vấn đề đặt ra là xây dựng công cụ tự động chuyển 1 mô tả các hành vi, tính chất của hệ thống thành đoạn mã biểu diễn mô hình mà Spin có thể chạy. Do vậy, giảm nhẹ công sức giành cho việc kiểm chứng. CHƢƠNG 1: MỞ ĐẦU 7 1.2.Mục tiêu và phạm vi của đề tài Đề tài nghiên cứu việc kiểm chứng hệ thống sử dụng Spin, các mô hình hệ thống dành cho Spin đƣợc viết bằng ngôn ngữ Promela. Công cụ đƣợc xây dựng với mong muốn có thể tự động sinh mã Promela chính xác và đầy đủ phục vụ cho việc kiểm chứng trong Spin. Công cụ đƣợc xây dựng đã tự động sinh mô hình Promela cho những hệ thống đã đƣợc biểu diễn ở mô hình máy hữu hạn trạng thái. 1.3.Cấu trúc khóa luận Chƣơng 2 trình bày về Model checking, là kỹ thuật kiểm chứng mà đề tài nghiên cứu, những nguyên tắc hoạt động của Model checking. Chƣơng 3 trình bày về các cấu trúc của ngôn ngữ Promela, là ngôn ngữ để viết các mô hình cho Spin. Chƣơng 4 bắt đầu đi vào giai đoạn kiểm chứng một mô hình trong Spin Chƣơng 5 Trình bày kết quả thực nghiệm của khóa luận dựa trên các khái niệm đã nêu trong chƣơng 2 và 3 Chƣơng 6 tổng kết lại quá trình nghiên cứu, đƣa ra kết quả đạt đƣợc và hƣớng nghiên cứu tiếp theo. CHƢƠNG 2: SƠ LƢỢC VỀ MODEL CHECKING 8 Chương 2 Sơ Lược Về Model Checking Chƣơng này giới thiệu về kiểm chứng hệ thống, những lợi thế của kiểm chứng hệ thống. Sau đó là khái niệm về model checking, những ƣu nhƣợc điểm của phƣơng pháp model checking. 2.1.Kiểm chứng hệ thống Trong giai đoạn kiểm thử khi kỹ nghệ phần mềm, phần mềm đƣợc chạy trên một số hữu hạn những bộ dữ liệu đầu vào đã đƣợc thiết kế sẵn, phần mềm chạy đúng hay sai dựa trên việc so sánh dữ liệu đầu ra thực tế với đầu ra mong muốn. Việc chạy hết các trƣờng hợp có thể của dữ liệu đầu vào là không thể, do vậy kiểm thử không đảm bảo chắc chắn rằng phần mềm không chứa lỗi [1]. Bên cạnh đó, lỗi đƣợc phát hiện trong giai đoạn này là muộn và dẫn đến tiêu tốn nhiều nỗ lực khắc phục lỗi. Hình 2.1.Sơ đồ việc kiểm chứng hệ thống [1] CHƢƠNG 2: SƠ LƢỢC VỀ MODEL CHECKING 9 Kiểm chứng hệ thống thực hiện việc xác minh một thiết kế hay một sản phẩm phần mềm đảm bảo những tính chất cụ thể mà thƣờng đã đƣợc nêu ra trong đặc tả của hệ thống [2]. Đặc tả hệ thống trở thành cơ sở của mọi hoạt động kiểm chứng. Một thiếu sót đƣợc phát hiện khi hệ thống không thỏa mãn một trong các tính chất đã đƣợc đặc tả, hệ thống đƣợc chứng minh là đúng khi nó thỏa mãn tất cả các tính chất đƣợc nêu trong đặc tả hệ thống. Từ đó, kiểm chứng có khả năng phát hiện lỗi sớm [1]. 2.2.Model checking 2.2.1.Phương pháp hình thức và model checking Phƣơng pháp hình thức đƣợc xem nhƣ là toán học đƣợc áp dụng vào mô hình hóa và phân tích hệ thống [1]. Từ những nghiên cứu về phƣơng pháp hình thức, chúng ta đã có đƣợc những kỹ thuật kiểm chứng dựa trên mô hình, trong đó có model checking, đi kèm với chúng là các phần mềm để tự động hóa nhiều bƣớc kiểm chứng khác nhau. Cơ sở của kiểm chứng dựa trên mô hình là mô tả các hành vi của hệ thống theo một cách không nhập nhằng, điều này giúp phát hiện ra những điểm nhập nhằng, mâu thuẫn và chƣa hoàn thiện trong những đặc tả không hình thức của hệ thống [1]. Kỹ thuật này giúp tích hợp kiểm chứng vào quá trình thiết kế, nó trở thành công cụ để kỹ nghệ những phần mềm buộc phải hoạt động không có sai sót [2]. 2.2.2.Hoạt động của model checking Từ đặc tả của hệ thống, ta xây dựng một mô hình hệ thống thể hiện các hành vi của hệ thống, mô hình này có thể đƣợc viết bằng ngôn ngữ C, các ngôn ngữ tƣơng tự C hay Java. Cùng với đó ta biểu diễn các tính chất (cần kiểm chứng) của hệ thống dƣới dạng các biểu thức hình thức. CHƢƠNG 2: SƠ LƢỢC VỀ MODEL CHECKING 10 Hình 2.2.Sơ đồ hoạt động của phƣơng pháp model checking [1] Sau đó công cụ chạy model checking (bộ kiểm chứng) đƣợc dùng để sinh ra tất cả các trạng thái của hệ thống và kiểm tra chúng thỏa mãn các tính chất đó hay không, nếu không, model checking sẽ tìm đƣợc một phản ví dụ - một trạng thái của hệ thống không thỏa mãn – và chỉ ra tính toán dẫn đến trạng thái đó. Sử dụng phản ví dụ này cùng với việc chạy giả lập mô hình trong model checker, ta có thể tìm ra lỗi trong mô hình (có thể là sự không nhất quán, không rõ nghĩa trong đặc tả hệ thống) và sửa lỗi. 2.2.3.Ưu nhược điểm của model checking Model checking mang một số ƣu điểm nhƣ sau [1]  Là một phƣơng pháp kiểm chứng tổng quát áp dụng đƣợc cho một phạm vi lớn các ứng dụng: hệ thống nhúng, kỹ nghệ phần mềm, thiết kế phần cứng…  Hỗ trợ kiểm chứng cụ bộ, các tính chất có thể đƣợc kiểm tra một cách riêng lẻ từ đó có thể tập chung kiểm chứng một tính chất quan trọng trƣớc mà không cần tới một đặc tả hệ thống hoàn chỉnh.  Cung cấp các thông tin ý nghĩa cho việc gỡ lỗi khi phát hiện đƣợc môt tính chất không đƣợc thỏa mãn. CHƢƠNG 2: SƠ LƢỢC VỀ MODEL CHECKING 11  Model cheking đang càng ngày trở nên phổ biến hơn và đƣợc ƣa chuộng, đã xuất hiện thêm nhiều model checker.  Có thể đƣợc tích hợp một cách dễ dàng vào nhứng quy trình phát triển phần mềm hiện tại.  Model checking có nền tảng đúng đắn của toán học, nó dựa trên lý thuyết về thuật toán đồ thị, cấu trúc dữ liệu, và logic. Bên cạnh đó phƣơng pháp model checking cũng chứa những nhƣợc điểm [1]  Chủ yếu phù hợp với các ứng dụng tập trung vào điều khiển là chủ yếu, không phù hợp với các ứng dụng hƣớng dữ liệu do khối lƣợng dữ liệu thƣờng tăng vô tận.  Model checking kiểm chứng mô hình của hệ thống, không phải bản thân hệ thống, mọi kết quả đạt đƣợc đều chỉ về mô hình của hệ thống, do vậy cần đến những kỹ thuật khác bổ trợ nhƣ kiểm thử để tìm ra những lỗi chế tạo (đối với phần cứng) và lỗi lập trình (đối với phần mềm).  Model checking chỉ kiểm tra những tính chất đƣợc đặc tả, ta không thể biết đƣợc thông tin về các tính chất không đƣợc model checking kiểm chứng.  Việc sử dụng model checking đòi hỏi kinh nghiệm trừu tƣợng hóa hệ thống để cho ra một mô hình hệ thống và thể hiện các tính chất của hệ thống theo logic hình thức. CHƢƠNG 3: NGÔN NGỮ PROMELA 12 Chương 3 Ngôn Ngữ Promela Với Spin, ngôn ngữ Promela đƣợc sử dụng để xây dựng mô hình của hệ thống và các tính chất của nó, chƣơng này trình bày các thành phần và câu lệnh cơ bản của Promela đƣợc sử dụng trong khóa luận. Promela là ngôn ngữ không tất định, là một trong các ngôn ngữ có cú pháp và ngữ nghĩa tƣơng tự ngôn ngữ C [6]. Một chƣơng trình Promela bao gồm một hay nhiều tiến trình, mỗi tiến trình chứa một chuỗi các câu lệnh. Các tiến trình có thể có tham số hoặc không.Các tiến trình đƣợc khai báo với từ khóa active sẽ đƣợc khởi tạo và gán một giá trị pid (process id) duy nhất. active proctype P( ) { // tiến trình P không có tham số lenh_1; … lenh_n } Tiến trình khai báo mà không có từ khóa active sẽ không đƣợc pid và đó đó chƣa thể chạy. proctype P( ) { // tiến trình P không có tham số lenh_1; … lenh_n } CHƢƠNG 3: NGÔN NGỮ PROMELA 13 Tính không tất định của Promela thể hiện ở chỗ khi Spin chạy chƣơng trình, các tiến trình đƣợc chọn bất kỳ để thực thi, do vậy các lệnh trong các tiến trình đƣợc thực thi xen kẽ một cách ngẫu nhiên. Mỗi tiến trình có riêng một biến lƣu vị trí của câu lệnh sẽ đƣợc thực thi khi đến lƣợt nó chạy. 3.1.Kiểu dữ liệu và toán tử cơ bản 3.1.1.Kiểu dữ liệu cơ bản Bảng 3.1 nêu các kiểu dữ liệu cơ bản trong Promela Bảng 3.1.Kiểu dữ liệu cơ bản trong Promela Tên kiểu Kích thƣớc (bits) Dữ liệu bit, bool 1 0, 1, false, true byte 8 0…255 short 16 -32768…32767 int 32 -2 31 …2 31 -1 unsigned ≤32 0…2 n -1 Promela không có kiểu số thực, kiểu kí tự và kiểu xâu. Promela định nghĩa kiểu mtype mtype = { name_1, name_2,…name_n}; 3.1.2.Toán tử cơ bản Các toán tử trong promela tƣơng tự với các toán tử trong ngôn ngữ C CHƢƠNG 3: NGÔN NGỮ PROMELA 14 Bảng 3.2.Các toán tử cơ bản trong Promela xếp theo thứ tự độ ƣu tiên giảm dần Ký hiệu Tên = toán tử gán || (toán tử logic) hoặc && (toán tử logic) và = =, != (toán tử so sánh) bằng, khác ,>= các toán tử so sánh ++, - - tăng, giảm ! (toán tử logic) phủ định ( ) đóng mở ngoặc 3.2.Dữ liệu kiểu kênh trong Promela 3.2.1.Cú pháp Kiểu kênh trong Promela đi kèm với hai toán tử gửi: ! và nhận: ?, đƣợc khai báo với một kiểu dữ liệu (kiểu của thông điệp) mà nó có thể nhận và gửi [2]. Khai báo: chan ch = [ dung_luong ] of { kieu_du_lieu_1,...,kieu_du_lieu_n } ; Có 2 kiểu kênh trong Promela o Kênh gặp : đƣợc khai báo với dung lƣợng bằng 0. o Kênh đệm : đƣợc khai báo với dung lƣợng lớn hơn 0. Lệnh truyền dữ liệu trên kênh  Gửi : CHƢƠNG 3: NGÔN NGỮ PROMELA 15 ten_bien_kenh ! bieu_thuc_1, ..., bieu_thuc_n  Nhận : ten_bien_kenh ? bien_1, ..., bien_n  Giá trị của các biểu thức có kiểu tƣơng ứng với kiểu khi kênh đƣợc khai báo. Các biểu thức trong lệnh gửi sẽ đƣợc tính toán và giá trị thu đƣợc sẽ trở thành thông điệp truyền trên kênh, lệnh nhận đƣợc thực thi sau lệnh đó sẽ gán các giá trị này cho các biến của nó. Một lệnh nhận chỉ đƣợc thực khi tồn tại thông điệp đƣợc gửi lên kênh. 3.2.2.Kênh gặp Kênh gặp (đƣợc khai báo với dung lƣợng bằng 0) biểu thị rằng nơi gửi (tiến trình chứa lệnh gửi) và nơi nhận thông điệp (tiến trình chứa câu lệnh nhận) truyền dữ liệu một cách đồng bộ. Khi đó, tiến trình chứa lệnh gửi sẽ bị chặn cho đến khi lệnh nhận trong tiến trình nhận đƣợc thực thi [2]. Nếu trong một tiến trình có một lệnh gửi (hay nhận) đƣợc khởi tạo mà không có lệnh nhận (hay gửi) nào tƣơng ứng (về của kiểu thông điệp) thì tiến trình đó sẽ bị khóa [2]. 3.3.Các cú pháp 3.3.1.Lệnh printf( ) Câu lệnh prinf printf (“xau_ki_tu”, cac_bien) ; trong xâu kí tự có thể chứa các định dạng in tƣơng ứng với các biến nhƣ %d 3.3.2.Lệnh lựa chọn if if ::bieu_thuc_logic_1 → lenh_11; lenh_12;…lenh_1n ::bieu_thuc_logic_2 → lenh_21; lenh_22;…lenh_2n ... CHƢƠNG 3: NGÔN NGỮ PROMELA 16 ::bieu_thuc_logic_n → lenh_n1; lenh_n2;…lenh_nn fi; Ngoài ra, biểu thức logic có thể là else hoặc true. Chuỗi lệnh theo sau else sẽ đƣợc thực thi nếu các biểu thức logic còn lại đều nhận giá trị false. Chuỗi lệnh theo sau true luôn luôn đƣợc chọn để thực thi. Chuỗi lệnh theo sau biểu thức logic có thể trống, khi gặp chuỗi lệnh trống, chƣơng trình bỏ qua chuyển sang câu lệnh sau câu lệnh if. skip có ý nghĩa tƣơng đƣơng với một chuỗi lệnh trống. 3.3.3.Lệnh lặp do do ::bieu_thuc_logic_1 → lenh_11; lenh_12;…lenh_1n ::bieu_thuc_logic_2 → lenh_21; lenh_22;…lenh_2n .... ::bieu_thuc_logic_n → lenh_n1; lenh_n2;…lenh_nn ::bieu_thuc_logic → break od; Câu lệnh if và do thể hiện tính không tất định của Promela: nếu hai hay nhiều biểu thức logic có giá trị true, chuỗi lệnh theo sau một biểu thức bất kỳ trong số đó sẽ đƣợc thực thi. 3.3.4.Lệnh nhảy goto Giúp nhảy đến 1 đoạn chƣơng trình sau một nhãn với tên nhãn đặt trƣớc dấu hai chấm. goto: ten_nhan; 3.3.5.Lệnh define define là lệnh macro dùng để định nghĩa ký hiệu cho một biểu thức và đƣợc đặt ở đầu chƣơng trình CHƢƠNG 3: NGÔN NGỮ PROMELA 17 #define length 10 3.4. run và atomic 3.4.1.run và tiến trình init() run là một cách khác để khởi tạo một tiến trình. Trƣớc đó một tiến trình đƣợc khai báo mà không có từ khóa active proctype P(){ … } run P (); Với việc sử dụng run ta có thể khai báo tất cả các tiến trình có trong chƣơng trình sau đó “run” (khởi tạo) chúng trong một tiến trình có tên init(). Tiến trình init() luôn là tiến trình đầu tiên đƣợc khởi tạo và do vậy luôn có pid bằng 0. proctype P(){ … } proctype Q(){ … } init { run P(); run Q(); } 3.4.2. atomic  Chuỗi lệnh đặt trong atomic {} sẽ đƣợc thực hiện nhƣ một câu lệnh độc lập và không bị chen vào bởi một lệnh nào khác ngoài nó. Do vậy, sử dụng atomic giúp giảm sự phức tạp của mô hình cần kiểm chứng. CHƢƠNG 3: NGÔN NGỮ PROMELA 18 Ví dụ 3.1. Chuỗi lệnh dùng atomic atomic { temp = n; n = temp+1 } Đoạn mã trong ví dụ 3.1. tƣơng đƣơng với lệnh n=n+1;  Ta có thể sử dụng atomic để kết hợp các câu lệnh giữa các tiến trình chan ch = [0] of {int}; active proctype P(){ atomic {A;ch!1;B}} active proctype Q(){ atomic {ch?1 -> C} Trong ví dụ trên, sau khi khối lệnh A trong tiến trình P đƣợc thực thi, dữ liệu kiểu int với giá trị 1 đƣợc gửi lên kênh ch kiểu gặp (câu lệnh ch!1; đƣợc thực hiện), tiến trình Q nhận dữ liệu trên kênh (bởi ch?1) và khối lệnh C đƣợc thực thi, khi khối lệnh C kết thúc, việc thực thi sẽ tự động chuyển về tiến trình P và thực thi khối lệnh B.  atomic có thể đƣợc sử dụng để khởi tạo một số các tiến trình và đảm bảo rằng không một tiến trình nào bắt đầu chạy cho tới khi tất cả các tiến trình đƣợc khởi tạo hết. Trong ví dụ về khởi tạo hai tiến trình P, Q ở 3.4.1, do tiến trình init đã đƣợc khởi tạo và có thể chạy, một trong hai tiến trình P, Q có thể đƣợc chạy trƣớc khi tiến trình còn lại đƣợc khởi tạo, điều đó không có lợi cho chúng ta. Bổ sung atomic sẽ loại bỏ đƣợc điều này: proctype P(){ … } proctype Q(){ CHƢƠNG 3: NGÔN NGỮ PROMELA 19 … } init { atomic { run P(); run Q(); } } CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 20 Chương 4 Kiểm Chứng Chương Trình Với Spin Chƣơng này trình bày về thêm một số khái niệm trong Promela để mô hình hóa đƣợc một hệ thống thực tế, cách chạy môt chƣơng trình Promela trong Spin tại các chế độ khác nhau, giới thiệu về logic thời gian tuyến tính (LTL) là ngôn ngữ biểu diễn tính chất mong muốn (hay tính chất cần kiểm chứng) của hệ thống. 4.1.Kiểm chứng chương trình trong Spin 4.1.1.Giả lập ngẫu nhiên Trong chế độ giả lập, Spin biên dịch và chạy một chƣơng trình promela, sau đó in ra các trạng thái của chƣơng trình. Khóa luận sử dụng công cụ jSpin cho ta giao diện đồ họa của Spin và xem xét kết quả kiểm chứng một cách trực quan. Một trạng thái của chƣơng trình là một bộ các giá trị gồm của các biến, các giá trị của biến đếm vị trí của các tiến trình. Một tính toán của chƣơng trình là chuỗi các trạng thái bắt đầu bởi trạng thái khởi tạo và tiếp tục với những trạng thái xuất hiện khi mỗi câu lệnh đƣợc thực hiện [3]. Trong ví dụ 4.1 biến n đƣợc khởi tạo với giá trị 0, chƣơng trình bao gồm 2 tiến trình: P và Q tƣơng ứng gán biến n giá trị 1 hoặc 2 và in ra giá trị của n cùng tên tiến trình Ví dụ 4.1.Chƣơng trình với 2 tiến trình 1 byte n=0; 2 active proctype P(){ 3 n=1; 4 printf("Process P, n=%d\n",n); 5 } 6 active proctype Q(){ CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 21 7 n=2; 8 printf("Process Q, n=%d\n",n); 9 } Trong jSpin ta chạy Random, chƣơng trình không có lỗi và nhận đƣợc kết quả: Starting P with pid 0 0: proc - (:root:) creates proc 0 (P) Starting Q with pid 1 0: proc - (:root:) creates proc 1 (Q) 1 Q 7 n = 2 Process Statement n 0 P 3 n = 1 2 Process P, n=1 0 P 4 printf('Proces 1 Process Q, n=1 1 Q 8 printf('Proces 1 4: proc 1 (Q) terminates 4: proc 0 (P) terminates 2 processes created Trong ví dụ 4.1, đầu tiên P và Q lần lƣợt đƣợc tạo với pid (process id) là 0 và 1. Các lệnh trong cả hai tiến trình đƣợc thực thi xen kẽ một cách tùy ý jSpin hiển thị trạng thái của chƣơng trình sau mỗi câu lệnh đƣợc thực thi (theo thứ tự: pid, tên tiên trình chứa câu lệnh, vị trí câu lệnh, nội dung câu lệnh đã đƣợc cắt ngắn, giá trị của biến). Trong lần chạy ở trên các câu lệnh đƣợc thực hiện theo thứ tự: n=2 n=1 prinf(Q) CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 22 prinf(P) Do vậy hai hàm printf đều in ra n=1 4.1.2. Verify Assertion là cách đơn giản để kiểm tra chƣơng trình. Một assertion là một mệnh đề đƣợc đặt trong 1 chƣơng trình mà ta cho rằng mệnh đề sẽ luôn đúng tại vị trí đó. Spin sẽ tính toán các assertion trong quá trình tìm kiếm phản ví dụ trong không gian trạng thái của chƣơng trình. Ví dụ 4.2 tìm số lớn nhất trong 2 số a và b, trong câu lệnh if, nếu a >=b biến max sẽ đƣợc gán giá trị a, nếu b>=a biến max sẽ đƣợc gán giá trị b, ở cuối chƣơng trình ta kiểm tra lại bởi biểu thức logic (a >= b -> max = = a : max = = b) Ví dụ 4.2. Tìm số lớn nhất trong 2 số active proctype P() { int a = 5, b = 5; int max; if :: a >= b -> max = a :: b >= a -> max = b fi; assert (a >= b -> max == a : max == b) } Trong jSpin ta chạy Verify, kết quả là không có lỗi vi phạm nào đƣợc thông báo từ chƣơng trình. (Spin Version 4.3.0 -- 22 June 2007) + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 23 cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 24 byte, depth reached 2, ••• errors: 0 ••• 3 states, stored 1 states, matched 4 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 2.302 memory usage (Mbyte) unreached in proctype P (0 of 8 states) Trong ví dụ 4.3, ta cũng tìm số lớn nhất trong 2 số a, b nhƣng khi b>=a, biến max lại đƣợc gán giá trị b+1, do vậy biểu thức (a >= b -> max = = a : max = = b) không đƣợc thỏa mãn. Ví dụ 4.3. Chƣơng trình có chứa lỗi active proctype P() { int a = 5, b = 6; int max; if :: a >= b -> max = a :: b >= a -> max = b+1 fi; assert (a >= b -> max == a : max == b) } Khi chạy Verify, jSpin sẽ đƣa ra thông báo assertion bị vi phạm. CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 24 pan: assertion violated ( ((a>=b)) ? ((max==a)) : ((max==b)) ) (at depth 0) pan: wrote max.pml.trail (Spin Version 4.3.0 -- 22 June 2007) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 24 byte, depth reached 2, ••• errors: 1 ••• 3 states, stored 0 states, matched 3 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 2.302 memory usage (Mbyte) 4.2.Logic thời gian tuyến tính (LTL) Spin sẽ tính toán assertion tại một vị trí nhất định trong chƣơng trình mà ở đó assertion đƣợc thêm vào, do vậy assertion có hạn chế trong việc biểu diễn tính chất của mô hình. Ta cần dùng đến logic thời gian tuyến tính (LTL), LTL mạnh mẽ hơn trong việc biểu diễn tính chất của mô hình (hệ thống). Với LTL ta có thể diễn tả những tính chất chung cần đƣợc thỏa mãn mà không liên quan đến một vị trí nào trong chƣơng trình. LTL đặc biệt phù hợp với các hệ thống tƣơng tác khi tính đúng đắn của hệ thống không chỉ thể hiện ở kết quả tính toán mà ta phải kiểm tra sự giao tiếp và thực thi các tiến trình trong hệ thống [1]. CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 25 4.2.1.Cú pháp Bảng 4.1 mô tả các toán tử của LTL Bảng 1.4.Các toán tử của LTL Toán tử Ký hiệu phủ định ! và && hoặc | | phụ thuộc → tƣơng đƣơng ↔ LTL hình thức hóa các tính chất về thời gian bởi các toán tử thời gian. Bảng 4.2.Các toán tử thời gian của LTL Toán tử Ký hiệu luôn luôn [ ] tồn tại cho đến khi U Thời gian trong LTL là thời gian “trừu tƣợng” do LTL quan niệm thời gian một cách rời rạc, chỉ bao bao gồm những thời điểm đơn lẻ [1]. [ ] A: hệ thống luôn luôn mang tính chất A CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 26 A: nếu hệ thống có tính chất A tại một thời điểm nào đó trong tƣơng lai thì ta nói hiện tại hệ thống có tính chất A A U B: tại thời điểm hiện tại hệ thống có tính chất A U B có nghĩa là: nếu trong một thời điểm nào đó trong tƣơng lai hệ thống có tính chất B thì hệ thống có tính chất A tại tất cả các thời điểm từ hiện tại cho tới khi nó mang tính chất B. 4.2.2.Biểu diễn tính chất bất biến của hệ thống bằng LTL Trong nhiều trƣờng hợp, hệ thống xây dựng phải thỏa mãn một tính chất bất biến nào đó. Với LTL ta biểu diễn tính chất đó bởi toán tử [] Ví dụ 4.4: Tính chất “mỗi yêu cầu (request) cuối cùng đều dẫn tới một phản hồi (response)” ta biểu diễn nhƣ sau [ ] ( request → response) 4.3.Cấu trúc Never claim Có những tính chất mà ta mong muốn nó không bao giờ đƣợc xuất hiện trong hệ thống. Trong Promela nó đƣợc biểu diễn bởi never claim Ví dụ 4.5 #define A (divisor > 0) never { /* !([] a) */ T0_init: if :: (! ((A))) -> goto accept_all :: (1) -> goto T0_init fi; accept_all: skip } CHƢƠNG 4: KIỂM CHỨNG CHƢƠNG TRÌNH VỚI SPIN 27 Ở ví dụ trên hệ thống cần thỏa mãn rằng biến divisor luôn phải lớn hơn 0, do vậy trƣờng hợp ngƣợc lại không bao giờ đƣợc xảy ra hay !(a)luôn phải nhận giá trị false. Nhãn T0_init đảm bảo trong khi chƣơng trình đƣợc chạy (và sinh ra các trạng thái), cho đến khi nào A còn đúng, lệnh goto thứ hai luôn luôn đƣợc chọn và Spin sẽ liên tục kiểm tra A. Khi thuật toán của chúng ta là đúng và chƣơng trình không chứa lỗi, Spin sẽ kết thúc sau khi sinh ra tất cả các trạng thái và thông báo không có trạng thái nào vi phạm đƣợc tìm thấy. Nhƣng nếu chƣơng trình tính toán đến một trạng thái mà ở đó A sai (divisor nhỏ hơn hoặc bằng 0) lệnh goto thứ nhất sẽ đƣợc thực hiện, Spin nhảy tới nhãn accept_all và kết thúc chƣơng trình. Trong Spin ta chỉ cần biểu diễn tính chất của hệ thống dƣới dạng một biểu thức LTL sau đó đƣa vào Spin, Spin sẽ tự động chuyển biểu thức LTL sang cấu trúc never claim của Promela dùng vào việc kiểm chứng. Trong jSpin ta chỉ cần nhập biểu thức LTL và chạy Translate. Biểu thức LTL đƣợc lƣu lại trong tệp .prp có tên trùng với tên chƣơng trình. Đoạn mã never claim đƣợc Spin lƣu lại trong tệp .ltl Tính chất ở ví dụ 1.3 đƣợc qua biểu thức [] (divisor > 0) CHƢƠNG 5: THỰC NGHIỆM 28 Chương 5 Thực Nghiệm 5.1.Mô tả bài toán 5.1.1.Mô hình máy hữu hạn trạng thái Mô hình máy hữu hạn trạng thái (FSM – Finite State Machine) đƣợc sử dụng để mô tả hoạt động của nhiều hệ thống trong thực tế. Mô hình máy hữu hạn trạng thái bao gồm một số hữu hạn các trạng thái, các bƣớc chuyển trạng thái (sang một trạng thái khác). Ta đề xuất cách thức để chuyển FSM sang mô hình Promela nhƣ sau  Các bƣớc chuyển trạng thái đƣợc khai báo trong một biến kiểu mtype  Thông tin về sự chuyển trạng thái đƣợc truyền trên một biến message kiểu kênh nhận thông điệp thuộc loại mtype trên, kênh message sẽ gửi thông điệp trong tiến trình coltrol() là tiến trình điều khiển hoạt động của máy trạng thái.  Trạng thái của máy đƣợc thể hiện bởi biến state có giá trị đƣợc thay đổi trong tiến trình action(), kênh message sẽ nhận thông điệp trong tiến trình action().  Mỗi khi tiến trình điều khiển coltrol() gửi một thông điệp về sự chuyển trạng thái, dựa vào thông điệp nhận đƣợc và giá trị hiện tại của state, state sẽ đƣợc gán một giá trị mới tƣơng ứng với trạng thái mới. 5.1.2.Ví dụ về mô hình máy hữu hạn trạng thái Ta xem xét một cái đèn có 3 trạng thái: tắt (off), sáng yếu (low), sáng mạnh (high) với công tắc có hai nút up và down. Hoạt động của đèn đƣợc thể hiện bởi mô hình máy hữu hạn trạng thái nhƣ sau: CHƢƠNG 5: THỰC NGHIỆM 29 Hình 5.1.Mô hình máy hữu hạn trạng thái mô tả hoạt động của đèn Mô hình promela mô tả hoạt động của đèn đƣợc xây dựng nhƣ sau: mô hình promela gồm 2 tiến trình: lamp() và switch() (lần lƣợt tƣơng ứng với active() và control()). Để thể hiện tƣơng tác giữa công tắc và bóng đèn hai tiến trình trao đổi thông tin qua kênh updown nhận và gửi thông điệp thuộc kiểu mtype = { up, down } Mô hình promela của cái đèn (file lamp.pml): byte state=0; mtype={up,down}; chan updown=[0] of {mtype}; proctype lamp(){ do ::atomic {updown?up->if ::state=0 -> state=1 ::state=1->state=2 ::state=2->state=2 ::else -> skip fi } ::atomic {updown?down->if ::state=0-> state=0 off down up up down up low low high CHƢƠNG 5: THỰC NGHIỆM 30 ::state=1->state=0 ::state=2->state=1 ::else -> skip fi } od } proctype switch(){ do ::updown!up; ::updown!down; od } init{ atomic{ run lamp(); run switch();} } Trong mô hình trên giá trị của biến state là 0, 1, 2 lần lƣợt mô tả ba trạng thái của đèn là off, low, high. Với mô hình này, trong Spin ta chạy chế độ random, để có thể kiểm tra lỗi của bản thân chƣơng trình Promela. Trong chế độ này, khi tiến trình init đƣợc thực thi, Spin giả lập hoạt động của đèn, chuỗi các tín hiệu up và down đƣợc sinh ra một cách tùy ý (nhờ sự thực thi tiến trình switch()) và từ đó trạng thái của đèn thay đổi (nhờ sự thực thi tiến trình lamp()). Chƣơng trình không có lỗi cú pháp và Spin dừng sau khi đạt tới giới hạn 250 bƣớc. CHƢƠNG 5: THỰC NGHIỆM 31 Hình 5.2.Kết quả khi chạy giả lập mô hình hệ thống đèn ở hình 5.1 5.2.Thực nghiệm Phần thực nghiệm đã xây dựng đƣợc công cụ nhận môt mô tả thô của hệ thống ở dạng máy hữu hạn trạng thái và chuyển đổi thành mô hình promela để kiểm chứng trong Spin. Mô tả ban đầu của hệ thống là một file input.txt đã đƣợc tạo trƣớc, trong đó mỗi bƣớc chuyển trạng thái đƣợc viết trên một dòng: nếu hệ thống đang ở before_state mà nhận đƣợc tín hiệu message_1 thì hệ thống sẽ đƣợc chuyển sang after_state. before_state:message_1:after_state Các bƣớc chuyển có cùng before_state cần đƣợc viết trên các dòng liên tiếp nhau. Khi đọc vào file input.txt, chƣơng trình thống kê và lƣu lại các trạng thái của hệ thống. Các bƣớc chuyển nằm giữa 2 dấu hai chấm cũng đƣợc đọc và dòng mã Promela CHƢƠNG 5: THỰC NGHIỆM 32 định nghĩa kiểu mtype đƣợc sinh ra. Sau đó chƣơng trình đọc lại file input.txt lần thứ hai và sinh ra đoạn mã nằm trong tiến trình action() thể hiện các hành vi của hệ thống khi nhận đƣợc các thông điệp chuyển trạng thái. Nhờ các bƣớc chuyển trạng thái đã đƣợc ghi lại, chƣơng trình sinh tiếp ra đoạn mã nằm trong tiến trình control(). Cuối cùng, đoạn mã khởi tạo hai tiến trình control() và action() (đƣợc đặt trong init()) đƣợc sinh ra. Bảng thể hiện giá trị của biến state tƣơng ứng với mỗi trạng thái cũng đƣợc in ra ở dạng chú thích (nằm trong cặp dấu /* và */) Ta đƣa vào chƣơng trình 1 file chỉ bằng cách đổi tham số trong hàm read (inputFile, outputFile) 5.2.1.Áp dụng kiểm chứng mô hình hệ thống đèn Mô tả ban đầu của mô hình cái đèn ở hình 5.1 đƣợc lƣu trong file state.txt có dạng: off:up:low off:down:off low:up:high low:down:off high:up:high high:down:low Ta đƣa tham số cho hàm read(): read (lamp.txt, lampcode.txt); và chạy chƣơng trình, chƣơng trình sẽ tạo ra file lampcode.txt với nội dung tƣơng đƣơng với đoạn mã trong phần 4.1.2 mô hình hóa cái đèn (phụ lục A). Sau khi chạy giả lập ở chế độ random nhƣ ở phần 5.2.2 ta cần kiểm tra tính chất mà hệ thống cần thỏa mãn bằng việc chạy verify. Tính chất cần kiểm chứng trong trƣờng hợp này là: khi đèn ở trạng thái high, cần phải qua trạng thái low rồi mới có thể về trạng thái off. Biểu thức LTL mô tả tính chất trên là CHƢƠNG 5: THỰC NGHIỆM 33 [] !((state = = 2) && (state != 1) U (state = =0)) (không bao giờ xảy ra trƣờng hợp biến state bằng 2 và, nó luôn khác 1 cho tới khi nó bằng 0) Ta thêm vào mô hình promela định nghĩa các kí hiệu #define a0 (state = = 0) #define a1 (state != 1) #define a2 (state = = 2) Biểu thức LTL đƣa vào Spin là [] !(a2 && (a1 U a0)) Spin sẽ sinh ra cấu trúc never claim, ta thêm nó vào chƣơng trình (phụ lục B) và chạy verify, kết quả cho thấy không có lỗi vi phạm do vậy hệ thống thỏa mãn tính chất cần kiểm tra. Hình 5.3.Kết quả kiểm chứng mô hình 5.1 của hệ thống đèn CHƢƠNG 5: THỰC NGHIỆM 34 5.2.2.Áp dụng kiểm chứng mô hình không đáp ứng thuộc tính Hình 5.4.Mô hình sai của hệ thống đèn Ta xem xét một mô hình của hệ thống đèn không thỏa mãn tính chất đã nêu trong phần 5.2.1.Trong mô hình trên từ trạng thái high, cái đèn có thể chuyển về trạng thái off mà không qua trạng thái low. Tệp mô tả các trạng thái của đèn lamp2.txt: off:up:low off:down:off low:up:high low:down:off high:up:high high:down:off Sau khi dùng công cụ để chuyển mô hình trên sang mã promela (phụ lục C) và thêm cấu trúc never claim để kiểm chứng tính chất nhƣ đã nêu ở 5.2.1 ta có mô hình promela cho mô hình 2 của cái đèn (phụ lục D) và chạy verify, kết quả cho thấy Spin báo lỗi vi phạm, suy ra mô hình vừa đƣa vào không thỏa mãn tính chất cần kiểm tra. off low high down up up down down down CHƢƠNG 5: THỰC NGHIỆM 35 Hình 5.5.Kết quả kiểm chứng mô hình 5.4 của hệ thống đèn CHƢƠNG 6: KẾT LUẬN 36 Chương 6 Kết Luận 6.1.Kết quả của khóa luận Sau khi tìm hiểu tƣ tƣởng và cách tiếp cận của kỹ thuật model checking cùng với hoạt động của model checker Spin, ngôn ngữ Promela và mô hình máy hữu hạn trạng thái, em đã xây dựng đƣợc cách chuyển đổi mô hình máy hữu hạn trạng thái sang ngôn ngữ Promela. Từ đó em đã cài đặt đƣợc công cụ từ một mô tả thô của hệ thống (dƣới dạng máy hữu hạn trạng thái) sinh ra đoạn mã Promela mô hình hóa hệ thống, từ đó dùng để kiểm chứng hệ thống trong Spin. 6.2.Hướng nghiên cứu tiếp theo Tiếp theo, chƣơng trình sẽ đƣợc phát triển để từ đó mô tả thô của bài toán có thể đƣợc nhập trực tiếp từng dòng với một giao diện, và có thể báo lỗi khi tệp đƣa vào không đúng định dạng (nhƣ trƣờng hợp trên một dòng chỉ có một dấu hai chấm, nhƣ vậy chƣơng trình hiện tại chƣa xử lý đƣợc). 37 Phụ lục Phụ lục A: Tệp lampcode.txt /* Trang thai Gia tri state off 0 low 1 high 2 */ byte state = 0; mtype={up,down}; chan message=[0] of {mtype}; proctype action(){ do ::atomic {message?up -> if ::state=0 -> state = 1 ::state=1 -> state = 2 ::state=2 -> state = 2 ::else -> skip fi } ::atomic {message?down -> if ::state=0 -> state = 0 ::state=1 -> state = 0 ::state=2 -> state = 1 ::else -> skip fi } od } proctype control(){ do ::message!up; ::message!down; od } init{ atomic{ run action(); run control();} } 38 Phụ lục B: Tệp lampcode.pml khi chạy verify trong Spin /* Trang thai Gia tri state off 0 low 1 high 2 */ byte state = 0; mtype={up,down}; chan message=[0] of {mtype}; proctype action(){ do ::atomic {message?up -> if ::state==0 -> state = 1 ::state==1 -> state = 2 ::state==2 -> state = 2 ::else -> skip fi } ::atomic {message?down -> if ::state==0 -> state = 0 ::state==1 -> state = 0 ::state==2 -> state = 1 ::else -> skip fi } od } proctype control(){ do ::message!up; ::message!down; od } init{ atomic{ run action(); run control();} } #define a0 (state == 0) #define a1 (state != 1) #define a2 (state == 2) 39 never { /* !([](!(a2 && (a1 U a0)))) */ T0_init: if :: ((a0) && (a2)) -> goto accept_all :: ((a1) && (a2)) -> goto T0_S4 :: (1) -> goto T0_init fi; T0_S4: if :: ((a0)) -> goto accept_all :: ((a1)) -> goto T0_S4 fi; accept_all: skip } 40 Phụ lục C: Tệp lamp2code.txt /* Trang thai Gia tri state off 0 low 1 high 2 */ byte state = 0; mtype={up,down}; chan message=[0] of {mtype}; proctype action(){ do ::atomic {message?up -> if ::state==0 -> state = 1 ::state==1 -> state = 2 ::state==2 -> state = 2 ::else -> skip fi } ::atomic {message?down -> if ::state==0 -> state = 0 ::state==1 -> state = 0 ::state==2 -> state = 0 ::else -> skip fi } od } proctype control(){ do ::message!up; ::message!down; od } init{ atomic{ run action(); run control();} } 41 Phụ lục D: Tệp lamp2code.pml khi chạy verify trong Spin /* Trang thai Gia tri state off 0 low 1 high 2 */ byte state = 0; mtype={up,down}; chan message=[0] of {mtype}; proctype action(){ do ::atomic {message?up -> if ::state==0 -> state = 1 ::state==1 -> state = 2 ::state==2 -> state = 2 ::else -> skip fi } ::atomic {message?down -> if ::state==0 -> state = 0 ::state==1 -> state = 0 ::state==2 -> state = 0 ::else -> skip fi } od } proctype control(){ do ::message!up; ::message!down; od } init{ atomic{ run action(); run control();} } #define a0 (state == 0) 42 #define a1 (state != 1) #define a2 (state == 2) never { /* !([](!(a2 && (a1 U a0)))) */ T0_init: if :: ((a0) && (a2)) -> goto accept_all :: ((a1) && (a2)) -> goto T0_S4 :: (1) -> goto T0_init fi; T0_S4: if :: ((a0)) -> goto accept_all :: ((a1)) -> goto T0_S4 fi; accept_all: skip } 43 Phụ lục E: Mã nguồn của chương trình #include #include using namespace std; void read(char* inFile, char* outFile) { ifstream input(inFile, ios::in); ofstream output(outFile, ios::out); if(!input) { cerr<<"ERROR"; return; } string* state[10];//mang luu cac trang thai string* message[10];//mang luu cac thong diep chuyen trang thai int i=0,j=0,k1=1,k2=1; //Doc file string s; input >> s; int len = s.length(); while (s[i] != ':' && i <= len) i++; state[0] = new string[10]; *state[0] = s.substr(0,i); string tmp1 = *state[0]; j = i+1; while (s[i+1] != ':' && i < len) i++; message[0] = new string[10]; *message[0] = s.substr(j,i-j+1); string tmp2 = *message[0]; while (input >> s) { 44 len = s.length(); i = 0; while(s[i]!=':' && i<= len) i++; string tm = s.substr(0,i); if (tm != tmp1) { tmp1 = tm; state[k1] = new string[10]; *state[k1] = tm; k1++; } j = i+1; while(s[i+1]!=':'&& i<len) i++; string tmp2 = s.substr(j,i+1-j); int kt=0; for(int m=0;m<k2;m++) if (tmp2 == *message[m]) { kt = 1; break; } if (kt == 0) {*message[k2] = tmp2; k2++;} if(input.eof()) break; } input.close(); //In file output<<"/*\nTrang thai\tGia tri state\n"; for(int m=0;m<k1;m++) output<<*state[m]<<"\t\t"<<m<<"\n"; output<<"*/\n"; output << "byte state = 0;\nmtype={"; for(int m=0;m<k2;m++) if(m == (k2-1)) output<<*message[m]<<"};"; else output<<*message[m]<<","; output<<"\nchan message=[0] of {mtype};\nproctype action(){\n\tdo"; 45 for(int m=0;m<k2;m++) { output if\n\t\t"; ifstream input(inFile, ios::in); while (input >> s) { len = s.length(); i=0; while(s[i] != ':' && i <= len) i++; j=i+1; while(s[i+1] != ':' && i < len) i++; if (s.substr(j,i-j+1) == *message[m]) { for(int n=0;n<k1;n++) if (s.substr(0,j-1) == *state[n]) { output state = "; break; } for (int n=0;n<k1;n++) if (s.substr(i+2,len-i) == *state[n]) { output<<n<<"\n\t\t"; break; } } } output skip fi\n\t\t}"; input.close(); } output<<"\n\tod\n\t}\nproctype control(){\n\tatomic{"; for(int m=0;m<k2;m++) output<<"\n\t\tmessage!"<<*message[m]<< ; output<<"\n\t\t}\n\t}"; output<<"\ninit{\n\tatomic{\n\t\trun action();\n\t\trun control();}\n\t}"; } int main() 46 { read("lamp.txt", "lampcode.txt"); return 0; } 47 Tài liệu tham khảo [1] C. Baier, JP Katoen, K. Larsen, Principale of Model Checking, MIT Press, May 2008. [2] Clarke, Grumberg, and Peled, Model Checking, MIT Press, 2000. [3] Mordechai Ben-Ari, Principale of the Spin Model Checker. [4] Dang Van Hung, Model-Checking and the Spin Modelchecker, The United Nations University, International Institute for Software Technology. [5] Sagar Chaki, Introduction to Spin and Promela, Carnegie Mellon University. [6]