Đặc tả và xác minh phần mềm là một phương pháp xác minh xem hệ thống có phù hợp với thiết kế hay không. Điều mà một lập trình viên phải làm để có được một sản phẩm phần mềm là luôn phân tích, lập trình, kiểm tra lại và thử nghiệm. Để việc xác minh trở nên dễ dàng, nhanh chóng hơn và tăng độ chính xác, chúng tôi luôn tìm kiếm giải pháp. Công nghệ có thể hỗ trợ việc này và SPIN là một trong những công cụ đó. Các hệ thống cần xác minh được xác định bằng cách sử dụng Promela (Process Meta Language) và sau đó được sử dụng (SPIN-Simple Promela Interpreter) để xác minh. Các thuộc tính cần xác minh được biểu thị bằng công thức LTL, âm và sau đó chuyển sang Büchi Automata. Ngoài việc xác thực mô hình, SPIN còn có thể hoạt động như một trình mô phỏng thực hiện chuỗi thực thi hệ thống và hiển thị dấu vết thực thi cho người dùng.
Luận án giới thiệu bộ kiểm tra mô hình SPIN, các mô hình hệ thống viết bằng ngôn ngữ Promel mà SPIN hiểu được và kiểm định mô hình bằng SPIN.
CHỨNG MÔ HÌNH
Xác minh mô hình là kiểm tra xem phần mềm được sản xuất có đáp ứng yêu cầu, hợp lý và đáp ứng đúng các điều kiện mà phần mềm phải đáp ứng hay không. Việc xác minh mô hình dựa trên mô tả chính xác về hành vi của hệ thống một cách rõ ràng, cho phép phát hiện sự mơ hồ, lỗi và sự không hoàn chỉnh của hệ thống. Việc xác minh mô hình được thực hiện bằng cách xác định các yêu cầu của hệ thống và sau đó xây dựng mô hình của hệ thống, giúp chúng ta hiểu được chức năng và hành vi của hệ thống. Chúng ta có thể xây dựng một mô hình. Cấu hình hệ thống sử dụng các ngôn ngữ lập trình như C, Promela hoặc Java.
Hình 1.2 Sơ đồ hoạt động của phương pháp kiểm chứng mô hình Các bước thực hiện kiểm chứng mô hình. Chúng tôi xây dựng một mô hình từ việc đặc tả các chức năng và yêu cầu của hệ thống. Kiểm tra mô hình cũng là một khả năng đánh giá phần mềm hiệu quả.
Tuy chi phí xây dựng mô hình cao nhưng chi phí duy trì phần mềm khi hệ thống ra mắt lại thấp hơn. Khi kiểm tra mô hình, các trường hợp kiểm thử được tạo tự động để phát hiện nhiều lỗi hơn. Các lỗi được phát hiện sớm sẽ tăng độ phân giải và thời gian phục vụ vì kiểm tra mô hình là một phương pháp xác minh chung.
Vì mô hình hệ thống phải được xây dựng chi tiết nên người kiểm thử phải là người biết phân tích và thiết kế hệ thống. Vì việc xác minh mô hình dựa trên việc xây dựng mô hình hệ thống nên người kiểm thử phải dành thời gian, trí tuệ và tiền bạc để xây dựng mô hình hệ thống. Như vậy SPIN có thể hiểu được mô hình hệ thống khi chúng ta sử dụng ngôn ngữ Promela để xây dựng mô hình.
Trong chương này, chúng ta sẽ tìm hiểu cách kiểm tra tự động bằng công cụ SPIN. Để làm việc với SPIN, chúng ta cần xây dựng mô hình hệ thống bằng ngôn ngữ Promela. Trong chương này, các khái niệm cơ bản sẽ lần lượt được giới thiệu. Giới thiệu về ngôn ngữ mô hình hóa Promela, công cụ SPIN và giao diện người dùng JSPIN và ISPIN.
BỘ KIỂM CHỨNG MÔ HÌNH
Chạy chế độ ngẫu nhiên để có thể tự kiểm tra lỗi trong chính chương trình Promela. Ở chế độ mô phỏng, SPIN sẽ biên dịch và chạy chương trình Promela, sau đó in trạng thái chương trình, trong luận án này tôi sử dụng công cụ JSPIN và ISPIN để xem xét trực quan kết quả xác minh. Một chương trình bao gồm nhiều trạng thái và mỗi trạng thái và mỗi trạng thái bao gồm một tập hợp các giá trị bao gồm các biến. Tính toán là một chuỗi các trạng thái ban đầu và tiếp tục với các trạng thái xảy ra khi mỗi câu lệnh được thực thi.
Một khẳng định là một cách đơn giản để kiểm tra một chương trình. Một xác nhận là một tuyên bố được đặt trong một chương trình được coi là đúng tại vị trí đó. SPIN sẽ tính toán các xác nhận trong khi tìm kiếm các phản ví dụ trong không gian trạng thái của chương trình. Trong chương trình này, chúng ta khai báo các biến, giá trị và đảo ngược, kiểu int. Biến đầu tiên được khởi tạo về giá trị ban đầu của nó. Giá trị gán cho biến nghịch đảo được tính từ giá trị của biến giá trị bằng cách chia và chia. còn lại thì giá trị của các biến đó được in ra màn hình. Câu lệnh printf được lấy từ ngôn ngữ C: một chuỗi trích dẫn kép theo sau là danh sách các biến.
Tại ISPIN, chúng tôi chạy Xác minh nên chương trình không báo cáo vi phạm nào. Logic tuyến tính tạm thời (viết tắt LTL) do Amir Pnueli, nhà khoa học người Israel đề xuất, là loại logic được ứng dụng theo thời gian, các công thức có thể xây dựng cho tương lai. Ví dụ: một điều kiện cuối cùng sẽ. LTL được xây dựng từ các biến mệnh đề AP (Atomic Proposition), toán tử logic và toán tử thời gian X,U.
Việc sử dụng các toán tử là đủ để biểu diễn các công thức trong logic mệnh đề. Công thức LTL biểu thị các thuộc tính của một chuỗi hành động (một đường dẫn, có thể gọi là dấu vết). Đầu tiên, ngữ nghĩa của công thức LTL được định nghĩa là ngôn ngữ Words(), chứa tất cả các từ vô hạn trong bảng chữ cái 2AP thỏa mãn , sau đó ngữ nghĩa được mở rộng để biểu diễn tất cả các trạng thái và chuỗi hành động của động lực dịch chuyển hệ thống.
Định nghĩa (ngữ nghĩa LTL): Cho là công thức LTL trên AP Thuộc tính logic thời gian được tạo bởi is.
THỰC NGHIỆM
Mô hình Promela mô tả hoạt động của đèn được xây dựng như sau: Mô hình Promela bao gồm hai quá trình: lamp() và switch() (tương ứng với active() và control(). Để hiểu được sự tương tác giữa công tắc và bóng đèn , hai quá trình trao đổi thông tin qua kênh ngược dòng để nhận và gửi tin nhắn cùng loại. Trong mô hình trên, giá trị của trạng thái biến là 0,1,2, tương ứng đại diện cho ba trạng thái của đèn mô tả: tắt, thấp , cao Mô hình này chạy chế độ ngẫu nhiên trong SPINta để kiểm tra lỗi của chính chương trình Promela. Mô tả trạng thái ánh sáng: off:up:low low:up:high low:down :off high:up: high high:low : thấp.
Sau khi chạy mô phỏng ở chế độ ngẫu nhiên như trên, chúng ta cần kiểm tra các thuộc tính mà hệ thống phải đáp ứng bằng cách chạy kiểm tra. Tính chất cần kiểm tra trong trường hợp này là: khi đèn ở trạng thái cao thì phải chuyển qua trạng thái thấp mới có thể trở về trạng thái tắt. Sau khi Translate dịch ngôn ngữ LTL sang Promela, chúng tôi tiến hành kiểm tra, kết quả không có vi phạm nên hệ thống đáp ứng đủ các đặc tính cần kiểm tra.
Ở model trạng thái cao, đèn có thể chuyển sang trạng thái tắt mà không qua trạng thái thấp. Tệp mô tả trạng thái của đèn là lamp. Sau khi chạy mô phỏng ở chế độ ngẫu nhiên như ở phần trên, chúng ta cần kiểm tra các thuộc tính mà hệ thống phải đáp ứng bằng cách chạy verify. Đặc tính cần kiểm chứng trong trường hợp này là: khi đèn ở trạng thái cao thì phải vượt qua trạng thái, trạng thái thấp mới có thể trở về trạng thái tắt. Vì vậy trong JSPIN chúng ta sử dụng chức năng Translate để dịch ngôn ngữ LTL sang Promela, sau đó chúng ta chạy verity, chương trình sẽ chạy chương trình Promle cho hệ thống chiếu sáng, đồng thời so sánh biểu thức LTL, kết quả cho thấy SPIN báo vi phạm, suy ra rằng mô hình được giới thiệu không đáp ứng các đặc tính cần kiểm định.
Dự án khám phá bộ xác minh mô hình SPIN, bao gồm các khái niệm về kỹ thuật xác minh và xác minh mô hình. Dự án đi sâu vào tìm hiểu hệ thống đồng thời và lập mô hình hệ thống bằng Promela, đồng thời tôi đang học cách xác minh bằng các công cụ JSPIN và ISPIN. Để kiểm nghiệm kết quả nghiên cứu trong đồ án, tôi xây dựng thí nghiệm về công tắc đèn.
Hướng nghiên cứu tiếp theo của đồ án là tiếp tục tìm hiểu và xây dựng SPIN để mô tả đặc trưng các hệ thống thời gian thực.
