Đồ án: Tìm hiểu bộ kiểm chứng mô hình spin

(6)
160 lượt xem
Share

Đồ án Tìm hiểu bộ kiểm chứng mô hình spin trình bày cơ sở lý thuyết của kiểm thử mô hình; trình bày các khái niệm về ngôn ngữ mô hình Promela, bộ kiểm chứng, các kết quả thực nghiệm của quá trình mô tả hệ thống đèn, thiết kế mô hình hệ thống đèn bằng Promela.

Mục lục nội dung

Đồ án: Tìm hiểu bộ kiểm chứng mô hình spin

1. Mở đầu

Trong lập trình muốn có được một chương trình thì người lập trình không thể thành công trong lần chạy đầu tiên và chưa thể tốt được trong lần biên dịch đầu tiên. Một chương trình ban đầu trông có vẻ hoàn hảo và luôn đúng nhưng khi đưa vào chạy thật có thể chứa những lỗi ở đâu đó,khi đó nó sẽ gây ra những thiệt hại về thời gian và tiền bạc của chùng ta rất nhiều. Trong quá trình thiết kế và sản xuất phần cứng cũng như phần mềm, chúng ta tốn rất nhiều thời gian và công sức trong việc thiết kế,đôi khi nhiều hơn cả việc xây dựng chúng. Có rất nhiều ứng dụng mà khi có lỗi dù là nhỏ nhất được đưa vào sử dụng có thể dẫn đến thiệt hại về người, tài sản cũng như tốn thật nặng nề đến môi trường. Việc thiết kế phần mềm dành cho các hệ thống này là vô cùng khó khăn. Việc một lập trình viên phải làm để có một sản phẩm phần mềm luôn là phân tích,lập trình, kiểm tra lại, kiểm thử. Để việc kiểm chứng được nhẹ nhàng và nhanh chóng, tăngsự chính xác hơn thì chúng ta luôn tìm kiếm các công nghệ để giúp cho việc đó và SPIN chính là một trong các công cụ đó.

2. Nội dung

2.1 Kiểm chứng mô hình

Kiểm chứng mô hình

Cách tiến hành

  • Các bước thực hiện của kiểm chứng mô hình
  • Ưu nhược điểm của kiểm chứng mô hình
  • Bên cạnh đó kiểm chứng mô hình cũng có những nhược điểm

2.2 Ngôn ngữ Promela

Ngôn ngữ Promela

  • Cấu trúc chương trình Promela
  • Kiểu dữ liệu cơ bản
  • Toàn tử cơ bản
  • Tên, Tên hằng số và Biểu thức
  • Tiến trình

Xử lí kênh trong Promela

  • Cú pháp
  • Kênh gửi và nhận

Các cú pháp

  • Lệnh printf
  • Lệnh lựa chọn if
  • Lệnh lặp do
  • Lệnh nhảy goto
  • Lệnh define

Run và atomic

  • run và tiến trình init
  • atomic

2.3 Bộ kiểm chứng mô hình

Bộ kiểm chứng mô hình SPIN

  • Giới thiệu về SPIN
  • Công cụ jSPIN
  • Công cụ ISPIN

Dùng SPIN để kiểm chứng

  • Giả lập ngẫu nhiên
  • Verify

Giới thiệu về LTL (Linear Temporal Logic)

  • Cú pháp
  • Ngữ nghĩa

2.4 Thực nghiệm

Mô hình máy trạng thái hữu hạn

Thực nghiệm với hệ thống đèn

  • Mô tả bài toán
  • Kiểm chứng mô hình hệ thống đèn bằng SPIN
  • Bảng chuyển Atomata

3. Kết luận

Đồ án tìm hiểu bộ kiểm chứng mô hình SPIN, trong đó các khái niệm về kiểm chứng mô hình, các kĩ thuật kiểm chứng. Đồ án đi sâu vào tìm hiểu hệ tương tranh và mô hình hóa hệ thống bằng Promela đồng thời em tìm hiểu cách kiểm chứng bằng công cụ JSPIN và ISPIN. Để thực nghiệm các kết quả nghiên cứu trong đồ án em đã xây dựng thực 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 để đặc tả các hệ thống thời gian thực.

4. Tài liệu tham khảo

Spin Model Checker The Primer and Reference Manual.

Software reliability methods.

Bài giảng môn Công Nghệ Phần Mềm của thầy Nguyễn Văn Vỵ

http://spinroot.com

Principles_of_model_checking.

Model Cheking của Edmund M Jr Clarke,Orna Grumberg,Doron A. Peled.

--- Nhấn nút TẢI VỀ hoặc XEM ONLINE để tham khảo đầy đủ nội dung Đồ án trên ---

(6)
160 lượt xem
Share
Ngày:09/09/2020 Chia sẻ bởi:Nguyễn Minh Duy
TẢI VỀ XEM ONLINE

CÓ THỂ BẠN QUAN TÂM