BỘ GIÁO DỤC VÀ ĐÀO TẠO
TRƯỜNG ĐẠI HỌC BÁCH KHOA HÀ NỘI
──────── * ───────
NGUYỄN ĐỨC CƯỜNG
NGHIÊN CỨU VỀ SEPARATION LOGIC VÀ ỨNG DỤNG
VÀO HỆ THỐNG KIỂM ĐỊNH TỰ ĐỘNG
LUẬN VĂN THẠC SĨ KỸ THUẬT
CÔNG NGHỆ THÔNG TIN
NGƯỜI HƯỚNG DẪN KHOA HỌC:
TS. TRẦN ĐỨC KHÁNH
HÀ NỘI -2014
LỜI CAM ĐOAN
Tôi xin cam đoan đề tài nghiên cứu của tôi hoàn toàn do tôi tự làm dưới sự
hướng dẫn của Thầy giáo TS. Trần Đức Khánh. Những kết quả nghiên cứu, thử
nghiệm được thực hiện trên các phần mềm mô phỏng. Các số liệu, kết quả trình bày
trong luận văn là hoàn toàn trung thực và chưa từng được công bố trong bất cứ công
trình nào.
Các tài liệu tham khảo sử dụng trong luận văn đều được dẫn nguồn.
Nếu xảy ra bất cứ điều không đúng như những lời cam đoan trên, tôi xin chịu
hoàn toàn trách nhiệm trước Viện và Nhà trường.
Hà Nội, ngày
tháng 3 năm 2014
Tôi rất mong nhận được ý kiến đóng góp của các thầy, cô giáo và các bạn.
Hà Nội, ngày 20 tháng 03 năm 2014.
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang3
MỤC LỤC
LỜI CAM ĐOAN .................................................................................................... 2
MỤC LỤC .............................................................................................................. 4
DANH MỤC BẢNG BIỂU ..................................................................................... 8
DANH MỤC HÌNH VẼ .......................................................................................... 9
DANH MỤC THUẬT NGỮ SỬ DỤNG ............................................................... 10
TÓM TẮT NỘI DUNG LUẬN VĂN TỐT NGHIỆP ............................................ 11
1.Lý do chọn đề tài ................................................................................................ 11
2.Lịch sử tìm hiểu .................................................................................................. 12
3.Mục đích tìm hiểu, đối tượng, phạm vi của luận văn ........................................... 13
3.1Mục đích tìm hiểu ............................................................................................. 13
3.2Đối tượng tìm hiểu............................................................................................ 14
3.3 Phạm vi tìm hiểu .............................................................................................. 14
4.Các luận điểm cơ bản và đóng góp của luận văn ................................................. 15
4.1 Các luận điểm cơ bản....................................................................................... 15
4.2 Đóng góp mới của luận văn ............................................................................. 15
5.Phương pháp tìm hiểu ......................................................................................... 15
6.Cấu trúc của luận văn ......................................................................................... 16
CHƯƠNG 1.TỔNG QUAN .................................................................................. 17
1.1 Hoare Logic và kiểm định phần mềm .............................................................. 17
1.2 Separation Logic và kiểm định phần mềm ....................................................... 18
2.5.1 Quy tắc Matching up Heap Node .................................................................. 55
2.5.2 Quy tắc Unfold vị từ Shape trong Atendence ................................................ 55
2.5.3 Quy tắc Fold vị từ Shape trong Consequence ................................................ 56
2.6 Tính đúng đắn của quy tắc suy diễn ................................................................. 57
2.6.1 Mô hình ngữ nghĩa........................................................................................ 58
2.6.2 Tính đúng đắn của quy tắc Verification ........................................................ 59
Định lý 1 (Preservation) ........................................................................................ 60
Định lý 2 (Progress) .............................................................................................. 60
Định lý 3 (Safety) .................................................................................................. 60
2.6.3Tính đúng đắn của quy tắc Entailment ........................................................... 61
Định lý 1 (Soundness) ........................................................................................... 61
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang5
Định lý 2(Termination) .......................................................................................... 61
2.7 Kết luận chương .............................................................................................. 61
CHƯƠNG3. CÀI ĐẶT THỬ NGHIỆM CÔNG CỤ KIỂM ĐỊNH TỰ ĐỘNG ỨNG
DỤNG SEPARATION LOGIC ............................................................................. 62
3.1 Phương hướng cài đặt thử nghiệm công cụ kiểm định tự động ứng dụng
Separation logic ..................................................................................................... 62
3.2 Kiến trúc của HIP/SLEEK ............................................................................... 63
3.3 Hoạt động của HIP/SLEEK ............................................................................. 64
3.3.1 File đầu vào .................................................................................................. 64
3.3.2 Kiểu dữ liệu cơ bản....................................................................................... 65
3.3.3 Cấu trúc dữ liệu ............................................................................................ 65
3.3.4 Định dạng công thức khẳng định .................................................................. 65
3.3.5 Một vài tính năng đặc biệt khác .................................................................... 66
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang7
DANH MỤC BẢNG BIỂU
Bảng 1 - Toán tử Separation Logic ........................................................................ 35
Bảng 2 - Truy xuất trên vùng nhớ Heap ................................................................. 36
Bảng 3 - Ý nghĩa ký hiệu sử dụng trong ngôn ngữ chương trình ............................ 38
Bảng 4 - Ký hiệu định nghĩa mô hình .................................................................... 58
Bảng 5 - Ký hiệu ngữ nghĩa ................................................................................... 59
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang8
DANH MỤC HÌNH VẼ
Hình 1 - Toán hạng cơ bản logic mệnh đề.............................................................. 23
Hình 2 - Ngôn ngữ chương trình ............................................................................ 37
Hình 3 - Ngôn ngữ đặc tả ...................................................................................... 41
Hình 4 - Các quy tắc kiểm tra suy diễn .................................................................. 54
Hình 5 - Tổng quan kiến trúc HIP/SLEEK............................................................. 63
Hình 6 – Kết quả kiểm định đặc tả cấu trúc dữ danh sách nối kép.......................... 73
Hình 7 – Cấu trúc dữ liệu cây ................................................................................ 74
Hình 8 – Kết quả kiểm định đặc tả cấu trúc dữ liệu cây ......................................... 78
Hình 9 – Cấu trúc dữ liệu hàng .............................................................................. 79
Hình 10 - Kết quả kiểm định đặc tả cấu trúc dữ liệu hàng ...................................... 86
Logic đề xuất bởi Brouwer tương tự như Logic
bậc nhất
Intuitionistic
Linear Logic
Logic được đề xuất bởi Girard
BI
Logic Bunch
BI được đề xuất bởi O'Hearn and Pym
Program
Chương trình
Forward
verification
Quy tắc suy diễn biến đổi
Entailment
checking
Quy tắc kiểm tra suy diễn
Wellformedness
Pure part
Phần công thức thuần túy không chứa suy diễn
Heap
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang10
TÓM TẮT NỘI DUNG LUẬN VĂN TỐT NGHIỆP
1.Lý do chọn đề tài
Ngày nay, tự động hóa được ứng dụng ở rất nhiều lĩnh vực, mục đích thường
rất đa dạng và tùy theo nhu cầu đặc thù của từng lĩnh vực, tuy nhiên điểm chung
nhất vẫn là giảm nhân lực, thời gian và sai sót. Ngành công nghệ thông tin mà cụ
thể là phát triển phần mềm cũng không ngoại lệ. Như chúng ta biết, để tạo ra sản
phẩmcông nghệ thông tinhayphần mềm có chất lượng thì hoạt động kiểm thử phần
mềm đóng vai trò rất quan trọng, trong khi đó hoạt động này lại tiêu tốn và chiếm tỷ
trọng khá lớn công sức và thời gian trong một dự án. Tuy nhiên, việc kiểm thử
chương trình là chưa đủ vì các phương pháp kiểm thử hiện tại chỉ là kiểm tra dữ
liệu đầu ra của phần mềm rồi so sánh với dữ liệu đầu vào để kiểm tra xem chương
trình chạy có lỗi hay không. Chúng ta không hề kiểm tra được chi tiết hoạt động của
chương trình và không kiểm soát được những lỗi tiềm ẩn ngay cả khi chương trình
vẫn chạy đúng. Nếu phần mềm phát hành ra mà vẫn còn chứa lỗi thì nhà sản xuất
phải thu hồi sản phẩm để sửa chữa. Điều này làm giảm uy tín và tiêu tốn nhiều tiền
của nhà sản xuất, mặt khác trong một số trường hợp còn gây nguy hại vô cùng lớn
đặc biệt trong những phần mềm điều khiển yêu cầu tính chính xác cao, chỉ một sai
sót nhỏ cũng có thể dẫn tới phá hủy toàn hệ thống. Chúng ta hoàn toàn có thể khắc
phục được những vấn đề trên bằng cách sử dụng các phương pháp kiểm định phần
trình để áp dụng các công cụ kiểm định chưa mô tả đầy đủ, toàn vẹn được các thuộc
tính, phương thức của chương trình.
Đó là lý tôi chọn đề tài “Nghiên cứu về Separation Logic và ứng dụng vào
hệ thống kiểm định tự động” làm luận văn tốt nghiệp.
2.Lịch sử tìm hiểu
Dạng thức logic đầu tiên được ứng dụng vào xây dựng công cụ kiểm định tự
động được đưa ra bởi Floyd và Hoare, với đặc trưng bộ ba Hoare p{c}q, mô tả
trạng thái của chương trình thay đổi từ p sang q sau khi thực hiện lệnh c. Tuy nhiên,
khi áp dụng bộ ba Hoare đặc tả chương trình thao tác trên dữ liệu có cấu trúc phức
tạp thì tính đúng đắn của chương trình không được đảm bảo, nhất là với các chương
trình khai thác con trỏ dữ liệu đòi hỏi khai thác bộ nhớ bên ngoài Stack, như là bộ
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang12
nhớ Heap; hoặc những chương trình đòi hỏi việc chia sẻ bộ nhớ dữ liệu hay tính
toán song song.
Để giải quyết vấn đề này, O’Hearn và Reynolds đã xây dựng lên Separation
logic, một dạng thức mở rộng của Hoare Logic thực hiện việc suy diễn về thao tác
trên cấu trúc dữ liệu chia sẻ(có thể tham chiếu bởi nhiều hơn một con trỏ).
Separation Logic được xây dựng với mong muốn mô tả những trạng thái của
chương trình.Một khẳng định Separation Logic sẽ mô tả trạng thái được lưu trữ
trong Stack và Heap, từ đó xây dựng nên các lý thuyết suy diễn có thể áp dụng
chứng minh tính đúng đắn của chương trình chính xác và ngắn gọn.Separation
Logic được ứng dụng trong lĩnh vực chứng minh tính dừng chương trình, tranh chấp
dữ liệu, kiểm định chương trình có cấu trúc, kiểm định các mã nguồn ở mức thấp
của chương trình (mức thư viện, hệ điều hành, hệ nhúng, tính toán song song…).
Tiếp thu các thành tựu của các nhà khoa học đi trước, chúng tôi cố gắng tìm
Với mong muốn làm nổi bật ứng dụng của Separation Logic trong lĩnh vực
kiểm định phần mềm tự động, luận văn đi sâu vào tìm hiểu kỹ thuật đặc tả chương
trình ứng dụng Separation Logic ngắn gọn, chính xác sử dụng trong xây dựng các
công cụ kiểm định phần mềm đầy đủ, toàn vẹn hơn.
Ngoài ra luận văn còn tìm hiểu về công cụ HIP/SLEEK sử dụng kỹ thuật đặc
tả chương trình trên nền tảng Separation Logic, sử dụng trong kiểm định các
Module chương trình thao tác trên cấu trúc dữ liệu con trỏ.
3.3 Phạm vi tìm hiểu
Trên cơ sở nghiên cứu về lý thuyết các công trình nghiên cứu trước đâyvới
mục đích chính là tìm hiểu về Separation Logic và ứng dụng vào hệ thống kiểm
định tự động, phạm vi tìm hiểu của luận văn bao gồm các vấn đề cơ bản như sau:
- Tìm hiểu về lý thuyết cơ bản của của Logic bậc nhất, Hoare Logic cơ sở
nền tảng để hiểu rõ khái niệm về Separation Logic.
- Tìm hiểu về lý thuyết Separation Logic và ứng dụngkỹ thuật đặc tả chương
trình ngắn gọn, chính xác, bao quát chương trình một cách toàn vẹn và đầy đủ nhất.
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang14
-Nghiên cứu áp dụng công cụ HIP/SLEEK ứng dụng Separation Logic kiểm
định tự động chương trình thực tế của nhóm các tác giả Wei-Ngan Chin, Cristina
David, Huu Hai Nguyen, Shengchao Qin.
4.Các luận điểm cơ bản và đóng góp của luận văn
4.1 Các luận điểm cơ bản
Khi thiết kế một chương trình thì công việc tốn kém chi phí và thời gian nhất
chính là kiểm định chất lượng của chương trình, do đó việc tìm hiểu lý thuyết về
Separation Logic và kỹ thuật đặc tả chương trình chính xác, đầy đủ, toàn vẹnhứa
hẹn làm nền tảng cho việc xây dựng các công cụ kiểm định chương trình hoàn toàn
Chương 3: Trình bày các vấn đề cơ bản về công cụ kiểm định phần mềm tự
động HIP/SLEEK ứng dựng Separation Logic và kết quả thử nghiệm công cụ áp
dụng kiểm định phần mềm.
KẾT LUẬN
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang16
CHƯƠNG 1.TỔNG QUAN
Nội dung chương 1:
Trình bày về tổng quan nền tảng lý thuyết Separation Logic.
Trình bày vai trò của Separation Logic trong tự động hóa kiểm định phần
mềm.
Trong những năm 60 và 70 thì các dạng thức phân tích chương trình và kiểm
định chương trình đã được đề xuất bởi những tác giả tiên phong (Floyd, 1967;
Hoare, 1969; Dijkstra, 1976), với mục đích thực hiện suy diễn về chương trình và
đảm bảo chất lượng của phần mềm. Lĩnh vực này hơn 40 năm sau đó vẫn tiếp tục
phát triển mặc dù các yêu cầu trong kỹ thuật phần mềm ngày một nhiều hơn. Có rất
nhiều kỹ thuật khác nhau được ứng dụng cho những hoàn cảnh cụ thể, luận văn lựa
chọn tìm hiểu những khái niệm cơ bản về Separation Logic (một dạng thức mở rộng
của Hoare Logic thực hiện suy diễn về tính đúng đắn của chương trình, đặc biệt là
các chương trình liên quan đến tính an toàn của vùng nhớ truy cập bởi con trỏ) để
thực hiện nghiên cứu về lý thuyết suy diễn chương trình thông qua đặc tả chương
trình và ứng dụng trong tự động hóa kiểm định phần mềm.
1.1 Hoare Logic và kiểm định phần mềm
Cách tiếp cận để mô tả những hành vi của chương trình có thể tìm thấy trong
1.2 Separation Logic và kiểm định phần mềm
Kỹ thuật của Separation Logic là mô hình về những trạng thái vùng nhớ của
chương trình, trong phần này ta tìm hiểu những khái niệm nền tảng của Logic này.
Khởi nguồn của Separation Logic được biết đến với khái niệm Logic Bunch
(BI) được đề xuất bởi O'Hearn and Pym (1999), đó là sự kết hợp của Intuitionistic
Logic và Intuitionistic Linear Logic. Mô hình chứng minh mệnh đề của BI là sự kết
hợp của hai loại Logic này, đồng thời mô hình này sử dụng các vị từ của Logic bậc
nhất cùng với các lượng từ tồn tại.
BI tồn tại chỉ giống như một mô hình lý thuyết, khó có khả năng áp dụng vào
thực tế, cho đến khi Reynolds công bố các kết quả nghiên cứu của mình về suy diễn
trong chương trình, về mô hình Logic thì tương tự BI. Đó là sự mở rộng của cách
tiếp cận Hoare Logic để chứng minh tính đúng đắn của chương trình thao tác với
các cấu trúc cơ sở dữ liệu được tham chiếu bởi nhiều hơn một con trỏ. Ý tưởng của
nó là sự “tách biệt độc lập” của P và Q, điều này chỉ đúng khi P và Q là đúng và có
cùng một miền lưu trữ .
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang18
Sự kết hợp của O'Hearn và Reynolds sau đó đã tạo nên nền tảng của lý
thuyết Separation Logic mà tập trung vào các vấn đề suy diễn trạng thái chương
trình trên bộ nhớ Heap. Separation Logic được thêm vào hai kết nối cơ bản: * và
, ý nghĩa của P*Q là miền Heap được nắm giữ bởi P và Q là tách biệt. Mô hình này
là sự kế thừa những quy tắc suy diễn của Hoare Logic, với quy tắc Frame được sử
dụng suy diễn cục bộ chương trình mà không ảnh hưởng đến trạng thái Heap cục
bộ:
Các nghiên cứu về Separation Logic được công bố có thể kể đến như Yang
quá trình kiểm định phần mềm (Hoare Logic), nó đảm bảo rằng chương trình đáp
ứng đúng đặc tả.Đặc tính trung tâm của Hoare Logic là bộ ba Hoare, bộ ba này mô
tả những yêu cầu và ảnh hưởng của mã nguồn chương trình. Tập công cụ này có thể
áp dụng trong một dải khá rộng các phần mềm, trong đó nhấn mạnh thách thức theo
nghĩa rộng là việc kiểm định chương trình giải quyết vấn đề đưa ra đặc tả chính xác.
Công cụ này cho phép phát hiện ra những hành vi không mong muốn của chương
trình để có thể đưa ra được thiết kế phù hợp.
Tuy nhiên, lý thuyết của Floyd và Hoare đã không thể thiết lập được tính
đúng đắn của những chương trình làm việc với cấu trúc dữ liệu. Khái niệm
“Shared” có nghĩa là cấu trúc dữ liệu có thể trỏ/tham chiếu bởi nhiều hơn một con
trỏ/tham chiếu. Khái niệm “Mutable” cấu trúc dữ liệu có thể bị thay đổi sau khi có
bất kỳ một sự truy cập nào đến nó. Những loại chương trình này yêu cầu sự lưu trữ
cho phép bên ngoài bộ nhớ Stack (là Heap) và tính đúng đắn dựa trên giới hạn phức
tạp của chia sẻ cấu trúc dữ liệu.Để giải quyết vấn đề này, O’Hearn và Reynolds đã
thiết kế ra Separation Logic, đây là một sự mở rộng của Hoare Logiccho suy diễn
về cấu trúc dữ liệu “Shared Mutable ”. Mỗi một khẳng định của Separation Logic
mô tả những trạng thái được lưu trữ trong bộ nhớ Heap và Stack.Đặc tính nổi bật
của Separation Logic là sử dụng khái niệm “Shape” để đặc tả chương trình dưới
hình thức của Separation Logic. Trong miền “Shape” các thuộc tính cấu trúc dữ liệu
được đặc tả một cách ngắn gọn và đầy đủ hơn bởi việc thêm vào các đặc tính “Size,
Length, Bag”. Đặc biệt để tăng cường tính biểu hiện của ngôn ngữ đặc tả thông qua
việc cho phép người dùng có thể tự định nghĩa vị từ “User-defined”, điều này giúp
người dùng có thể định nghĩa ra các loại vị từ khác nhau mô tả quan hệ giữa các
thành phần của cấu trúc dữ liệu và các tính chất lượng từ mà người dùng mong
muốn.Đồng thời kế thừa thuộc tính của Hoare Logic, Separation Logic cũng có khả
năng áp dụng trong kiểm định chương trình tự động.
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang20
cũng như tính đúng đắn của suy diễn Logic.
Trong chương 1 đã trình bày khái quát các công đoạn liên quan tới quá trình
kiểm định phần mềm cũng như các phương pháp chủ yếu ứng dụng trong việc kiểm
định phần mềm. Để từ đó thấy được sự cần thiết của việc xây dựng nên những công
cụ kiểm định phần mềm tự động, đảm bảo cho việc kiểm định phần mềm được thực
hiện chính xác, hiệu quả, tiết kiệm chi phí, nhân lực cho công đoạn kiểm định phần
mềm.
Trong chương 2luận văn trình bày cơ sở lý thuyết về Separation Logic được
sử dụng làm nền tảng ứng dụng xây dựng những công cụ kiểm định phần mềm tự
động.Đồng thời trình bày kỹ thuật đặc tả chương trình ứng dụng Separation Logic.
Cụ thể, trong chương 2hướng tới làm rõ hơn về lý thuyết Separation Logic, luận văn
sẽ trình bày các vấn đề như sau:
-Để hiểu rõ hơn về khái niệm Separation Logic, luận văn đưa ra những khái
niệm cần thiết về Logic đặc biệt trình bày các khái niệm cơ bản lý thuyết về Hoare
Logic. Đây được coi là cơ sở nền tảng của lý thuyết về Separation Logic.
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang22
-Trình bày về lý thuyết cơ bản về Separation Logic và trọng tâm là kỹ thuật
đặc tả chương trình ứng dụng Separation Logic bao hàm các vấn đề:
Ngôn ngữ lập trình được sử dụng cho đặc tả dữ liệu và thủ tục chương trình.
Ngôn ngữ đặc tả với trọng tâm nhấn mạnh tìm hiểu vị từ User-defined.
Thủ tục forward verification.
Thủ tục entailment checking.
Các vấn đề về ngữ nghĩa, gồm có mô hình lưu trữ, mô hình ngữ nghĩa.
2.1 Logic bậc nhất
được coi là tập tiền đề và
là tập kết luận. Trong đó tập tiền đề và kết
luận là dạng thức logic bậc nhất. Ý nghĩa của tính toán liên tiếp là nguồn gốc của
những kết luận phải bắt nguồn từ những tiền đề. Đây là cú pháp cơ bản về nguồn
gốc trong hệ thống chứng minh.Những quy tắc suy diễn định nghĩa làm thế nào một
tính toán liên tiếp có thể được bắt nguồn từ những yếu tố khác trong một chứng
minh.Những quy luật này có thể chia nhỏ thành 2 nhóm: những quy tắc chứng minh
logic và những quy tắc chứng minh cấu trúc.
Ví dụ về chứng minh logic:
Học viên thực hiện: Nguyễn Đức Cường – Lớp 11BCNTT
Trang24
Quy tắc này đôi khi được ký hiệu
và nó thể hiện:
1. Bất cứ khi nào
đúng thì P phải là đúng
2. Bất cứ khi nào
đúng thì Q phải là đúng
Copyright: Tài liệu đại học ©