Một số phương pháp kiểm chứng tái cấu trúc phần mềm luận án ts máy tính 624801

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Đào Thị Hường MỘT SỐ PHƯƠNG PHÁP KIỂM CHỨNG TÁI CẤU TRÚC PHẦN MỀM LUẬN ÁN TIẾN SỸ CÔNG NGHỆ THÔNG TIN Hà Nội - 2018 LỜI CAM ĐOAN Tôi xin cam đoan luận án “Một số phương pháp kiểm chứng tái cấu trúc phần mềm” là công trình nghiên cứu của riêng tôi. Các số liệu, kết quả được trình bày trong luận á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 án hoàn toàn là công việc của riêng tôi.

 Trong các công trình khoa học được công bố trong luận án, tôi đã thể hiện rõ ràng và chính xác đóng góp của các đồng tác giả và những gì do tôi đã đóng góp.  Luận án được hoàn thành trong thời gian tôi làm Nghiên cứu sinh tại 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. Tác giả: Hà Nội: i ii LỜI CẢM ƠN Trước hết, tôi muốn bày tỏ sự biết ơn đến PGS.TS Trương Ninh Thuận, cán bộ hướng dẫn, người đã trực tiếp giảng dạy và định hướng tôi trong suốt thời gian học cao học, thực hiện luận văn thạc sĩ cũng như luận án này. Thầy không chỉ hướng dẫn cho tôi những kiến thức về học thuật mà còn chỉ bảo cho tôi những kinh nghiệm quý báu trong cuộc sống.

Một vinh dự lớn cho tôi được học tập, nghiên cứu dưới sự hướng dẫn của Thầy. Tôi xin bày tỏ sự biết ơn sâu sắc đến các Thầy Cô trong Bộ môn Công nghệ phần mềm vì sự giúp đỡ của các Thầy Cô về các đóng góp rất hữu ích cho luận án. Tôi xin trân trọng cảm ơn Khoa Công nghệ thông tin, Phòng Đào tạo và Ban giám hiệu trường Đại học Công nghệ đã tạo điều kiện thuận lợi cho tôi trong suốt quá trình thực hiện luận án. Tôi cũng bày tỏ sự biết ơn đến Ban giám hiệu Trường Đại học Hải Phòng đã tạo điều kiện về thời gian và tài chính cho tôi thực hiện luận án này.

Tôi muốn cảm ơn đến Ban chủ nhiệm, các cán bộ, giảng viên Khoa Công nghệ thông tin - Trường Đại học Hải Phòng đã cổ vũ động viên và sát cánh bên tôi trong suốt quá trình nghiên cứu. Một phần của nghiên cứu này được thực hiện trong khuôn khổ đề tài nghiên cứu khoa học số 102. Xin cảm ơn các trao đổi và trợ giúp của các thành viên đề tài. Tôi muốn cảm ơn đến tất cả những người bạn của tôi, đến toàn thể Anh/Chị/Em NCS những người luôn chia sẻ, động viên tôi bất cứ khi nào tôi cần và tôi luôn ghi nhớ điều đó.

Cuối cùng, tôi xin bày tỏ lòng biết ơn vô hạn đối với cha mẹ, chồng, con và gia đình đã luôn ủng hộ và yêu thương tôi một cách vô điều kiện. Nếu không có sự ủng hộ của gia đình và chồng con tôi không thể hoàn thành được luận án này. Một lần nữa xin được trân trọng cảm ơn vì tất cả. Đào Thị Hường iii TÓM TẮT Trong qúa trình phát triển của hệ thống phần mềm, tái cấu trúc (refac- toring) được biết đến “như tiến trình cải thiện cấu trúc bên trong (internal structure) mà không làm ảnh hưởng đến hành vi bên ngoài (external beha- viour) của hệ thống”.

Tuy nhiên, hoạt động tái cấu trúc thực hiện trên các hệ thống phần mềm rất dễ phát sinh lỗi đặc biệt trong trường hợp người phát triển không tuân thủ một cách nghiêm ngặt các quy trình và tiêu chuẩn phát triển phần mềm. Bởi vậy, tiến trình tái cấu trúc cần được kiểm soát một cách chặt chẽ đồng thời phải đánh giá ảnh hưởng của tiến trình này trên các đặc trưng về chất lượng và xem xét sự bảo toàn các đặc tính quan trọng của hệ thống phần mềm. Luận án đề xuất một số phương pháp bảo toàn các ràng buộc của hệ thống phần sau tiến trình tái cấu trúc. Cụ thể, luận án quan tâm đến các tiến trình tái cấu trúc áp dụng trên các hệ thống hướng đối tượng với các đặc trưng về bất biến (invariants) và hành vi (behaviors).

