Báo cáo 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ư 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ội dung trích xuất từ tài liệu:
Báo cáo " Kiểm chứng từng phần cho chương trình C " Kiểm chứng từng phần cho chương trình C Hoàng Mạnh Khôi Trường Đại học Công nghệ Luận văn Thạc sĩ ngành: Công nghệ phần mềm; Mã số: 60 48 10 Người hướng dẫn: PGS.TS Nguyễn Việt Hà Năm bảo vệ: 2012 Abstract: 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 chươ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ụ. Keywords: Công nghệ phần mềm; Kiểm chứng mô hình; Mã nguồn CContent Chương 1: Giới thiệuĐảm bảo chất lượng phần mềm là một trong những giai đoạn quan trọng bậc nhất trong quytrình phát triển phần mềm. Có rất nhiều phương pháp được sử dụng trong việc đảm bảo chấtlượng phần mềm, trong đó kiểm chứng mô hình [6] là một trong những cách tiếp cận hiệu quảnhất, và ngày càng được sử dụng rộng rãi, đặc biệt là trong các hệ thống phần mềm đòi hỏi độchính xác cao. Kiểm chứng mô hình là một nhóm các kĩ thuật kiểm định tự động một mô hình với cácđặc tả tính năng của mô hình đó. Mô hình là một hệ thống bao gồm tập hợp có giới hạn cáctrạng thái và tập hợp các bước chuyển tiếp giữa các trạng thái đó. Kiểm chứng mô hình là xácminh tính đúng đắn của mô hình bằng cách xác định xem thuộc tính mà người dùng mongmuốn có được thõa mãn bởi mô hình đó hay không [6]. Trong kiểm chứng mô hình phần mềm có hai bài toán được quan tâm chính đó là kiểmchứng đặc tả và kiểm chứng mã nguồn. Bài toán kiểm chứng tự động mã nguồn được xem làứng dụng đầu tiên của kiểm chứng mô hình trong việc đảm bảo chất lượng phần mềm. Dù đãcó từ lâu nhưng đến nay nó vẫn là vấn đề mở và chưa có giải pháp thỏa đáng, cho nên nó vẫnđang nhận được sự quan tâm rộng rãi. Như chúng ta đã biết một chương trình C có mã nguồn lớn, sẽ tồn tại nhiều lời gọihàm hay nhiều lời gọi đến các thư viện hàm. Việc kiểm chứng theo mô hình một chương trìnhnhư vậy sẽ gặp khó khăn và phức tạp vì hoặc có thể chúng ta chưa có được đầy đủ mã nguồncủa các thư viện hàm hoặc dễ gây ra bùng nổ không gian trạng thái. Trong luận văn này tôixin giới thiệu một phương pháp mới trong kiểm chứng tự động để kiểm chứng một cài đặt củachương trình C có mã nguồn lớn và có nhiều thành phần. Cách tiếp cận của phương pháp là chúng ta đưa việc kiểm chứng một chương trìnhphần mềm lớn về việc kiểm chứng các thành phần con nhỏ hơn và đơn giản hơn bằng cáchtrừu tượng hóa hành vi [3] (procedure abtraction-PA) của các thành phần con (hay các hàmthư viện) theo một khái niệm đặc tả của máy hữu hạn trạng thái đó là hệ thống chuyển trạngthái được gán nhãn LTS (Label Transition System) [4]. Phương pháp cho phép chúng ta tựđịnh nghĩa các hành vi của các hàm thư viện (chưa có mã nguồn hoặc chưa rõ hành vi) và sửdụng chúng như là giả thiết trong quá trình xây dựng mô hình kiểm chứng. Nội dung chính của luận văn là giới thiệu phương pháp kiểm chứng phần cài đặt củamột hệ thống viết bằng ngôn ngữ C có đảm bảo đúng với đặc tả của nó, để làm được điều đótrước hết từ mã nguồn C chúng ta phải xây dựng được mô hình LTS biểu diễn hành vi của hệthống, sau đó sử dụng kĩ thuật kiểm chứng để thẩm định xem nó có đảm bảo đúng với môhình LTS của đặc tả hay không. Nội dung của luận văn được trình bày trong 4 chương: Chương 1 giới thiệu về đề tài, trình bày tổng quan về nội dung phương pháp đượcnghiên trong đề tài, mục tiêu của đề tài và cấu trúc của luận văn. Chương 2 trình bày các khái niệm cơ bản phục vụ cho đề tài, chương này đưa ra cáckhái niệm về mô hình chuyển trạng thái được gán nhãn LTS, khái niệm về trừu tượng hóahành vi của hệ thống PA, cũng như các khái niệm cần thiết trong kĩ thuật kiểm chứng … Chương 3 trình bày nội dung chính của luận văn, đó là nêu cách xây dựng mô hìnhLTS 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ý CFA (Control Flow Automata) [3] và sơ đồ luồng xử lý mở rộng (Expanding Control flowAutomata) [3] của chương trình có sử dụng các LTS giả thiết. Nêu cách kiểm chứng mô hìnhLTS của phần cài đặt có đảm bảo với mô hình LTS của đặc tả. Chương 4 luận văn đưa ra ứng dụng thực tế của phương pháp bằng cách giới thiệu cáccông cụ Copper [2]. Đầ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 2đặ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 đ ...