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

Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là một vấn đề quan trọng nhằm đảm bảo tính đúng đắn, giảm tỉ lệ lỗi, tìm khiếm khuyết, v.v. của phần mềm trước khi đưa vào sử dụng. Vấn đề này không chỉ là yếu tố quyết định thành công của các công ty phần mềm trong việc nâng cao uy tín và giảm chi phí bảo trì mà nó còn góp phần quan trọng tới sự thành công của khách hàng. Vấn đề này càng cấp thiết hơn khi phát triển các phần mềm nhúng/điều khiển. Lỗi trong phần mềm có thể gây ra thiệt hại không mong muốn cho người sử dụng phần mềm hoặc có thể ảnh hưởng nghiêm trọng tới tình hình kinh tế, chính trị, an ninh của quốc gia. Ví dụ, sự cố Therac-25 vào khoảng giữa tháng 6 năm 1985 và tháng giêng năm 1987. Nguyên nhân của sự cố này được xác định là do tương tác giữa các thành phần của hệ thống và lỗi chương trình song song khi thực hiện một chức năng quan trọng của chương trình. Sự cố này được xem như là tai nạn bức xạ tồi tệ nhất trong lịch sử 35 năm phát triển của ngành y học kể từ năm 1985. Hơn nữa, trong tương lai các tiện ích phục vụ cho con người đang dần được thay thế bởi các hệ thống nhúng/điều khiển. Nên các hệ thống này sẽ trở nên phổ biến.

Để đảm bảo chất lượng phần mềm, hầu hết các công ty hiện nay sử dụng các kỹ thuật kiểm thử trong đó chủ yếu là kỹ thuật kiểm thử hộp đen. Tuy nhiên, các kỹ thuật kiểm thử chỉ có thể phát hiện ra lỗi/khiếm khuyết chứ không chỉ ra được phần mềm không còn lỗi. Một số dự án phần mềm hiện nay yêu cầu phải chứng minh được tính đúng đắn của chương trình (đảm bảo rằng chương trình không còn lỗi) trước khi đưa vào sử dụng. Điều này có nghĩa là chỉ áp dụng phương pháp kiểm thử là chưa đủ để đảm bảo chất lượng phần mềm, đặc biệt đối với những phần mềm yêu cầu tính đúng đắn và chất lượng cao như: hệ thống điều khiển máy bay/tên lửa, hệ thống giám sát hạt nhân, v.v. Một trong những phương pháp nhằm chứng minh tính đúng đắn của chương trình đang được quan tâm nghiên cứu và áp dụng vào thực tế là kiểm chứng mô hình (model checking). Ý tưởng của phương pháp này là xây dựng mô hình của hệ thống và các thuộc tính cần kiểm tra bằng các công cụ toán học và chứng minh tự động tính đúng đắn của nó dựa trên mô hình này. Tuy nhiên, một trong những hạn chế lớn nhất của phương pháp này là vấn đề “bùng nổ không gian trạng thái” khi áp dụng vào các hệ thống có kích thước lớn. Phương pháp kiểm chứng giả định-đảm bảo (Assume-Guarantee Verification) được xem là giải pháp tiềm năng để giải quyết vấn đề trên cho các hệ thống dựa trên thành phần. Phương pháp này được xây dựng dựa trên phương pháp kiểm chứng mô hình kết hợp với kỹ thuật chia để trị nhằm mục đích chia nhỏ công việc kiểm chứng cả hệ thống thành các bài toán con để kiểm chứng các thành phần riêng biệt. Bằng cách tiếp cận này, bài toán bùng nổ không gian trạng thái hứa hẹn sẽ được giải quyết. Để áp dụng phương pháp này, chúng ta cần cài đặt công cụ hỗ trợ nhằm mục tiêu ứng dụng nó trong thực tế. Mặc dù phương pháp này được đề xuất bởi Dimitra Giannakopoulou và đã có công cụ hỗ trợ nhưng công cụ này không được công bố. Một công cụ hỗ trợ phương pháp này có tên là AGTool 1 đã được cài đặt bởi nhóm nghiên cứu. AGTool cho phép người dùng sinh ra một giả thiết kiểm chứng để kiểm tra một thành phần và cả hệ thống có thỏa mãn một thuộc tính hay không.