Các đóng góp chính của luận án được tóm tắt như sau: (i) Đề xuất phương pháp bảo toàn bất biến trong tái cấu trúc biểu đồ lớp của UML. Các phần tử của biểu đồ lớp cùng với các ràng buộc bất biến được hình thức hóa bằng các ký pháp toán học. Tái cấu trúc trên biểu đồ lớp được thực hiện thông qua các phép toán Folding, Abstraction, Composition, Factoring và Unfolding. Luận án đề xuất luật tái cấu trúc (refactoring rules) cho các phép toán đồng thời cũng chứng minh sự đúng đắn của các luật này bằng phương pháp toán học.

Tiến trình tái cấu trúc áp dụng các phép toán trên được khẳng định là bảo toàn bất biến của các lớp của mô hình ban đầu trên mô hình tái cấu trúc. (ii) Đề xuất phương pháp kiểm chứng sự bảo toàn hành vi trong tái cấu trúc hệ thống phần mềm bằng cách áp dụng mẫu thiết kế. Phần mềm ban đầu cùng với các ràng buộc về hành vi (pre/post-conditions) của các kịch bản (scenarios) tham gia vào tiến trình tái cấu trúc được hình thức hóa. Hoạt động tái cấu trúc được thực thi sẽ gây ảnh hưởng trực tiếp đến các thành phần cấu tạo cũng như các ràng buộc hành vi này.

iv Bởi vậy, các ràng buộc hành vi được tính toán lại và so sánh với với các ràng buộc của hệ thống ban đầu. Chú ý rằng, đối tượng được quan tâm đến khía cạnh bảo toàn hành vi là các kịch bản tham gia vào tiến trình tái cấu trúc. Đóng góp chủ yếu của luận án trong giải quyết bài toán bảo toàn hành vi là việc xây dựng các định nghĩa biểu diễn hình thức các khái niệm trong kịch bản và sử dụng các định nghĩa này trong quy trình kiểm chứng được đề xuất. Bài toán bảo toàn hành vi đã được giải quyết tại các giai đoạn thiết kế và cài đặt trong vòng đời phát triển phần mềm.

(iii) Xây dựng công cụ CVT (Consistency Validator Tool) hỗ trợ cho quá trình kiểm chứng tính nhất quán trong tái cấu trúc mô hình phần mềm. CVT nhận dữ liệu đầu vào là mô hình cùng với các ràng buộc hành vi của các hệ thống trước và sau khi tái cấu trúc. Sau quá trình thực thi, CVT sẽ trả lại kết luận về khả năng nhất quán giữa các mô hình này. Từ khóa: tái cấu trúc, bảo toàn bất biến, bảo toàn hành vi, kiểm chứng tính nhất quán.

Mục lục Lời cam đoan i Lời cảm ơn ii Tóm tắt iii Mục lục v Danh mục các từ viết tắt viii Danh mục các bảng ix Danh mục các hình vẽ x Danh mục các đặc tả xii Chương 1.2 Nội dung nghiên cứu .3 Cấu trúc luận án. KIẾN THỨC CƠ SỞ 9 2.2 Mô hình hướng đối tượng .3 Ngôn ngữ mô hình hóa thống nhất UML .2 Biểu đồ tuần tự .4 Mẫu thiết kế .5 Ngôn ngữ ràng buộc đối tượng OCL (Object Constraint Lan- guage) .6 Ngôn ngữ đặc tả cho Java (Java Modeling Language - JML) .7 Logic vị từ bậc 1 (First-Order Logic - FOL) .8 Kết chương. 27 v Contents vi Chương 3. PHƯƠNG PHÁP BẢO TOÀN BẤT BIẾN TRONG TÁI CẤU TRÚC 28 3.2 Các nghiên cứu liên quan .3 Tái cấu trúc trên biểu đồ lớp của UML .1 Tái cấu trúc các lớp với mối quan hệ phân cấp .2 Tái cấu trúc các liên kết trong biểu đồ lớp .4 Phương pháp bảo toàn bất biến trong tái cấu trúc biểu đồ lớp của UML .1 Quy trình kiểm tra sự bảo toàn bất biến trong tái cấu trúc biểu đồ lớp của UML .2 Mô hình hóa biểu đồ lớp trong UML .3 Khuôn mẫu biễu diễn các phép toán tái cấu trúc .4 Xây dựng các luật tái cấu trúc .5 Chứng minh tính đúng đắn của các luật tái cấu trúc .6 Kiểm chứng sự bảo toàn các ràng buộc bất biến sau tái cấu trúc .5 Kết chương.

