Đề tài: TÌM HIỂU ERIGONE MODEL CHECKER

Chia sẻ: Nguyen Tuan Anh | Ngày: | Loại File: DOC | Số trang:48

Thêm vào BST

Báo xấu

67
lượt xem 18
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Erigone là mô hình triển khai lại của mô hình kiểm chứng Spin được phát triển với mục đích kiểm chứng được dễ dàng trực quan, uyển chuyển nhằm thuận lợi cho việc nghiên cứu và mô phỏng mô hình hệ thống, erigone có thể được thực hiện bằng công cụ trên giao diện đồ họa EUI hoặc thao tác bằng câu lệnh dưới dạng command line với nhiều tùy biến lựa chọn cho phép kiểm chứng hoạt động của hệ thống....

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Đề tài: TÌM HIỂU ERIGONE MODEL CHECKER

ĐẠI HỌC CÔNG NGHỆ - ĐẠI HỌC QUỐC GIA HÀ NỘI KHOA CÔNG NGHỆ THÔNG TIN BÁO CÁO Đề tài: TÌM HIỂU ERIGONE MODEL CHECKER Giảng viên hướng dẫn : TS. Đặng Đức Hạnh TS. Vũ Diệu Hương Sinh viên thực hiện : Lưu Hoàng Tùng Nguyễn Công Đức Hà nội - 2012
MỤC LỤC LỜI NÓI ĐẦU............................................................................1 Chương 1. ERIGONE TRÊN CÔNG CỤ EUI...........................2 I/ Giới thiệu tổng quan..................................................................................................................2 1.Giới thiệu Erigone model checker..........................................................................................2 2.Công cụ phát triển.................................................................................................................3 2.1. Command line.............................................................................................................3 2.2. EUI (Erigone User Interface).........................................................................................7 3.Mô phỏng và xác minh trong Erigone....................................................................................9 4.Chương trình Trace................................................................................................................9 II/ Ví dụ demo.............................................................................................................................10 1.Giải quyết hai tiến trình loại trừ lẫn nhau............................................................................10 2.Loại trừ lẫn nhau với một semaphore..................................................................................12 3.Xác minh một chương trình Promela với câu lệnh assert....................................................14 4.Xác minh một thuộc tính an toàn sử dụng LTL...................................................................16 5.Chứng minh khái niệm về sự công bằng với câu lệnh LTL.................................................18 Chương 2: ERIGONE BẰNG CÂU LỆNH..............................22 I/ Tìm hiểu về Erigone bằng dòng lệnh:.....................................................................................22 1.Erigone:................................................................................................................................22 1.1. Thực thi theo phương thức:.........................................................................................23 1.2. Hiển thị lựa chọn với các đối số:................................................................................24 1.3. Biên dịch chạy thông điệp:...........................................................................................24 1.4. Chuyển tiếp(transitions):..............................................................................................24 1.5. Chuyển đổi LTL:..........................................................................................................25 1.6. Kiểm tra lỗi(debug arguments)....................................................................................25 Tìm hiểu về Erigone model checker Trang 1
2. List:......................................................................................................................................26 3. Trace:..................................................................................................................................26 4. VMC....................................................................................................................................27 II/ Mô phỏng một số chương trình Promela bằng công cự Erigone...........................................28 1. Mô phỏng với quá trình truyền thông điệp(chanel).............................................................28 2. Mô phỏng chương trình tương tranh...................................................................................34 3. Kiểm chứng độ tin cậy khi sử dụng LTL............................................................................36 III/ Chương trình List...................................................................................................................37 IV/ Chương trình Trace...............................................................................................................37 V/ Chương trình VMC.................................................................................................................40 TÀI LIỆU THAM KHẢO.........................................................44 Tìm hiểu về Erigone model checker Trang 2
LỜI NÓI ĐẦU Erigone là mô hình triển khai lại của mô hình ki ểm ch ứng Spin đ ược phát triển với mục đích kiểm chứng được dễ dàng trực quan, uyển chuy ển nh ằm thuận lợi cho việc nghiên cứu và mô phỏng mô hình hệ thống, erigone có th ể được thực hiện bằng công cụ trên giao diện đồ họa EUI hoặc thao tác b ằng câu lệnh dưới dạng command line với nhiều tùy biến lựa ch ọn cho phép ki ểm chứng hoạt động của hệ thống. Tìm hiểu Erigone model checker nhằm mục đích tìm hiểu rõ hơn về mô hình kiểm chứng erigone thông qua một số ví dụ, được thực hi ện b ằng công c ụ đồ họa EUI và bằng câu lệnh command line, với những nhìn ảnh, phân tích chương trình một cách trực quan. Vì đây là lần đầu tiếp xúc, tìm hiểu về 1 khía c ạnh m ới nên s ẽ không tránh khỏi những khó khăn dẫn đến những thiếu sót trong báo cáo, chúng em mong thầy (cô) bỏ qua. Chúng em xin chân thành cảm ơn thầy cô đã chỉ bảo hướng dẫn chúng em đ ể chúng em có thể hoàn thành báo cáo này. Tìm hiểu về Erigone model checker Trang 1
Chương 1. ERIGONE TRÊN CÔNG CỤ EUI I/ Giới thiệu tổng quan 1. Giới thiệu Erigone model checker Erigone là một phần triển khai lại của mô hình kiểm chứng Spin. Erigone triển khai một tập con của Promela, nó là đủ để chứng minh các khái ni ệm cơ bản của mô hình kiểm chứng cho việc xác minh (verification) của các chương trình đồng thời. Không một ngôn ngữ cấu trúc nào đ ược thêm vào sao cho chương trình cho Erigone có thể được sử dụng với Spin để có nhiều tính uyển chuyển và hiệu suất tốt hơn mong muốn. Erigone được viết bằng ADA năm 2005 cho độ tin cậy, bảo trì và tính linh hoạt. Nó được sử dụng như một chuẩn kiến trúc. Đặc tính của Erigone:  Erigone là đơn nhất, khép kín, tập tin th ực thi đ ể cài đ ặt và s ử d ụng là dễ dàng. Erigone sản sinh một vết (trace) chi tiết trong những thuật toán mô  hình kiểm chứng. Nội dung các vết có thể tùy chỉnh và một định dạng thống nhất dựa trên từ khóa được sử dụng để có th ể được đọc trực tiếp hoặc được sử dụng bởi các công cụ khác.  Mô-đun hóa mở rộng được sử dụng trong việc thiết kế của ch ương trình Erigone tạo điều kiện cho hiểu biết về mã nguồn. Điều này cũng sẽ cho phép các nhà nghiên cứu dễ dàng sửa đổi và mở rộng chương trình.  Ngoài việc kiểm chứng mô hình Erigone còn chứa các chương trình bổ xung riêng biệt: – COMPILER: Chạy chương trình biên dịch của chính nó. – LST: Định dạng đầu ra của trình biên dịch Tìm hiểu về Erigone model checker Trang 2
– TRACE: Định dạng đầu ra của mô hình kiểm chứng – VMC: Tạo đồ thị mô hình từ thuật toán mô hình kiểm tra. Mô hình hoạt động: 2. Công cụ phát triển Erigone có thể được thực thi bằng 2 cách : sử dụng command line và EUI (Erigone User Interface) 2.1. Command line Erigone được xây dựng với trình biên dịch Gnat Ada 2005, nó có th ể được download tại : Tìm hiểu về Erigone model checker Trang 3
http://code.google.com/p/erigone/downloads/list • Cú pháp dòng lệnh: erigone [arguments] filename Với filename: nếu phần mở rộng không được đưa ra trong tệp tin, mặc định mã nguồn PROMELA tập tin đuôi mở rộng là pml. Vi ệc chuy ển đổi tự động tên tập tin thu được bằng cách sử dụng các tập tin g ốc và phần mở rộng aut, và tập tin kéo theo mở rộng là trl. N ếu thu ộc tính đúng đắn LTL của tên tập tin không được đưa ra, mặc đ ịnh là g ốc v ới ph ần m ở rộng prp. • Đối số dòng lệnh: Các chế độ (mode) thực thi  -r Random simulation -i Interactive simulation -g Guided simulation -s Verification of safety -a Verification of acceptance -f Verification with fairness -b LTL to BA translation only -c Compile PROMELA only  Giới hạn thực thi -eN Total st[e]ps 10 -kN State stac[k] 2 -lN [L]ocation stack 3 Tìm hiểu về Erigone model checker Trang 4
-pN [P]rogress step 1 Trong đó, tham số N trong khoảng 1000 và mặc định của nó được liệt kê trong cột 3 của bảng Đối với ngăn xếp, đây là số lượng các khung ngăn xếp và không phải là số lượng các bytes Tổng các bước (Total steps) là số lượng các bước của một mô phỏng hoặc xác minh trước khi thực hiện các chấm dứt Đối với một xác minh, một báo cáo tiến trình có thể được in sau mỗi bước tiến trình(progress step) đã được thực hiện, nếu g được bao gồm trong các đối số hiển thị.  Một số đối số bổ sung: -h Display [h]elp screen -nN Seed of ra[n]dom simulation -o Compiler l[o]gs -t[f] Read L[T]L formula Hạt giống (seed) mặc định thu được từ đồng hồ Các bản ghi của trình biên dịch (compiler logs) bằng văn bản đ ể tách các tập tin, không phải đầu ra tiêu chuẩn. Nếu một tên tệp tin không được đưa ra với đối số -t, các tên t ập tin được xây dựng như mô tả ở trên. Không có khoảng trống giữa -t và tên của tập tin Tìm hiểu về Erigone model checker Trang 5
Nhãn Accept chưa được triển khai, do đó -t nên được thiết lập với chế độ thực thi -a hoặc –f; một thông điệp cảnh báo sẽ được đưa ra nếu điều này chưa được thực hiện.  Đối số hiển thị Đối số -d hiển thị tất cả các dữ liệu. Hiển thị chọn lọc có thể dùng với đối số -dX, trong đó X là một chuỗi của một hoặc nhiều: Compile and runtime messages g Pro[g]ress messages p [P]rogram transitions and symbols r [R]un-time statistics v [V]ersion and copyright notice Transitions a [A]ll transitions from a state c [C]hosen transition (simulation) e [E]xcutable transitions from a state l [L]ocation stack t [T]rail y B[y]te code States h State [h]ash table m States in a si[m]ulation s [S]tate stack Tìm hiểu về Erigone model checker Trang 6
LTL translation messages b [B]üchi automaton n [N]odes in the LT tableau 2.2. EUI (Erigone User Interface) EUI là một môi trường phát triển cho Erigone bao gồm m ột giao diện người dùng đồ họa và các thuật toán để định dạng và hiển thị kết quả của một mô phỏng và xác minh. EUI là m ột chuy ển th ể c ủa JSpin - môi trường phát triển cho Spin. Tập tin cài đặt EUI eui-N.exe (N là số phiên bản) có thể t ải t ừ dự án Jspin tại Google Code: http://code.google.com/p/jspin/ EUI cần Java JRE phiên bản thấp nhất là 1.5 Tìm hiểu về Erigone model checker Trang 7
Giao diện chính của EUI 2.3. Kích thước giới hạn của Erigone Giới hạn về kích thước của các mô hình Promela được biên d ịch vào Erigone có trong ba gói thông số kĩ thuật: Global cho các khai báo c ơ b ản, Config cho các kích cỡ bảng và Config State cho cỡ của các vectơ trạng thái nén trong stack và hash table: Declarations in package Global Identifier Type Meaning Byte mod 256 Values and indices Name String(1..64) Names and source statements Declarations in package Config Identifier Type Meaning Process_Index Byte range 0..7 Processes Symbol_Index Byte range 0..15 Symbols Transition_Index Byte range 0..63 Transitions in a process Location_Index Byte range 0..7 Transitions from any state Byte_Code_Index Byte range 0..63 Byte codes per statement Interpret_Index Byte range 0..63 Interpretation stack Max_Futures constant := 4 Number of future formulas Declarations in package Config_State Identifier Type Meaning Process_Size_Index Byte range 0..3 Size of processes in a state vector Tìm hiểu về Erigone model checker Trang 8
Variable_Size_Index Byte range 0..15 Size of variables in a state vector 3. Mô phỏng và xác minh trong Erigone Khi một mô hình Promela được mô phỏng thường sẽ có nhiều h ơn một tin thực thi (executable) chuyển đổi trong mỗi trạng thái. Sự lựa ch ọn của quá trình chuyển đổi có thể được: random, interactive, hoặc guided bởi các tập tin trail cái mà được viết trong một xác minh. Các mode của xác minh trong Erigone là:  Safety : Kiểm tra sự an toàn của thuộc tính  Acceptance : Kiểm tra cho chu trình chấp nhận  Fairness : Kiểm tra cho chu trình chấp nhận dưới sự công bằng yếu Một thuộc tính đúng đắn có thể được xác định bởi một công thức trong LTL 4. Chương trình Trace Chương trình Trace thực hiện xử lý chuỗi trên dữ liệu đầu ra viết bởi Erigone. Nó in đầu ra của một mô phỏng ở dạng bảng. Đầu tiên thực hiện: erigone -dcmp filename > filename.trc để viết một tập tin với bảng kí hiệu, trạng thái và quá trình chuy ển đ ổi được thực hiện. Sau đó sử dụng câu lệnh: trace [arguments] filename Trong đó các đối số có thể là: -tn Number of lines between column [t]itles -ln Column width for [l]ine numbers Tìm hiểu về Erigone model checker Trang 9
-pn Column width for [p]rocesses -sn Column width for [s]tatements -vn Column width for [v]ariables -xs E[x]clude variables with s -ms Exclude state[m]ents with s -x và -m là đối số sử dụng để lọc đầu ra. Các chu ỗi s là danh sách c ủa các chuỗi chấm dứt bởi # : -xwant# -massert#!# ý nghĩa là một cột cho một biến (-x) hoặc một hàng cho một câu l ệnh (-m) sẽ không được in nếu một trong những chuỗi xuất hiện trong phạm vi biến hoặc câu lệnh, tương ứng. Với các đối số ở trên, các cột cho wantp và wantq sẽ không được in, cũng sẽ không phải hàng với câu lệnh assert hoặc toán tử phủ định. II/ Ví dụ demo 1. Giải quyết hai tiến trình loại trừ lẫn nhau Mã nguồn của chương trình nằm trong tập tin second.pml ở thư mục examples: bool wantp = false, wantq = false; byte critical = 0; active proctype p() { do Tìm hiểu về Erigone model checker Trang 10
:: !wantq; wantp = true; critical++; assert (critical == 1); critical--; wantp = false; od } active proctype q() { /* Symmetrical */ } Mã nguồn Promela được hiển thị trong khung bên trái của giao diện EUI. Ta sử dụng mode Random để chạy một mô ph ỏng, các câu l ệnh được lựa chọn ngẫu nhiên. Kết quả trả về ở khung bên ph ải của giao diện. Nó bao gồm một dòng hiển thị phiên bản hiện tại của Erigone, chế độ được thực thi, chế độ của mô phỏng và cấu hình được s ử dụng. Các trạng thái của mô phỏng được hiển thị ở dạng bảng. Cột đầu tiên là tiến trình mà từ đó một câu lệnh đã được th ực hiện, ti ếp theo là c ột chứa số dòng và mã nguồn của câu lệnh, các cột còn l ại cung c ấp các giá trị của các biến trong trạng thái. Theo sau bảng, kết quả của mô phỏng được đưa ra. Một lỗi giao tranh xảy ra khi biến critical có giá trị là 2 và khi đó mô phỏng sẽ chấm dứt với thông báo: simulation terminated=assert statement is false Với mode Guided ta sẽ nhận được kết quả tương tự. Tìm hiểu về Erigone model checker Trang 11
Ví dụ với second.pml 2. Loại trừ lẫn nhau với một semaphore Mã nguồn của ví dụ được chứa trong tập tin sem.pml trong thư mục examples: byte sem = 1; byte critical = 0; active proctype p() { do :: atomic { Tìm hiểu về Erigone model checker Trang 12
sem > 0; sem-- } critical++; assert(critical == 1); critical--; sem++ od } active proctype q() { /* The same */ } active proctype r() { /* The same */ } Với mode Random tương tự như ví dụ trên, mô phỏng sẽ chạy liên tục cho đến khi ta ngừng mô phỏng hoặc đến một bước nào đó. Không có l ỗi nào xảy ra do ta đã đặt một cờ hiệu tránh cho sự giao tranh. Với mode Interactive, ta có thể lựa chọn các câu lệnh mong muốn được thực thi trong mô phỏng Tìm hiểu về Erigone model checker Trang 13
Sử dụng mode Interactive 3. Xác minh một chương trình Promela với câu lệnh assert Sử dụng chương trình second.pml, với mode Safety, kết quả trả về với thông báo xác minh chấm dứt khi có lỗi xảy ra: verification terminated=assert statement is false, line=22,statement={assert (critical == 1)}, Tìm hiểu về Erigone model checker Trang 14
Safety khi giao tranh Sử dụng chương trình sem.pml với mode Safety kết quả trả về với thông báo: verification terminated=successfully, Tìm hiểu về Erigone model checker Trang 15
Safety không có giao tranh 4. Xác minh một thuộc tính an toàn sử dụng LTL Erigone có thể xác minh một thuộc tính đúng đắn được viết bằng công thức trong ngôn ngữ LTL. Chương trình second-ltl.pml tương tự như second.pml chỉ khác rằng câu lệnh assert được thay bằng một công thức LTL. bool wantp = false, wantq = false; byte critical = 0; ltl { [](critical
active proctype p() { do :: !wantq; wantp = true; critical++; critical--; wantp = false; od } active proctype q() { /* Symmetrical */ } Chọn mode Safety ta được kết quả của xác minh: verification terminated=never claim terminated, line=11,statement={critical--}, Run a guided simulation to see the counterexample steps=8, ... times=,compilation=0.01,verification=0.01, Cụm từ never claim terminated là một thuật ngữ kĩ thuật được sử dụng bởi các mô hình kiểm tra để báo cáo rằng một lỗi đã được tìm th ấy. Cu ối cùng là thông tin về việc thực hiện mô hình kiểm tra được hiển thị. Tìm hiểu về Erigone model checker Trang 17