Đề 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 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. Chương 1. ERIGONE TRÊN CÔNG CỤ EUI I/ Giới thiệu tổng quan 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 – 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: 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 : 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 -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 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 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: EUI cần Java JRE phiên bản thấp nhất là 1.5 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 Variable_Size_Index Byte range 0..15 Size of variables in a state vector 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 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 -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 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 :: !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ự. Ví dụ với second.pml 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 { 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 Sử dụng mode Interactive 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)}, 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, Safety không có giao tranh 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<=1) } 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ị. Safety với câu lệnh LTL Chứng minh khái niệm về sự công bằng với câu lệnh LTL Chương trình sau là một ví dụ đơn giản để chứng minh khái niệm về sự công bằng fair1.pml: byte n = 0; bool flag = false; ltl { flag } active proctype p() { do :: flag -> break; :: else -> n = 1 - n; od } active proctype q() { flag = true } Nếu tiến trình q thực hiện, nó sẽ thiết lập cờ là đúng và tiến trình p sau đó sẽ chấm dứt. Khi ta chọn mode Accept, mô hình kiểm tra tìm kiếm cho một chu trình chấp nhận (acceptance cycle) – một thuật ngữ kĩ thuật cho một lỗi trong một xác minh của một công thức LTL có chứa kí hiệu () và kết quả trả về là: verification terminated=acceptance cycle, line=9,statement={else -> n = 1 - n}, Verification với Accept Chọn mode Guided ta sẽ được một phản ví dụ đối với sự đúng đắn của thuộc tính, kết quả trả về có dạng: simulation terminated=end of acceptance cycle, line=9,statement={else -> n = 1 - n}, Với Fairness, nó thực hiện một xác minh trong chế độ Accept với mức công bằng yếu. Trong chế độ, chỉ tính toán một cách yếu ớt sự công bằng những ứng viên cho chu trình chấp nhận. Trong một cách yếu ớt tính toán công bằng, quá trình chuyển đổi liên tục được kích hoạt cuối cùng phải được thực hiện. Kể từ khi câu lệnh gán flag=true là xác thật liên tục kích hoạt, nó phải được thực hiện. Khi đó kết quả là: verification terminated=successfully, Verification với Fairness Chương 2: ERIGONE BẰNG CÂU LỆNH I/ Tìm hiểu về Erigone bằng dòng lệnh: Sau khi tải file chứa erigone-N.zip ở trang , với N là số phiên bản, mã nguồn chương trình trong erigone-source-N.zip. Sau khi giải nén file lư trữ erigone-N.zip chứa các thư mục : dist: thư mục dist chứa file erigone-release.html đây là file ghi nội dung các phiên bản của erigon và ngày phát hành có thể link trực tiếp đến trang chủ nếu máy có kết nối mạng internet. docs: Chứa hai file erigone-quick.pdf và erigone-ug.pdf đó là hai file giới thiệu và hướng dẫn sử dụng phần mềm erigone.exe, list.exe, trace.exe, vmc.exe. examples: Thư mục chứa các file mã nguồn ví dụ Promela. vmc-examples: Thư mục chứa mã nguồn ví dụ Promela có thể chuyển đổi mô hình tốt bằng chương trình VMC. Erigone: Hướng dẫn thực hiện chạy chương trình: Câu lệnh: erigone [arguments] filename erigone là tên của chương trình thực thi [arguments] đối số truyền vào để thực thi câu lệnh theo yêu cầu. Filename là file mã nguồn Promela (Được định đạng file là pml). Ví dụ erigon –i ch1.pml Nếu mã nguồn promela chứa ở một thư mục khác thì cấu trúc câu lệnh là: erigone [arguments] fodder\filename (Trong đó folder là thư mục chứa file mã nguồn pml). Ví dụ: ….\erigone –i examples\ch1.pml (Thư mục examples chứ file ch1.pml). Để tìm hiểu thêm về cấu trúc câu lệnh erigon ta sử dụng cú pháp: erigone –h Trong đó [arguments] gồm có: 1.1. Thực thi theo phương thức: -a: acceptance verification – kiểm chứng chấp nhận -c: compilation only – chỉ biên dịch file chương trình chứ không chạy chương trình sẽ in ra file biện dịch phần mở rộng là aut -f: fairness(công bằng) verification – kiểm chứng tương đương -g: guided simulation – hướng mô phỏng -gN: guided simulation – hướng mô phỏng với tham số N - i:interactive simulation – mô phỏng sự tương tác -r: random simulation – mô phỏng ngẫu nhiên (mặc định) -s: safely verification – kiểm chứng an toàn(tin cậy). 1.2. Hiển thị lựa chọn với các đối số: -d display everything – hiển thị toàn bộ. -dX: đối số động X, là một trong chuỗi của các đối số 1.3. Biên dịch chạy thông điệp: -dg Pro[g]ress notification. -dp Program symbols and transitions -dr Runtime statistics -dv version and copyright message – Chạy chường trình và in ra thông báo về phiên bản 1.4. Chuyển tiếp(transitions): -da: all transitions – toàn bộ chuyển tiếp(giữa các tiến trình với câu lệnh) -db: buchi automata – Biên dịch chuyển đổi tự động file pml sang file aut -dc: chosen transitions(simulation) - mô phỏng lựa chọn chuyển đổi. -de: executable transitions from a state – thực thi chuyển đến từ một trạng thái -dl: location stack – vị trí ngăn xếp -dt: trail: -dy: byte code 1.2.c Trạng thái: -dh: state in the hash table – trạng thái ở trong bảng băm -dm: states in a simulation – trạng thái trong mô phỏng -do: channel contents – nội dung kênh -ds: state stack – trạng thái ngăn xếp 1.5. Chuyển đổi LTL: -db: buchi automaton -dn: nodes in the LTL tableau 1.6. Kiểm tra lỗi(debug arguments) Đối số hiển thị lỗi dữ liệu –u. Lựa chọn các đối số -ux với x là kí tự hoặc chuỗi kí tự truyền vào. -uc: compiler tokens -ui: Interpreter stack -ur: P[r]reprocessor 2. List: List đọc và chuyển đổi hiển thị file một cách tự động sang file có đôi mở sau khi dịch chương trình, Biên dịch: erigone -c filename list filename Trước khi chạy list cần biên dịch chương trình bằng erigone (erigone -c filename) trình biên dịch sẽ ghi ra một file chạy (filename.aut) rồi chạy câu lệnh list filename list sẽ chuyển dổi file biên dịch ra file (filemame.lst) trong đó ghi lại trạng thái tiến trình chạy của chương trình theo các phần. 3. Trace: Trace thực thi chuỗi sử lý lựa chọn trong file biên dịch của erigone, nó hiển thị đầu ra mô phỏng dưới dạng bảng.Đẩu tiên: erigone -dcmop filename > filename.trc Viết ra file với các đối số và trạng thái thực hiện. trace [arguments] filename Với các bảng đối số: -tn: number of lines between column [t]itles – số dòng của giưa các cột. -ln: column width for [l]ine numbers – khoảng rộng độ rộng cho số dòng(line) -pn: column width for [p]rocesses – khoảng rộng độ rộng giữa các tiến trình(processes) -sn: column width for [s]tatements – khoảng rộng độ rộng giữa các cột câu lệnh(statements) -vn: column width for [v]ariables – khoảng rộng của các cột biến( variables) -xs: e[x]clude variables with string – dung để hiển loại trừ giữa các dạng biến. -ms: exclude state[m]ents with string – dung dể loại trừ một số câu lệnh trong bảng 4. VMC VMC (Visualization of Model Checking) là một hậu sử lý với tập lệnh đầu ra của erigone, nó tạo tạo ra chuỗi mô hình đồ thị, các mối quan hệ, trạng thái của chúng. File hiển thị đầu ra với phần mở rộng(đuôi file) trc, bằng cách lựa chọn đối số đầu ra của erigone ta có trạng thái đồ thị mô phỏng tương ứng. Cấu trúc câu lệnh: erigone -dehlmprs filename > filename.trc ta có thể them các đối số đầu ra để có các trạng thái tương ứng erigone -s -dehlmprs filename > filename.trc - với s là trạng thái tin cậy (safely). Hoặc có thể dựa vào bảng I.1.1 erigone -a -dehlmprs filename > filename.trc - với trạng thái kiểm chứng chấp nhận Chạy: vmc filename Chương trình sẽ hiển thị ra file với phần mở rộng (đuôi file) dot là phần chuyển đổi của dạng đồ thị, tên file cũng là số thứ tự nối từ thứ tự đâu đến thứ tự hiện tại. Khi chạy tập tin dot ta dùng phần mềm GRAPHVIZ.MSI tùy vào cấu hình máy dùng dùng hệ điều hành nào bạn download về cài tương ứng với (win32 bit: ) sau khi cài đặt GRAPHVIZ ta bật cửa sổ comand line chuyển đến thư mục chứa file dot để thực thi, rồi thực hiện chuyển đổi file dot ra mô hình đồ thị bằng lệnh: …./dot -Tpng graph1.dot -o graph1.png Chú ý: Muốn hiển thị toàn bộ đồ thị trạng thái ta chọn file dot có chỉ số lớn nhất, việc chuyển file đầu ra có thể được hiển thị bằng file(doc, png, svg, hoăc lựa chọn chuyển đổi ra file pdf). II/ Mô phỏng một số chương trình Promela bằng công cự Erigone 1. Mô phỏng với quá trình truyền thông điệp(chanel) Với chương trình ch1.pml lưu ở thư mục examples. Code: chan ch1 = [2] of { byte, byte, byte}; chan ch2 = [0] of { byte, byte, byte}; byte a, b, c; active proctype p() { ch1 ! 1, 2, 3; ch1 ! 4, 5, 6; ch2 ! 7, 8, 9; ch2 ! 10, 11, 12; } active proctype q() { ch1 ? a, b, c; printf("%d %d %d\n", a, b, c); ch1 ? a, b, c; printf("%d %d %d\n", a, b, c); ch2 ? a, b, c; printf("%d %d %d\n", a, b, c); ch2 ? a, b, c; printf("%d %d %d\n", a, b, c); } Đây là chương trình với việc truyền các biến trong một kênh các byte và tiến trình p (có vai trò như một client), gửi thông điệp đến tiến trình q(có vai trò như một server) có nhiệm vụ hiển thị thông điệp các byte ra màn hinh. Chạy bằng lệnh: erigone examples\ch1 Đẩu ra: Các biến được in ra màn hình, với trạng thái kết thúc ở dòng thứ 20, với câu lệnh statement = {printf(“%d %d %d\n”, a, b, c)}, Ta có thể chọn chế độ chạy thông qua một số các đối số khai báo ở trong phần thực thi các phương thức. Chạy chế độ ngẫu nhiên(random): erigone -r examples\ch1 Output băng EUI: Chạy bằng lệnh Erigone: Giao diện bằng dòng lệnh đã rút gọn chỉ hiển thị kết quả, trong EUI hiển thị các trạng thái tiến trình thông số các biến trong các trạng thái, kết quả đầu ra là như nhau. Mô ta có thể mô phỏng tương tác (interactive simulation – mô phỏng sự tương tác) như trong EUI. Dòng lệnh: erigone –i examples\ch1 Output bằng EUI: Out put bằng comand line: Ở dao diện của eui nếu ta chọn phía (p7 ch1 ! 4, 5, 6) tương đương phái chọn from =0(nếu ta chọn 0) chương trình sẽ hiển thị toàn bộ tiến trình tiếp theo tự động. Nếu ta chọn to = 1(chọn 1) chương trình sẽ chạy từng tiến trình một còn trong dao diện EUI ta chọn p13 ch1 ! a, b, c. Tương tự ta lại lựa chọn như trên. Nếu ta ấn q chương trình chấm dứt. Sau khi chạy lệnh erigon cho file ch1.pml thì thư mục examples tự động xuất hiện file ch1.aut lưu chữ ghi lại các trạng thái tiến trình và biến sau khi chạy. Nếu ta chạy với chế độ -dm: states in a simulation – trạng thái trong mô phỏng Với câu lệnh: erigone –dm examples\ch1 Output: Trên hình ta thấy ở trạng thái thứ 3, 5, 8, 11 kết quả được hiển thị trên màn hình, và kết thúc ở dòng thứ 20. Tương tự với các đối số đầu vào chương trình ta có thể chạy chương trình với chế độ theo như mục (I. 1.1 Thực thi theo phương thức). Ta có thể thực hiện mô phỏng với chế độ random, safety, accept, fairness, interactive, compile, guided như trong EUI bằng câu lệnh lần lượt như sau: erigone – r examples\ch1(chế độ random) erigone – i examples\ch1(chế độ interactive) erigone – s examples\ch1(chế độ safety) erigone – c examples\ch1(chế độ compile) erigone – f examples\ch1(chế độ fairness) erigone – g examples\ch1(chế độ guided) 2. Mô phỏng chương trình tương tranh Với chương trình “Second Attempt” xem xét vấn đề loại trừ lẫn nhau, (Ben- Ari, 2006, Section 3.6) trong thư mục examples file second.pml. Biên dịch bằng erigone examples\second Ta được: Chương trình sẽ chạy đến mức giới hạn khi có lỗi xảy ra tương tranh và biến critical sẽ vượt quá 1, chương trình tự thoát và in ra màn hình trạng tái ở dòng thứ 22. Ta có thể thực hiện mô phỏng với chế độ random, safety, accept, fairness, interactive, compile, guided như trong EUI bằng câu lệnh lần lượt như sau: erigone – r examples\second(chế độ random) erigone – i examples\second(chế độ interactive) erigone – s examples\second(chế độ safety) erigone – c examples\second(chế độ compile) erigone – f examples\second(chế độ fairness) erigone – g examples\second(chế độ guided) Ngoài thực hiện như trong giao diện EUI erigone thực hiện giao diện bằng câu lệnh như : erigone –dm examples\second(Hiển thị các trạng thái) erigone –dv examples\second(Hiển thị phiên bản và trạng thái) …. 3. Kiểm chứng độ tin cậy khi sử dụng LTL Với chương trình second.pml giờ loại bỏ câu lệnh assert và ta dùng LTL để kiểm soát tương tranh bằng file second-ltl.pml. Khi ta chạy chương trình với câu lệnh: erigone examples\second-ltl Chương trình sẽ thông báo có quá nhiều nhiều bước(too many steps) hay chương trình có khả năng chạy không dừng vì tương tranh được giải quyết, chương kết thúc ở một trạng thái bất kỳ khi đưa ra thông báo vì với ltl lỗi tương tranh được giải quyết và chương trình sẽ có khả năng lặp lại. erigone –s examples\second-ltl Chương trình đưa ra thông báo kiểm soát tương tranh thành công erigone –s –t examples\second-ltl Chươn trình đưa ra cảnh báo sẽ không bao giờ chấm dứt bắt đầu vòng lặp ở trạng thái thứ 11. Để kiểm tra trạng thái của chương trình ta dùng câu lệnh erigone –dm examples\second-ltl Ta thấy trạng thái của chương trình chạy mãi mãi không dừng. Xem hình: III/ Chương trình List List được sử dụng để tự chuyển đổi chương trình khi ta biên dịch chương trình bằng erigone, list sẽ chuyển đổi file biên dịch thành file có đuôi chấm list ghi lại mô hình của các tiến trình. Câu lệnh phải chạy chương trình erigone trước để có file chương trình đinh dang aut. list filename IV/ Chương trình Trace Trace sử lý dữ liệu đầu ra của erigone dưới dạng bảng. Với file second.pml erigone –dcmop examples\second > examples\second.trc Ta có thể chuyển tiếp file đầu ra dưới dạng txt hoạc chuyển truc tiếp ra file doc khi cần để lưu trữ là erigone –dcmop examples\second > examples\second.txt erigone –dcmop examples\second > examples\second.doc file dầu ra của trace ghi lại các trạng thái tập thông báo các loại sử lý, khi biên dịch hiển thị ra màn hình ta bắt buộc phải có định dạng chuyển đổi ra file định dạng trc. Chạy chương trình ta có thể truyền thêm tham số để định dạng hiển thị: Khi chạy trace thông thường ta có trace examples\second, giờ ta có thể định số dòng giữa các cột giả sử lấy 3 dòng thành một nhóm. trace –t3 texamples\second. Trong hiển thị trên ta thấy các trạng thái biến, và các ở trong tiến trình nào dòng bao nhiêu, giái trịnh wantp, wantq = 0 hoặc 1 là trạng thái dùng để kiểm soát biến critical sao cho luôn bằng giá trị 1, ở dòng thứ 10 giá trị đã bị lỗi khi biến critical == 2 và chương trình đã in ra lỗi. Khi ta muốn nhóm một số dòng lại cho đễ hiển thị ta thêm đối số tn với n là số dòng cần nhóm. Tương tự khi ta thể căn bản như trong phần hướng dẫn của trace. Giả sử ta muốn tăng độ rộng của các cột lên 2 hoặc lên 8, ta dùng lệnh trace – l2 examples\second hoặc trace – l8 examples\second ta thấy độ rộng của các cột dộng dòng(line) với cột câu lệnh(statement) có nghĩa là mở rộng khoảng cách của cột line trong trường hợp cột có chỉ số dòng lớn. Tương tự ta có thể định dạng như trong phần mục trace. Bây giờ ta có thể xóa những cột hoặc dòng không cần thiết bằng cách cho thêm tham biến Giả sử ta muốn xóa cột biến want chỉ để lại biến critical ta sử dụng lệnh –xs#(với s là chuỗi(string) cần xóa), còn muốn xóa dòng có các lệnh ta dùng đối số -ms#(s là chuỗi cần xóa) . Ta dùng lệnh trace –xwant# -mwant# -massert# examples\second Ta còn lại được các biến và các lệnh critical. V/ Chương trình VMC VMC chuyển đổi file thự thi của chương trình erigone sang mô hình đồ họa được lưu dưới dạng dot, để chuyển đổi file dot sang file ảnh ta dùng graphviz với hướng dẫn ở trên, ta thử chuyển đổi file chương trình second thành dạng mô hình để mô hình hóa trạng thái và tiến trình. Ta chạy chương trình với chế độ safely(-s) để cho tối thiếu các tiến trình, nếu chạy thông thường thì trạng thái tiến trình ghi lại lên đến hơn 100 file dot. erigone -s -dehlmprs examples\second > examples\second.trc vmc examples\second Ta chọn file second-046.dot là file lớn có chỉ số dot lớn nhất vì file này chứa toàn bộ các trạng thái tính toán, ta chuyển file dot về mô hình đồ thị thể hiện mối quan hệ các trạng thái tính toán(ta sử dụng lệnh dot –Tjpg second-046.dot -o second.jpg tên file đầu ra đặt tùy ý còn –Tjpg có nghĩa chúng ta chuyển file dot sang file jpg, phần file đầu ra phải đặt đúng dạng file là jpg) ta có mô hình đồ thị. Các ô vuông và tròn thể hiện trạng thái trong một thời điểm, mũi tên thể hiện sau khi thực hiện xong một trạng thái xẽ chuyển đến trạng thái tiếp theo, các chỉ số trong ô vuông là các chỉ số dòng lệnh thực hiện trong một trạng thái 3 giá trị ở dưới lần lượt là các giá trị wantp, wantq, critical, ô vuông có viền thể hiện ở trạng thái đó có lặp lại trạng lại thái, ô tròn đỏ thể hiện lỗi của chương trình và kết thúc chương trình. Ví dụ trạng thái đầu: Trong ô vuông trên đầu thể hiện viền in đậm nói rằng trạng thái đầu có thể được lặp lại chu trình, 7!wantq, 19!wantp số 7 và 19 thể hiện dòng lệnh trong số 7 và 19 trong trạng thái, số 0 0 0 là giá trị biến wantp, wantq, critical, mũi tên thể hiện từ trạng thái ban đầu chương trình chuyển xuốn trạng thái tiếp theo. KẾT LUẬN Erigone là một công cụ mô phỏng dùng để kiểm chứng hệ thống, đựa trên mô hình Jspin và được triển khai lại riêng giúp cho việc mô phỏng kiểm chứng hệ thống được dễ dàng, uyển chuyển, chính xác, theo theo chuẩn. Với khả năng tùy biến kiểm chứng bằng công cụ đồ họa EUI, và qua dòng lệnh với các đối số tham biến nhằm mục đích xem xét kiểm chứng hệ thống với nhiều trường hợp và có thể chuyển đổi mô hình trạng thái bằng đồ thị, ta có thể dễ dàng xem sét phân tích một cách trực quan. Erigone là một công cụ mã nguồn mở viết bằng ADA với mục đích theo chuẩn, ta cũng có thể tùy biến đầu ra của chương trình nhờ vào mã nguồn mở của công cụ, nhưng trong tài liệu này chúng em chỉ tìm hiểu được về mô hình và một số cách thức sử dụng chương trình bằng công cụ erigone và việc tùy biến đầu ra chúng em vẫn chưa thể tìm hiểu được rất mong được sự giúp đỡ của thầy cô và các, để để giúp chúng em sẽ hoàn thành tốt được tài liệu hơn. TÀI LIỆU THAM KHẢO The ERIGONE Model Checker Quick Start Guide - Mordechai (Moti) Ben-Ari Principles of the Spin Model Checker - Mordechai Ben-Ari The ERIGONE Model Checker User’s Guide (Version 3.2.1) - Mordechai Ben-Ari The ERIGONE Model Checker (Version 1.0.0) - Mordechai Ben-Ari Tool Presentation Teaching Concurrency and Model Checking - Mordechai Ben-Ari