PHƯƠNG PHÁP KIỂM CHỨNG SỰ BẢO TOÀN HÀNH VI TRONG TÁI CẤU TRÚC 62 4.2 Các nghiên cứu liên quan .3 Phương pháp kiểm chứng sự bảo toàn hành vi trong tái cấu trúc hệ thống phần mềm .1 Quy trình kiểm chứng sự bảo toàn hành vi trong tái cấu trúc hệ thống phần mềm .2 Phương pháp kiểm chứng tính nhất quán trong tái cấu trúc mô hình phần mềm .3 Phương pháp kiểm chứng tính nhất quán trong tái cấu trúc chương trình phần mềm .4 Áp dụng phương pháp kiểm chứng sự bảo toàn hành vi trên hệ thống điều khiển lưu lượng giao thông đường bộ (ARTC).1 Mô tả hệ thống ARTC .2 Một số hạn chế của hệ thống ARTC trước tái cấu trúc 82 4.3 Xác định các hành vi cần bảo toàn .4 Kiểm chứng tính nhất quán trong tái cấu trúc mô hình hệ thống ARTC.5 Kiểm chứng tính nhất quán trong tái cấu trúc chương trình phần mềm ARTC.5 Kết chương. CÔNG CỤ KIỂM CHỨNG 93 5.2 Xây dựng công cụ kiểm chứng CVT .1 Kiến trúc của công cụ kiểm chứng CVT .2 Chuyển đổi biểu thức OCL sang công thức FOL .3 Cài đặt và thực nghiệm .4 Kết chương. KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN 107 6.1 Các đóng góp của luận án .2 Hướng phát triển. 109 DANH MỤC CÁC CÔNG TRÌNH KHOA HỌC 113 TÀI LIỆU THAM KHẢO 114 DANH MỤC CÁC TỪ VIẾT TẮT Từ viết tắt Dạng đầy đủ Diễn giải/Tạm dịch ATM Automated Teller Machine Hệ thống rút tiền tự động ARTC Adaptive Road Traffic Control Hệ thống điều khiển giao thông AST Abstract Syntax Tree Cây cú pháp trừu tượng CVT Consistency Validator Tool Công cụ kiểm chứng tính nhất quán CD Class Diagram Biểu đồ lớp FOL First-Order Logic Logic vị từ bậc 1 JML Java Modeling Language Ngôn ngữ đặc tả cho Java OCL Object Constraint Language Ngôn ngữ ràng buộc đối tượng OOM Object Oriented Modeling Mô hình hóa hướng đối tượng SD Sequence Diagram Biểu đồ tuần tự SMT Satisfiability Modulo Theories Tính khả thỏa của lý thuyết môđun UML Unified Modeling Language Ngôn ngữ mô hình hóa thống nhất XML eXtensible Markup Language Ngôn ngữ đánh dấu mở rộng viii DANH MỤC CÁC BẢNG 3.1 Khuôn mẫu biểu diễn phép toán tái cấu trúc .1 Biểu thức OCL và công thức FOL tương ứng .2 Các luật sản xuất R của văn phạm phi ngữ cảnh G .3 Tập các luật xây dựng cây AST từ văn phạm phi ngữ cảnh G 100 ix DANH MỤC CÁC HÌNH VẼ 1.1 Cấu trúc luận án .1 Tổng quan về các loại biểu đồ trong UML 2.2 Minh họa biểu đồ lớp trong UML .3 Minh họa biểu đồ tuần tự trong UML .4 Một số mẫu thiết kế .