ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ Phạm Thanh Hải NGHIÊN CỨU VỀ ĐẶC TẢ VÀ KIỂM CHỨNG RÀNG BUỘC THỜI GIAN GIỮA CÁC THÀNH PHẦN TRONG CHƢƠNG TRÌNH TƢƠNG TRANH LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 2015 HÀ NỘI - 2011 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ Phạm Thanh Hải Lời Cam Đoan NGHIÊN CỨU VỀ ĐẶC TẢ VÀ KIỂM CHỨNG RÀNG BUỘC THỜI GIAN GIỮA CÁC THÀNH PHẦN TRONG CHƢƠNG TRÌNH TƢƠNG TRANH Ngành: Công nghệ thông tin Chuyên ngành : Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƢỜI HƢỚNG DẪN KHOA HỌC: PGS. Nguyễn Việt Hà Hà Nội - 2015 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com i LỜI CÁM ƠN Đầu tiên tôi xin gửi lời cảm ơn sâu sắc tới thầy giáo PGS. Nguyễn Việt Hà, bộ môn công nghệ phần mềm, khoa công nghệ thông tin, trƣờng Đại học Công nghệ – Đại học Quốc Gia Hà Nội ngƣời đã định hƣớng đề tài và tận tình hƣớng dẫn chỉ bảo tôi trong suốt quá trình thực hiện luận văn tốt nghiệp này. Tôi cũng xin trân trọng cảm ơn quý thầy cô trong Khoa Công nghệ thông tin trƣờng Đại học Công nghệ – Đại học Quốc Gia Hà Nội đã tận tình giảng dạy, truyền đạt những kiến thức quý báu trong suốt hai năm học làm nền tảng cho tôi thực hiện luận văn tốt nghiệp này.
Tôi cũng xin đƣợc cảm ơn các tác giả của các công trình nghiên cứu, tài liệu đã đƣợc tôi sử dụng, trích dẫn trong luận văn vì đã cung cấp nguồn tƣ liệu quý báu và các kiến thức liên quan để tôi thực hiện luận văn. Con xin cảm ơn cha mẹ và gia đình đã sinh ra và nuôi dạy con khôn lớn, luôn bên cạnh động viên và ủng hộ con trên con đƣờng mà con yêu thích và lựa chọn. Cám ơn các bạn học viên cao học Khoa công nghệ thông tin khóa K19. Các bạn đã giúp đỡ và ủng hộ tôi rất nhiều cũng nhƣ đóng góp nhiều ý kiến quý báu, qua đó giúp tôi hoàn thiện luận văn tốt hơn.
Mặc dù đã rất nỗ lực, cố gắng nhƣng chắc hẳn luận văn của tôi vẫn còn nhiều thiếu sót. Tôi rất mong nhận đƣợc nhiều những ý kiến đánh giá quý, phê bình của quý thầy cô, của anh chị và các bạn. Một lần nữa tôi xin chân thành cảm ơn! Hà Nội, tháng 11 năm 2015 Phạm Thanh Hải LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com ii LỜI CAM ĐOAN Tôi xin cam đoan luận văn tốt nghiệp “Nghiên cứu về đặc tả và kiểm chứng ràng buộc thời gian giữa các thành phần trong chƣơng trình tƣơng tranh” là công trình nghiên cứu của riêng tôi dƣới sự hƣớng dẫn của PGS.TS Nguyễn Việt Hà. Các số liệu các kết quả đƣợc 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 kỳ một công trình nào khác.
Tôi đã trích dẫn đầy đủ các tài liệu tham khảo, công trình nghiên cứu liên quan ở trong nƣớc và quốc tế. Ngoại trừ các tài liệu tham khảo này, luận văn hoàn toàn là công việc của riêng tôi. Nếu có phát hiện nào về sự gian lận sao chép tài liệu, công trình nghiên cứu của tác giả khác mà không đƣợc ghi rõ trong phần tài liệu tham khảo, tôi sẽ chịu hoàn toàn trách nhiệm về kết quả luận văn của mình. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com iii MỤC LỤC LỜI CÁM ƠN .i LỜI CAM ĐOAN.
ii MỤC LỤC. iii DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT .v DANH SÁCH BẢNG.vi DANH SÁCH HÌNH VẼ. vii Chƣơng 1. Một số nghiên cứu liên quan.
Nội dung nghiên cứu. Cấu trúc luận văn. Kiến thức cơ sở. Kiểm chứng phần mềm.
Kiểm chứng hình thức. Kiểm chứng mô hình. Chứng minh định lý. Kiểm chứng tại thời điểm thực thi.
Một số vấn đề trong chƣơng trình tƣơng tranh. Sự tƣơng tranh trong Java. Lập trình hƣớng khía cạnh. Thực thi cắt ngang.
Cơ chế hoạt động của AspectJ. Ràng buộc thời gian giữa các thành phần trong chƣơng trình tƣơng tranh .17 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Bài toán kiểm chứng ràng buộc thời gian giữa các thành phần tƣơng tranh. Phƣơng pháp đặc tả và kiểm chứng ràng buộc thời gian.
Mô tả phƣơng pháp. Đặc tả ràng buộc thời gian. Biểu thức chính quy thời gian. Phƣơng pháp sinh mã aspect.
Đọc và phân tích biểu thức chính quy thời gian. Xây dựng công cụ TVG. Đọc và phân tích biểu thức chính quy thời gian. Kiểm chứng một số chƣơng trình.
Kiểm chứng chƣơng trình tuần tự. Kiểm chứng chƣơng trình tƣơng tranh. Công cụ sinh mã kiểm chứng TVG. Hƣớng dẫn sử dụng.
Các yêu cầu cài đặt. Các chức năng chính. Hƣớng dẫn thực hiện .42 TÀI LIỆU THAM KHẢO .44 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com v DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT Dạng viết tắt Dạng đầy đủ Diễn giải AOP Aspect Oriented Programming Lập trình hƣớng khía cạnh CFG Context Free Grammar Văn phạm phi ngữ cảnh IDE Integrated Development Môi trƣờng pháp triển tích hợp Environment MCS Method Call Sequence Tuần tự gọi phƣơng thức OOP Object Oriented Programming Lập trình hƣớng đối tƣợng TVG Timed Verify Generator Công cụ kiểm sinh mã TC Timing constraint Ràng buộc thời gian TRE Timed Regular Expressions Biểu thức chính quy thời gian LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com vi DANH SÁCH BẢNG Bảng 2.1 - Ánh xạ giữa các loại điểm nối (joinpoint) và hƣớng cắt (pointcut) tƣơng ứng .14 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com vii DANH SÁCH HÌNH VẼ Hình 1.1 – Kiểm chứng chƣơng trình mức cài đặt sử dụng lập trình AOP.1 – Ví dụ sử dụng phƣơng thức run .2 – Xung đột các tiến trình trong Java .3 – Sử dụng synchoronized để giải quyết tƣơng tranh .4 – Xử lý cắt ngang trong lập trình OOP.5 – Xử lý cắt ngang trong lập trình AOP.6 – Biểu diễn một khía cạnh với mã hành vi trƣớc và sau .7 – Cấu trúc cơ bản của một khía cạnh.1 – Mã nguồn một chƣơng trình bao gồm thành phần tuần tự và tƣơng tranh.2 – Mô tả quá trình chạy các phƣơng thức.3 – Phƣơng pháp kiểm chứng ràng buộc thời gian.4 – Thuật toán đọc biểu thức chính quy thời gian.5 – Ví dụ một mẫu aspect.6 – Thuật toán Sinh mã aspect.1 – Cài đặt công cụ TVG bằng Netbean 7.2 – Một đoạn mã aspect sinh ra từ công cụ TVG.3 – Pattern kiểm tra từng thành phần trong TRE .5 – Quá trình đọc và phân tích biểu thức TRE.6 – Tạo mã aspect từ các mẫu đã định nghĩa .9 – Mã nguồn một chƣơng trình tuần tự .10 – Kết quả thực nghiệm ca kiểm thử đúng chƣơng trình tuần tự.11 – Kết quả thực nghiệm ca kiểm thử sai chƣơng trình tuần tự.12 – Mã nguồn một chƣơng trình tƣơng tranh.13 – Kết quả thực nghiệm ca kiểm thử đúng chƣơng trình tƣơng tranh .14 – Kết quả thực nghiệm ca kiểm thử sai chƣơng trình tƣơng tranh .39 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com viii Hình A.1 – Giao diện chính của công cụ sinh mã TVG .2 – Đặc tả ràng buộc thời gian các thành phần bằng TRE .3 – Đan mã aspect với mã chƣơng trình Java viết bằng Eclipse .43 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 1 Chƣơng 1. Bối cảnh Phần mềm hiện đóng một vai trò vô cùng quan trọng trong xã hội [24].
Quá trình phát triển phần mềm gồm rất nhiều giai đoạn: Thu thập yêu cầu, phân tích, thiết kế, xây dựng, kiểm thử, triển khai và bảo trì phần mềm. Trong các giai đoạn trên thì giai đoạn kiểm thử, phát hiện, xác định và sửa lỗi phần mềm là rất quan trọng để đảm bảo chất lƣợng của phần mềm. Lỗi hệ thống gây ra hậu quả đặc biệt nghiêm trọng không chỉ gây thiệt hại về kinh tế mà còn tổn hại trực tiếp đến sinh mạng con ngƣời. Lỗi phần mềm đƣợc phát hiện càng muộn thì càng gây hậu quả nghiêm trọng, tốn rất nhiều thời gian và công sức để sửa lỗi, thậm chí phải xây dựng lại toàn bộ hệ thống.
Vì vậy, trong công nghệ phần mềm đã có nhiều phƣơng pháp khác nhau đƣợc đề xuất và phát triển để giảm lỗi phần mềm từ pha thiết kế đến cài đặt. Các phƣơng pháp kiểm chứng nhƣ chứng minh định lý (theorem proving) và kiểm chứng mô hình (model checking) đã ứng dụng thành công để kiểm chứng mô hình thiết kế của phần mềm [7, 5]. Trong nhiều hệ thống, cài đặt thực tế thƣờng chỉ đƣợc thực hiện sau khi mô hình thiết kế đã đƣợc kiểm chứng. Tuy nhiên việc cài đặt mã nguồn chƣơng trình hoàn toàn có thể vi phạm các ràng buộc thiết kế [34].
Do đó, phần mềm vẫn tồn tại lỗi mặc dù thiết kế của nó đã đƣợc kiểm chứng và thẩm định một cách chi tiết. Các phƣơng pháp kiểm chứng tại thời điểm thực thi [25, 13, 17] nhƣ kiểm thử phần mềm bằng các bộ dữ liệu kiểm thử (test suite) gặp phải một hạn chế là thƣờng chỉ phát hiện đƣợc các lỗi về giá trị đầu ra (out put) mà không phát hiện đƣợc các lỗi vi phạm ràng buộc thiết kế. Trong đó mỗi tiến trình là một chƣơng trình tuần tự thực hiện một tập các câu lệnh tuần tự. Các tiến trình thƣờng cộng tác với nhau thông qua các biến chia sẻ (shared variables) hoặc cơ chế truyền thông điệp (message passing).
Lập trình và kiểm chứng chƣơng trình tƣơng tranh thƣờng khó hơn so với chƣơng trình tuần tự do khả năng thực hiện của các chƣơng trình này. Với một chƣơng trình tƣơng tranh chúng ta thực thi hai lần cùng với một đầu vào nhƣ nhau thì không thể đảm bảo chƣơng trình sẽ trả về cùng một kết quả. Các nghiên cứu gần đây tập trung vào các vấn đề về xung đột (interference), tắc nghẽn (dead lock) trong chƣơng trình Java tƣơng tranh. Tuy nhiên các phƣơng pháp này chƣa kiểm chứng vấn đề về thỏa mãn ràng buộc thời gian nhƣ thời gian thực thi của các tiến trình.
Đối với các hệ thống thời gian thực, hệ thống an toàn – bảo mật việc vi phạm ràng buộc thời gian sẽ gây ra các lỗi hệ thống rất nghiêm trọng. Do đó nhu cầu nghiên LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 2 cứu phƣơng pháp kiểm chứng ràng buộc về thời gian trong chƣơng trình tƣơng tranh trở nên cần thiết. Một số nghiên cứu liên quan Đã có một vài phƣơng pháp, công cụ đƣợc đề xuất để kiểm chứng ràng buộc thời gian trong các hệ thống phần mềm. Các đặc tả thiết kế đƣợc dịch sang máy hữu hạn trạng thái (finite state machine) đƣợc tối ƣu và kiểm chứng bằng mô hình ký hiệu (symbolic model checking).