Kiểm chứng từng phần cho chương trình C
Trình bày cơ sở lý luận về kiểm chứng. Trình bày các khái niệm cơ bản liên quan như các khái niệm về mô hình chuyển trạng thái được gán nhãn Hệ chuyển trạng thái gán nhãn (LTS), các phương pháp biểu diễn LTS, khái niệm về trừu tượng hóa hành vi của hệ thống Trìu tượng hóa thủ tục (PA), cũng nh...
Lưu vào:
| Tác giả chính: | , |
|---|---|
| Định dạng: | Luận án |
| Ngôn ngữ: | other |
| Thông tin xuất bản: |
Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội
2016
|
| Chủ đề: | |
| Truy cập trực tuyến: | http://repository.vnu.edu.vn/handle/VNU_123/6461 |
| Từ khóa: |
Thêm từ khóa bạn đọc
Không có từ khóa, Hãy là người đầu tiên gắn từ khóa cho biểu ghi này!
|
| id |
oai:112.137.131.14:VNU_123-6461 |
|---|---|
| record_format |
dspace |
| spelling |
oai:112.137.131.14:VNU_123-64612016-04-04T20:17:25Z Kiểm chứng từng phần cho chương trình C Hoàng, Mạnh Khôi Nguyễn, Việt Hà Công nghệ phần mềm Kiểm chứng mô hình Mã nguồn C Trình bày cơ sở lý luận về kiểm chứng. Trình bày các khái niệm cơ bản liên quan như các khái niệm về mô hình chuyển trạng thái được gán nhãn Hệ chuyển trạng thái gán nhãn (LTS), các phương pháp biểu diễn LTS, khái niệm về trừu tượng hóa hành vi của hệ thống Trìu tượng hóa thủ tục (PA), cũng như các khái niệm cần thiết trong kĩ thuật kiểm chứng … Trình bày nội dung chính c ủa Kiểm thử từng phần cho chương trình C: nêu cách xây dựng mô hình LTS biểu diễn hành vi của hệ thống từ mã nguồn bắt đầu bằng việc xây dựng sơ đồ luồng xử lý Otomat luồng điều khiển (CFA); sơ đồ luồng xử lý mở rộng (Expanding Control flow Automata) của c hương trình có sử dụng các LTS giả thiết; giới thiệu phương pháp trừu tượng mệnh đề để xây dựng được mô hình LTS biểu diễn hành vi của mã nguồn từ sơ đồ luồng xử lý mở rộng; nêu cách kiểm chứng mô hình LTS của phần cài đặt có đảm bảo với mô hình LTS của đặ c tả. Đưa ra ứng dụng của phương pháp bằng cách giới thiệu các công cụ Copper. Đầu vào của công cụ này là tập file mã nguồn C của chương trình và các đặc tả của các thuộc tính cần kiểm chứng, đầu ra là kết luận phần cài đặt đã đúng với đặc tả của nó hoặc đưa ra phản ví dụ chứng minh cài đặt không đúng với đặc tả. Giới thiệu một vài ứng dụng đơn giản được áp dụng thực tế trên công cụ bằng cách nêu chi tiết cách xây dựng các file đặc tả cũng như cách xây dựng các PA giả thiết bằng ví dụ. 2016-04-04T08:03:17Z 2016-04-04T08:03:17Z 2012 Thesis 17 tr. http://repository.vnu.edu.vn/handle/VNU_123/6461 other application/pdf Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội |
| institution |
Đại học Quốc Gia Hà Nội |
| collection |
DSpace |
| language |
other |
| topic |
Công nghệ phần mềm Kiểm chứng mô hình Mã nguồn C |
| spellingShingle |
Công nghệ phần mềm Kiểm chứng mô hình Mã nguồn C Hoàng, Mạnh Khôi Nguyễn, Việt Hà Kiểm chứng từng phần cho chương trình C |
| description |
Trình bày cơ sở lý luận về kiểm chứng. Trình bày các khái niệm cơ bản liên
quan như các khái niệm về mô hình chuyển trạng thái được gán nhãn Hệ chuyển trạng
thái gán nhãn (LTS), các phương pháp biểu diễn LTS, khái niệm về trừu tượng hóa
hành vi của hệ thống Trìu tượng hóa thủ tục (PA), cũng như các khái niệm cần thiết
trong kĩ thuật kiểm chứng … Trình bày nội dung chính c ủa Kiểm thử từng phần cho
chương trình C: nêu cách xây dựng mô hình LTS biểu diễn hành vi của hệ thống từ mã
nguồn bắt đầu bằng việc xây dựng sơ đồ luồng xử lý Otomat luồng điều khiển (CFA);
sơ đồ luồng xử lý mở rộng (Expanding Control flow Automata) của c hương trình có
sử dụng các LTS giả thiết; giới thiệu phương pháp trừu tượng mệnh đề để xây dựng
được mô hình LTS biểu diễn hành vi của mã nguồn từ sơ đồ luồng xử lý mở rộng; nêu
cách kiểm chứng mô hình LTS của phần cài đặt có đảm bảo với mô hình LTS của đặ c
tả. Đưa ra ứng dụng của phương pháp bằng cách giới thiệu các công cụ Copper. Đầu
vào của công cụ này là tập file mã nguồn C của chương trình và các đặc tả của các
thuộc tính cần kiểm chứng, đầu ra là kết luận phần cài đặt đã đúng với đặc tả của nó
hoặc đưa ra phản ví dụ chứng minh cài đặt không đúng với đặc tả. Giới thiệu một vài
ứng dụng đơn giản được áp dụng thực tế trên công cụ bằng cách nêu chi tiết cách xây
dựng các file đặc tả cũng như cách xây dựng các PA giả thiết bằng ví dụ. |
| format |
Thesis |
| author |
Hoàng, Mạnh Khôi Nguyễn, Việt Hà |
| author_facet |
Hoàng, Mạnh Khôi Nguyễn, Việt Hà |
| author_sort |
Hoàng, Mạnh Khôi |
| title |
Kiểm chứng từng phần cho chương trình C |
| title_short |
Kiểm chứng từng phần cho chương trình C |
| title_full |
Kiểm chứng từng phần cho chương trình C |
| title_fullStr |
Kiểm chứng từng phần cho chương trình C |
| title_full_unstemmed |
Kiểm chứng từng phần cho chương trình C |
| title_sort |
kiểm chứng từng phần cho chương trình c |
| publisher |
Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội |
| publishDate |
2016 |
| url |
http://repository.vnu.edu.vn/handle/VNU_123/6461 |
| work_keys_str_mv |
AT hoangmanhkhoi kiemchungtungphanchochuongtrinhc AT nguyenvietha kiemchungtungphanchochuongtrinhc |
| _version_ |
1768572954083328000 |