Các thành phần đầu vào của AGTool được biểu diễn dưới dạng một loại máy hữu hạn trạng thái (LTS) và được truyền vào AGTool bằng cách liệt kê các hàm chuyển trạng thái (trong luận văn này được gọi là dạng biểu diễn liệt kê (LF)). Cách biểu diễn này yêu cầu phải chuẩn bị các thành phần đầu vào một cách chi tiết, tốn nhiều thời gian và dễ gây ra lỗi. Bên cạnh đó, dạng biểu diễn liệt kê không được ứng dụng rộng rãi như một số ngôn ngữ mô hình hóa khác, ví dụ như FSP. Vì vậy, AGTool gặp khó khăn trong việc tương tác và sử dụng lại đặc tả của các chương trình kiểm chứng phần mềm khác như LTSA 2. Để giải quyết những vấn đề này, AGTool đã được nâng cấp lên phiên bản mới có tên gọi là GUI-AGTool 3 bởi [9, 10]. GUI-AGTool cung cấp giao diện người dùng hỗ trợ nhập liệu trực quan và dễ dàng. Bên cạnh đó, GUI-AGTool cũng có khả năng tương tác với các kiểu dữ liệu LF, FSP đơn giản. Những cải tiến này là một bước tiến quan trọng trong quá trình đưa AGTool tiếp cận với thực tế và mở ra một tiềm năng ứng dụng mới. Tuy nhiên, GUI-AGTool vẫn còn tồn tại nhiều vấn đề cần được cải tiến. GUI-AGTool cần có khả năng sử dụng được kiểu dữ liệu FSP hoàn chỉnh. Kết quả của quá trình chuyển đổi từ LF sang FSP cần được tối ưu nhiều hơn.

Mục tiêu của luận văn này là đưa GUI-AGTool trở thành một công cụ làm việc được với ngôn ngữ FSP hoàn chỉnh. Ý tưởng cơ bản của luận văn là nghiên cứu đặc tả hoàn chỉnh của FSP và tích hợp GUI-AGTool với công cụ LTSA. Những cải tiến này sẽ biến GUI-AGTool trở thành một công cụ hiệu quả và có tính tương tác rộng rãi hơn trong thực tế.

Cấu trúc của luận văn được chia thành sáu phần. Chương đầu tiên giới thiệu về vai trò của kiểm chứng phần mềm, công cụ hỗ trợ và bài toán cần giải quyết trong luận văn này. Tiếp theo, chương 2 trình bày các khái niệm cơ bản nhằm phục vụ luận văn. Chương này bao gồm các khái niệm về máy hữu hạn trạng thái, dẫn xuất, ghép nối song song, thuộc tính an toàn, đặc tả của ngôn ngữ FSP, ngôn ngữ lập trình hàm OCaml, Ocamllex và Ocamlyacc. Công cụ kiểm chứng phần mềm dựa thành phần AGTool được mô tả ở chương 3. Những vấn đề còn tồn tại của công cụ kiểm chứng AGTool được nêu ra trong chương này. Các phương pháp chuyển đổi giữa các dạng biểu diễn của LTS được trình bày trong chương 4. Trong chương này đưa ra hai phương pháp chuyển đổi qua lại giữa hai cách biểu diễn của LTS là FSP và LF. Kết quả sau khi làm thực nghiệm bằng công cụ GUI-AGTool được trình bày ở chương 5. Cuối cùng, chương 6 tóm tắt kết quả đạt được sau khi hoàn thành luận văn, những vấn đề cần khắc phục và hướng phát triển trong tương lai.

Link tải tài liệu: https://tii.la/CmVTTl3

Lưu ý: Link tải có chứa quảng cáo được rút gọn bằng Shrinkearn.com

Mật khẩu mở tệp PDF: sharetailieu.net

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

LEAVE A REPLY Cancel reply

Mới Nhất

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Nâng cao độ chính xác định vị robot bằng phương pháp tổng hợp dữ liệu cảm biến lập mã quang với bộ lọc Kalman...

Cùng Chuyên Mục

Đọc Nhiều Nhất

Áp dụng OSGi trong việc xây dựng hệ thống dựa thành...

Kiến trúc hướng dịch vụ và ứng dụng điện toán đám...

Nghiên cứu tính khả kiểm thử của ứng dụng trên nền...

Kiểm thử đơn vị cho hệ thống

Phát triền phần mềm cho người học tại Đại học Quốc...

Các kỹ thuật phân cụm trong khai phá dữ liệu sử...