Tìm kiếm
Đang tải khung tìm kiếm
Kết quả 1 đến 1 của 1

    TIẾN SĨ Nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm

    D
    dream dream Đang Ngoại tuyến (18524 tài liệu)
    .:: Cộng Tác Viên ::.
  1. Gửi tài liệu
  2. Bình luận
  3. Chia sẻ
  4. Thông tin
  5. Công cụ
  6. Nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm

    Giới thiệu
    Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là
    một vấn đề quan trọng nhằm đảm bảo tính đúng đắn, giảm tỉ lệ lỗi, tìm khiếm
    khuyết, v.v. của phần mềm trước khi đưa vào sử dụng [1]. Vấn đề này không chỉ
    là yếu tố quyết định thành công của các công ty phần mềm trong việc nâng cao
    uy tín và giảm chi phí bảo trì mà nó còn góp phần quan trọng tới sự thành công
    của khách hàng. Vấn đề này càng cấp thiết hơn khi phát triển các phần mềm
    nhúng/điều khiển. Lỗi trong phần mềm có thể gây ra thiệt hại không mong
    muốn cho người sử dụng phần mềm hoặc có thể ảnh hưởng nghiêm trọng tới
    tình hình kinh tế, chính trị, an ninh của quốc gia. Ví dụ, sự cố Therac-25 vào
    khoảng giữa tháng 6 năm 1985 và tháng giêng năm 1987. Nguyên nhân của sự
    cố này được xác định là do tương tác giữa các thành phần của hệ thống và lỗi
    chương trình song song khi thực hiện một chức năng quan trọng của chương
    trình [2, 3]. Sự cố này được xem như là tai nạn bức xạ tồi tệ nhất trong lịch sử
    35 năm phát triển của ngành y học kể từ năm 1985 [2, 3]. Hơn nữa, trong tương
    lai các tiện ích phục vụ cho con người đang dần được thay thế bởi các hệ thống
    nhúng/điều khiển. Nên các hệ thống này sẽ trở nên phổ biến.
    Để đảm bảo chất lượng phần mềm, hầu hết các công ty hiện nay sử dụng
    các kỹ thuật kiểm thử trong đó chủ yếu là kỹ thuật kiểm thử hộp đen [1]. Tuy
    nhiên, các kỹ thuật kiểm thử chỉ có thể phát hiện ra lỗi/khiếm khuyết chứ không
    chỉ ra được phần mềm không còn lỗi. Một số dự án phần mềm hiện nay yêu cầu
    phải chứng minh được tính đúng đắn của chương trình (đảm bảo rằng chương
    trình không còn lỗi) trước khi đưa vào sử dụng. Điều này có nghĩa là chỉ áp
    dụng phương pháp kiểm thử là chưa đủ để đảm bảo chất lượng phần mềm,
    đặc biệt đối với những phần mềm yêu cầu tính đúng đắn và chất lượng cao
    như: hệ thống điều khiển máy bay/tên lửa, hệ thống giám sát hạt nhân, v.v.
    Một trong những phương pháp nhằm chứng minh tính đúng đắn của chương
    trình đang được quan tâm nghiên cứu và áp dụng vào thực tế là kiểm chứng mô
    1Chương 1. Giới thiệu
    hình (model checking) [4]. Ý tưởng của phương pháp này là xây dựng mô hình
    của hệ thống và các thuộc tính cần kiểm tra bằng các công cụ toán học và chứng
    minh tự động tính đúng đắn của nó dựa trên mô hình này. Tuy nhiên, một trong
    những hạn chế lớn nhất của phương pháp này là vấn đề "bùng nổ không gian
    trạng thái" khi áp dụng vào các hệ thống có kích thước lớn [4]. Phương pháp
    kiểm chứng giả định-đảm bảo (Assume-Guarantee Verification) [5] được xem là
    giải pháp tiềm năng để giải quyết vấn đề trên cho các hệ thống dựa trên thành
    phần. Phương pháp này được xây dựng dựa trên phương pháp kiểm chứng mô
    hình kết hợp với kỹ thuật chia để trị nhằm mục đích chia nhỏ công việc kiểm
    chứng cả hệ thống thành các bài toán con để kiểm chứng các thành phần riêng
    biệt. Bằng cách tiếp cận này, bài toán bùng nổ không gian trạng thái hứa hẹn
    sẽ được giải quyết. Để áp dụng phương pháp này, chúng ta cần cài đặt công cụ
    hỗ trợ nhằm mục tiêu ứng dụng nó trong thực tế. Mặc dù phương pháp này
    được đề xuất bởi Dimitra Giannakopoulou [5] và đã có công cụ hỗ trợ [6] nhưng
    công cụ này không được công bố. Một công cụ hỗ trợ phương pháp này có tên
    là AGTool 1 đã được cài đặt bởi nhóm nghiên cứu [7]. AGTool cho phép người
    dùng sinh ra một giả thiết kiểm chứng để kiểm tra một thành phần và cả hệ
    thống có thỏa mãn một thuộc tính hay không.
    Các thành phần đầu vào của AGTool được biểu diễn dưới dạng một loại
    máy hữu hạn trạng thái (LTS) và được truyền vào AGTool bằng cách liệt kê các
    hàm chuyển trạng thái (trong luận văn này được gọi là dạng biểu diễn liệt kê (LF)).
    Cách biểu diễn này yêu cầu phải chuẩn bị các thành phần đầu vào một cách chi
    tiết, tốn nhiều thời gian và dễ gây ra lỗi. Bên cạnh đó, dạng biểu diễn liệt kê
    không được ứng dụng rộng rãi như một số ngôn ngữ mô hình hóa khác, ví dụ
    như FSP. Vì vậy, AGTool gặp khó khăn trong việc tương tác và sử dụng lại đặc
    tả của các chương trình kiểm chứng phần mềm khác như LTSA 2 [8]. Để giải
    quyết những vấn đề này, AGTool đã được nâng cấp lên phiên bản mới có tên gọi
    là GUI-AGTool 3 bởi [9, 10]. GUI-AGTool cung cấp giao diện người dùng hỗ trợ
    nhập liệu trực quan và dễ dàng. Bên cạnh đó, GUI-AGTool cũng có khả năng
    tương tác với các kiểu dữ liệu LF, FSP đơn giản. Những cải tiến này là một bước
    tiến quan trọng trong quá trình đưa AGTool tiếp cận với thực tế và mở ra một
    tiềm năng ứng dụng mới. Tuy nhiên, GUI-AGTool vẫn còn tồn tại nhiều vấn đề
    cần được cải tiến. GUI-AGTool cần có khả năng sử dụng được kiểu dữ liệu FSP
    hoàn chỉnh. Kết quả của quá trình chuyển đổi từ LF sang FSP cần được tối ưu
    nhiều hơn.
    Mục tiêu của luận văn này là đưa GUI-AGTool trở thành một công cụ làm
    việc được với ngôn ngữ FSP hoàn chỉnh. Ý tưởng cơ bản của luận văn là nghiên
    1
    http://uet.vnu.edu.vn/~hungpn/AGTools/
    2
    http://www.doc.ic.ac.uk/ltsa/
    3
    http://uet.vnu.edu.vn/~hungpn/GUI-AGTool/
    2Chương 1. Giới thiệu
    cứu đặc tả hoàn chỉnh của FSP và tích hợp GUI-AGTool với công cụ LTSA.
    Những cải tiến này sẽ biến GUI-AGTool trở thành một công cụ hiệu quả và có
    tính tương tác rộng rãi hơn trong thực tế.
    Cấu trúc của luận văn được chia thành sáu phần. Chương đầu tiên giới
    thiệu về vai trò của kiểm chứng phần mềm, công cụ hỗ trợ và bài toán cần giải
    quyết trong luận văn này. Tiếp theo, chương 2 trình bày các khái niệm cơ bản
    nhằm phục vụ luận văn. Chương này bao gồm các khái niệm về máy hữu hạn
    trạng thái, dẫn xuất, ghép nối song song, thuộc tính an toàn, đặc tả của ngôn ngữ
    FSP, ngôn ngữ lập trình hàm OCaml, Ocamllex và Ocamlyacc. Công cụ kiểm
    chứng phần mềm dựa thành phần AGTool được mô tả ở chương 3. Những vấn
    đề còn tồn tại của công cụ kiểm chứng AGTool được nêu ra trong chương này.
    Các phương pháp chuyển đổi giữa các dạng biểu diễn của LTS được trình bày
    trong chương 4. Trong chương này đưa ra hai phương pháp chuyển đổi qua lại
    giữa hai cách biểu diễn của LTS là FSP và LF. Kết quả sau khi làm thực nghiệm
    bằng công cụ GUI-AGTool được trình bày ở chương 5. Cuối cùng, chương 6 tóm
    tắt kết quả đạt được sau khi hoàn thành luận văn, những vấn đề cần khắc phục
    và hướng phát triển trong tương lai.






    Mục lục
    1 Giới thiệu 1
    2 Kiến thức cơ bản 4
    2.1 Labeled Transition System (LTS) . 4
    2.2 Các phương pháp biểu diễn LTS . 5
    2.2.1 Phương pháp liệt kê 6
    2.2.2 FSP 6
    2.3 Dẫn xuất . 7
    2.4 Ghép nối song song . 7
    2.5 LTS an toàn và thuộc tính an toàn . 8
    2.6 Tính thỏa mãn 9
    2.7 Đặc tả ngôn ngữ FSP 9
    2.7.1 Định nghĩa FSP . 10
    2.7.2 Các định danh 10
    2.7.3 Nhãn hành động 11
    2.7.4 Const, Range, Set 12
    2.7.5 Định nghĩa tiến trình 12
    2.7.6 Tiến trình kết hợp 13
    2.7.7 Tham số . 14
    2.7.8 Phép gán lại nhãn và phép ẩn . 15
    2.7.9 Property, Progress và Menu 16
    2.7.10 Biểu thức . 16
    viiMỤC LỤC
    2.8 Ngôn ngữ lập trình hàm OCaml . 17
    2.8.1 Đặc trưng của OCaml . 17
    2.8.2 Cú pháp và ngữ nghĩa . 18
    2.9 OCamllex và OCamlyacc 23
    2.9.1 OCamllex 23
    2.9.2 OCamlyacc . 23
    3 AGTool 25
    3.1 Giới thiệu AGTool 25
    3.2 Hạn chế của AGTool 27
    4 Chuyển đổi giữa các dạng biểu diễn của LTS 28
    4.1 Chuyển đổi FSP sang LF 29
    4.1.1 Ý tưởng . 29
    4.1.2 Thiết kế . 32
    4.1.3 Phân tích đánh giá . 32
    4.2 Chuyển đổi LF sang FSP 33
    4.2.1 Ý tưởng . 33
    4.2.2 Phân tích đánh giá . 36
    5 Thực nghiệm 37
    5.1 Cài đặt chương trình 37
    5.2 Giới thiệu về chương trình . 37
    5.3 Thực nghiệm . 39
    5.4 Đánh giá thực nghiệm . 43
    6 Kết luận 44
    Tài liệu tham khảo 46
    viiiDanh sách hình vẽ
    2.1 Ví dụ của LTS . 5
    2.2 Phương pháp biểu diễn liệt kê của LTS 6
    2.3 Ví dụ của LF 6
    2.4 Ví dụ của FSP . 7
    2.5 Ghép nối song song giữa INPUT và OUTPUT 8
    2.6 Biểu diễn LTS của thuộc tính an toàn Safety Property 9
    2.7 Ví dụ định nghĩa hằng số 9
    2.8 Ví dụ định nghĩa danh sách đối số . 10
    2.9 Định nghĩa FSP 10
    2.10 Định nghĩa các định danh 11
    2.11 Định nghĩa các chữ hoa, thường 11
    2.12 Định nghĩa nhãn hành động 11
    2.13 Định nghĩa tập các nhãn hành động 12
    2.14 Định nghĩa Const, Range, Set 12
    2.15 Định nghĩa tiến trình . 13
    2.16 Định nghĩa tiến trình địa phương . 14
    2.17 Định nghĩa thành phần tuần tự . 15
    2.18 Định nghĩa thành phần tuần tự . 15
    2.19 Định nghĩa tham số . 16
    2.20 Định nghĩa phép gán lại nhãn . 16
    2.21 Định nghĩa phép ẩn . 17
    2.22 Định nghĩa Property . 17
    2.23 Định nghĩa Progress . 18
    ixDANH SÁCH HÌNH VẼ
    2.24 Định nghĩa Menu . 18
    2.25 Định nghĩa biểu thức . 19
    2.26 Định nghĩa biểu thức (tiếp) . 20
    2.27 Định nghĩa biểu thức (tiếp) . 21
    2.28 Ví dụ khai báo hàm 21
    2.29 Ví dụ gọi hàm . 21
    2.30 Ví dụ hàm mức cao 22
    2.31 Ví dụ hàm nặc danh . 22
    2.32 Ví dụ hàm đệ quy . 22
    2.33 Cấu trúc lệnh của so sánh mẫu . 22
    2.34 Ví dụ so sánh mẫu 22
    2.35 Cấu trúc tập tin đặc tả từ vựng . 23
    2.36 Ví dụ tập tin đặc tả từ vựng . 24
    2.37 Cấu trúc tập tin đặc tả cú pháp . 24
    3.1 Mô hình công cụ kiểm chứng AGTool . 25
    3.2 Thành phần đầu vào của AGTool 26
    3.3 Kết quả được sinh ra bởi AGTool 26
    4.1 Kiến trúc của GUI-AGTool 28
    4.2 Cấu trúc thành phần chuyển đổi từ FSP sang LF . 29
    4.3 FSP M . 29
    4.4 Mô hình FSP Compiler 32
    4.5 Cấu trúc thành phần chuyển đổi từ LF sang FSP . 33
    5.1 Giao diện chính của GUI-AGTool 38
    5.2 Giao diện thể hiện giả định sinh ra bởi GUI-AGTool . 39
    5.3 Ví dụ FSP đầu vào của AGTool . 40
    5.4 LTS của thành phần M1 . 41
    5.5 LTS của thành phần M2 . 41
    5.6 LTS của thành phần P 41
    x

    Xem Thêm: Nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm
    Nội dung trên chỉ thể hiện một phần hoặc nhiều phần trích dẫn. Để có thể xem đầy đủ, chi tiết và đúng định dạng tài liệu, bạn vui lòng tải tài liệu. Hy vọng tài liệu Nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm sẽ giúp ích cho bạn.
    #1
  7. Đang tải dữ liệu...

    Chia sẻ link hay nhận ngay tiền thưởng
    Vui lòng Tải xuống để xem tài liệu đầy đủ.

    Gửi bình luận

    ♥ Tải tài liệu

social Thư Viện Tài Liệu
Tài liệu mới

Từ khóa được tìm kiếm

Nobody landed on this page from a search engine, yet!

Quyền viết bài

  • Bạn Không thể gửi Chủ đề mới
  • Bạn Không thể Gửi trả lời
  • Bạn Không thể Gửi file đính kèm
  • Bạn Không thể Sửa bài viết của mình
  •  
DMCA.com Protection Status