peheo.baby
New Member
Link tải luận văn miễn phí cho ae Kết Nối
Luận văn ThS. Công nghệ phần mềm -- Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội, 2012
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ó hay đư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ụ
BẢNG CÁC CHỮ VIẾT TẮT ...........................................................................ii
DANH MỤC HÌNH VẼ ....................................................................................iii
Chương 1: Giới Thiệu ........................................................................................ 1
Chương 2: Một Số Khái Niệm Cơ Bản............................................................... 4
2.1 Hệ chuyển trạng thái được gán nhãn - LTS .................................... 4
2.2 Các phương pháp biểu diễn LTS .................................................... 8
2.2.1 Phương pháp liệt kê............................................................. 8
2.2.2 FSP...................................................................................... 8
2.3 Trừu tượng hóa thủ tục - PA......................................................... 10
2.4 Logic thời gian tuyến tính - LTL .................................................. 12
2.5 Đồ thị luồng điều khiển - CFG ..................................................... 14
Chương 3: Phương Pháp Kiểm Chứng ............................................................. 16
3.1 Xây dựng mô hình MImp ............................................................. 16
3.1.1 Otomat luồng điều khiển ................................................... 17
3.1.2 Otomat luồng điều khiển mở rộng ..................................... 19
3.1.3 Phương pháp trừu tượng mệnh đề...................................... 20
3.2 Kiểm chứng.................................................................................. 26
3.2.1 Phép ghép nối song song ................................................... 27
3.2.2 Kiểm chứng tính đúng đắn của chương trình ..................... 28
Chương 4: Ứng Dụng Với Công Cụ Copper..................................................... 30
4.1 Công cụ Copper ........................................................................... 30
4.2 Một số ứng dụng .......................................................................... 32
Ví dụ 4.1: ..................................................................................... 32
Ví dụ 4.2: ..................................................................................... 38
KẾT LUẬN...................................................................................................... 42
TÀI LIỆU THAM KHẢO ................................................................................ 43 3.1.1 Otomat luồng điều khiển
Việc xây dựng mô hình MImp từ mã nguồn của một chương trình C bắt đầu bằng
việc xây dựng otomat luồng điều khiển (Control Flow Automata - CFA) của
chương trình theo nguyên tắc:
Mỗi trạng thái của CFA là một điểm điều khiển (control location) trong
chương trình (tương ứng với một câu lệnh trong chương trình).
Mỗi bước chuyển trạng thái trong CFA tương ứng với một bước chuyển
giữa hai điểm điều khiển (hai câu lệnh) trong chương trình.
Định nghĩa 3.1: CFA của một chương trình C
CFA của một chương trình là một bộ gồm 4 thành phần {SCF , ICF , TCF , ℒ}
trong đó:
SCF là tập các trạng thái,
ICF ∈ SCF là trạng thái khởi tạo,
TCF ⊆ SCF × SCF là tập các chuyển đổi trạng thái,
ℒ: SCF \ {Final} Stmt là hàm gán nhãn các trạng thái của CFA.
{Final} là trạng thái kết thúc duy nhất của CFA. ℒ(ICF ) là lệnh khởi tạo
của chương trình, và s1, s2 ∈ TCF nếu và chỉ nếu một trong các điều kiện sau
đây được thõa mãn:
Nếu ℒ(s1) là lệnh gán, lệnh gọi hàm hay lệnh goto và ℒ(s2) là lệnh kế
tiếp duy nhất của nó.
Nếu ℒ(s1) là lệnh rẽ nhánh và ℒ(s2) là lệnh kế tiếp nó sau then hay else.
Nếu ℒ(s1) là lệnh return và s2 = {Final}.
Từ định nghĩa dễ thấy là CFA của một chương trình chính là CFG được gán
nhãn tại các đỉnh. Với CFA ở trên các trạng thái được gán nhãn tương ứng là S0, S1,…S9,
FINAL, trong đó S0 là trạng thái khởi tạo, FINAL là trạng thái kết thúc.
Như vậy CFA là mô hình đơn giản nhất của chương trình tuy nhiên nó chỉ
mới đặc tả được luồng điều khiển của chương trình mà chưa trừu tượng hóa
được dữ liệu các biến tại các trạng thái của chương trình. Để làm được điều này
chúng ta sử dụng đến tập các mệnh đề logic P và một phương pháp gọi là
predicate abstraction [3] để xây dựng một mô hình luồng điều khiển mở rộng.
3.1.2 Otomat luồng điều khiển mở rộng
Mô hình của chương trình được đặc tả bởi otomat luồng điều khiển mở rộng là
sự kết hợp giữa mỗi trạng thái s của CFA với một tập con của Exp thu được từ P
gọi là Ps (P thường là các điều kiện rẽ nhánh trong chương trình). Như vậy nếu
Ps
có k phần tử mỗi phần tử nhận giá trị là true hay false thì lúc đó mỗi trạng
thái trong CFA sẽ tương ứng với 2k trạng thái trong CFA mở rộng. Việc xây
dựng LTS MImp thực hiện theo các bước như sau:
1) Xây dựng CFA
2) Xây dựng một CFA mở rộng MExp = (SExp , S0Exp , ActSpec , TExp ) theo
nguyên tắc:
Với mỗi trạng thái trong CFA, chúng ta bổ sung 2k trạng thái trong SExp ,
mỗi trạng thái trong CFA mở rộng là tổ hợp trạng thái trong CFA và giá
trị của tập các mệnh đề logic đang xem xét.
Xem xét một cạnh (s1, s2) trong CFA. Lúc đó mỗi s1 và s2 sẽ tương ứng
với 2k trạng thái trong tập các trạng thái SExp . Như vậy (s1, s2) có
2k × 2k khả năng chuyển đổi trạng thái tương ứng trong TExp . Tuy nhiên
không phải tất cả các khả năng chuyển trạng thái đều thuộc TExp . Chúng
ta sẽ sử dụng công cụ chứng minh định lý (theorem prover) [4] để quyết
định xem phép chuyển đổi nào là thực sự được chấp nhận. Chúng ta cũng
sẽ chỉ loại bỏ những chuyển trạng thái nào bị loại trừ bởi kĩ thuật chứng
minh định lý.
3) MExp là mô hình chính xác hơn so với CFA. Tuy nhiên nó cũng không mô
hình hóa được hành vi của các hàm thư viện mà thủ tục proc gọi đến. Để
làm được việc đó thì chúng ta phải kết hợp các PAs giả thiết với MExp . LTS
thu được sau khi kết hợp với các PAs giả thiết chính là MImp .
Do Drive thay đổi chính sách, nên một số link cũ yêu cầu duyệt download. các bạn chỉ cần làm theo hướng dẫn.
Password giải nén nếu cần: ket-noi.com | Bấm trực tiếp vào Link để tải:
Luận văn ThS. Công nghệ phần mềm -- Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội, 2012
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ó hay đư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ụ
BẢNG CÁC CHỮ VIẾT TẮT ...........................................................................ii
DANH MỤC HÌNH VẼ ....................................................................................iii
Chương 1: Giới Thiệu ........................................................................................ 1
Chương 2: Một Số Khái Niệm Cơ Bản............................................................... 4
2.1 Hệ chuyển trạng thái được gán nhãn - LTS .................................... 4
2.2 Các phương pháp biểu diễn LTS .................................................... 8
2.2.1 Phương pháp liệt kê............................................................. 8
2.2.2 FSP...................................................................................... 8
2.3 Trừu tượng hóa thủ tục - PA......................................................... 10
2.4 Logic thời gian tuyến tính - LTL .................................................. 12
2.5 Đồ thị luồng điều khiển - CFG ..................................................... 14
Chương 3: Phương Pháp Kiểm Chứng ............................................................. 16
3.1 Xây dựng mô hình MImp ............................................................. 16
3.1.1 Otomat luồng điều khiển ................................................... 17
3.1.2 Otomat luồng điều khiển mở rộng ..................................... 19
3.1.3 Phương pháp trừu tượng mệnh đề...................................... 20
3.2 Kiểm chứng.................................................................................. 26
3.2.1 Phép ghép nối song song ................................................... 27
3.2.2 Kiểm chứng tính đúng đắn của chương trình ..................... 28
Chương 4: Ứng Dụng Với Công Cụ Copper..................................................... 30
4.1 Công cụ Copper ........................................................................... 30
4.2 Một số ứng dụng .......................................................................... 32
Ví dụ 4.1: ..................................................................................... 32
Ví dụ 4.2: ..................................................................................... 38
KẾT LUẬN...................................................................................................... 42
TÀI LIỆU THAM KHẢO ................................................................................ 43 3.1.1 Otomat luồng điều khiển
Việc xây dựng mô hình MImp từ mã nguồn của một chương trình C bắt đầu bằng
việc xây dựng otomat luồng điều khiển (Control Flow Automata - CFA) của
chương trình theo nguyên tắc:
Mỗi trạng thái của CFA là một điểm điều khiển (control location) trong
chương trình (tương ứng với một câu lệnh trong chương trình).
Mỗi bước chuyển trạng thái trong CFA tương ứng với một bước chuyển
giữa hai điểm điều khiển (hai câu lệnh) trong chương trình.
Định nghĩa 3.1: CFA của một chương trình C
CFA của một chương trình là một bộ gồm 4 thành phần {SCF , ICF , TCF , ℒ}
trong đó:
SCF là tập các trạng thái,
ICF ∈ SCF là trạng thái khởi tạo,
TCF ⊆ SCF × SCF là tập các chuyển đổi trạng thái,
ℒ: SCF \ {Final} Stmt là hàm gán nhãn các trạng thái của CFA.
{Final} là trạng thái kết thúc duy nhất của CFA. ℒ(ICF ) là lệnh khởi tạo
của chương trình, và s1, s2 ∈ TCF nếu và chỉ nếu một trong các điều kiện sau
đây được thõa mãn:
Nếu ℒ(s1) là lệnh gán, lệnh gọi hàm hay lệnh goto và ℒ(s2) là lệnh kế
tiếp duy nhất của nó.
Nếu ℒ(s1) là lệnh rẽ nhánh và ℒ(s2) là lệnh kế tiếp nó sau then hay else.
Nếu ℒ(s1) là lệnh return và s2 = {Final}.
Từ định nghĩa dễ thấy là CFA của một chương trình chính là CFG được gán
nhãn tại các đỉnh. Với CFA ở trên các trạng thái được gán nhãn tương ứng là S0, S1,…S9,
FINAL, trong đó S0 là trạng thái khởi tạo, FINAL là trạng thái kết thúc.
Như vậy CFA là mô hình đơn giản nhất của chương trình tuy nhiên nó chỉ
mới đặc tả được luồng điều khiển của chương trình mà chưa trừu tượng hóa
được dữ liệu các biến tại các trạng thái của chương trình. Để làm được điều này
chúng ta sử dụng đến tập các mệnh đề logic P và một phương pháp gọi là
predicate abstraction [3] để xây dựng một mô hình luồng điều khiển mở rộng.
3.1.2 Otomat luồng điều khiển mở rộng
Mô hình của chương trình được đặc tả bởi otomat luồng điều khiển mở rộng là
sự kết hợp giữa mỗi trạng thái s của CFA với một tập con của Exp thu được từ P
gọi là Ps (P thường là các điều kiện rẽ nhánh trong chương trình). Như vậy nếu
Ps
có k phần tử mỗi phần tử nhận giá trị là true hay false thì lúc đó mỗi trạng
thái trong CFA sẽ tương ứng với 2k trạng thái trong CFA mở rộng. Việc xây
dựng LTS MImp thực hiện theo các bước như sau:
1) Xây dựng CFA
2) Xây dựng một CFA mở rộng MExp = (SExp , S0Exp , ActSpec , TExp ) theo
nguyên tắc:
Với mỗi trạng thái trong CFA, chúng ta bổ sung 2k trạng thái trong SExp ,
mỗi trạng thái trong CFA mở rộng là tổ hợp trạng thái trong CFA và giá
trị của tập các mệnh đề logic đang xem xét.
Xem xét một cạnh (s1, s2) trong CFA. Lúc đó mỗi s1 và s2 sẽ tương ứng
với 2k trạng thái trong tập các trạng thái SExp . Như vậy (s1, s2) có
2k × 2k khả năng chuyển đổi trạng thái tương ứng trong TExp . Tuy nhiên
không phải tất cả các khả năng chuyển trạng thái đều thuộc TExp . Chúng
ta sẽ sử dụng công cụ chứng minh định lý (theorem prover) [4] để quyết
định xem phép chuyển đổi nào là thực sự được chấp nhận. Chúng ta cũng
sẽ chỉ loại bỏ những chuyển trạng thái nào bị loại trừ bởi kĩ thuật chứng
minh định lý.
3) MExp là mô hình chính xác hơn so với CFA. Tuy nhiên nó cũng không mô
hình hóa được hành vi của các hàm thư viện mà thủ tục proc gọi đến. Để
làm được việc đó thì chúng ta phải kết hợp các PAs giả thiết với MExp . LTS
thu được sau khi kết hợp với các PAs giả thiết chính là MImp .
Do Drive thay đổi chính sách, nên một số link cũ yêu cầu duyệt download. các bạn chỉ cần làm theo hướng dẫn.
Password giải nén nếu cần: ket-noi.com | Bấm trực tiếp vào Link để tải:
You must be registered for see links