- ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ. - 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. - CHƯƠNG TRÌNH TƯƠNG TRANH Ngành: Công nghệ thông tin. - 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.. - 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 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.. - 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.. - Một số nghiên cứu liên quan. - Cấu trúc luận văn. - Kiểm chứng phần mềm. - Kiểm chứng hình thức. - Kiểm chứng mô hình. - 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. - Ràng buộc thời gian giữa các thành phần trong chương trình tương tranh. - 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 gianError! Bookmark not defined.. - Đặ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. - Sinh mã aspect. - Đọ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. - 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. - 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. - Hình 2.1 – Ví dụ sử dụng phương thức run. - Hình 2.2 – Xung đột các tiến trình trong Java. - Hình 2.3 – Sử dụng synchoronized để giải quyết tương tranhError! Bookmark not defined.. - Hình 2.4 – Xử lý cắt ngang trong lập trình OOP. - Hình 2.5 – Xử lý cắt ngang trong lập trình AOP. - Hình 2.6 – Biểu diễn một khía cạnh với mã hành vi trước và sauError! Bookmark not defined.. - Hình 2.7 – Cấu trúc cơ bản của một khía cạnh. - Hình 3.1 – Mã nguồn một chương trình bao gồm thành phần tuần tự và tương tranh.. - Hình 3.2 – Mô tả quá trình chạy các phương thức. - Hình 3.3 – Phương pháp kiểm chứng ràng buộc thời gian.Error! Bookmark not defined.. - Hình 3.4 – Thuật toán đọc biểu thức chính quy thời gian.Error! Bookmark not defined.. - Hình 3.5 – Ví dụ một mẫu aspect. - Hình 3.6 – Thuật toán Sinh mã aspect. - Hình 4.1 – Cài đặt công cụ TVG bằng Netbean 7.0.1. - Hình 4.2 – Một đoạn mã aspect sinh ra từ công cụ TVG.Error! Bookmark not defined.. - Hình 4.3 – Pattern kiểm tra từng thành phần trong TREError! Bookmark not defined.. - Hình 4.4 – Lớp TimingMethod. - Hình 4.5 – Quá trình đọc và phân tích biểu thức TRE. - Hình 4.6 – Tạo mã aspect từ các mẫu đã định nghĩa. - Hình 4.7 – Template aspectHead. - Hình 4.8 – Template aspectTail. - Hình 4.9 – Mã nguồn một chương trình tuần tự. - Hình 4.10 – Kết quả thực nghiệm ca kiểm thử đúng chương trình tuần tự. - Hình 4.11 – Kết quả thực nghiệm ca kiểm thử sai chương trình tuần tự. - Hình 4.12 – Mã nguồn một chương trình tương tranh. - Hình 4.13 – Kết quả thực nghiệm ca kiểm thử đúng chương trình tương tranh. - Hình 4.14 – Kết quả thực nghiệm ca kiểm thử sai chương trình tương tranh. - Hình A.1 – Giao diện chính của công cụ sinh mã TVG Error! Bookmark not defined.. - Hình A.2 – Đặc tả ràng buộc thời gian các thành phần bằng TREError! Bookmark not defined.. - Hình A.3 – Đan mã aspect với mã chương trình Java viết bằng Eclipse. - Kiểm chứng sự tuân thủ về ràng buộc thời gian trong các ứng dụng phần mềm. - in In Formal Techniques in Real-Time and Fault Tolerant systems, FTRTFT’98 school, Lyngby, Denmark.. - in In Software Engineering Research and Practice, CSREA Press.. - in In Proceedings of the 2008 Third International Conference on Dependability of Computer Systems, Washington, DC, USA.. - Journal of the ACM,, no. - 49, Journal of the ACM.. - in In Proceedings of the 3rd international conference on Aspect-oriented software. - in In Proceedings of the 6th Conference on WSEAS International Conference on Applied Computer Science, USA.. - in In ECOOP ’01 : Proceedings of the 15th European Conference on Object-Oriented Programming, London, UK.. - Ben-Ari (2008), Principles of the Spin Model Checker, 1st ed.. - in In Proceedings of the First IFIP TC10 International Workshop on Software Engineering for Parallel and Distributed Systems, London, UK, UK.. - in In Companion to the proceedings of the 29th International Conference on Software Engineering, Washing- ton, DC, USA.. - in In ASE ’00 : Proceedings of the 15th IEEE international conference on Automated software engineering, Washington, DC, USA.. - in In Proceedings of the 31st Annual International Computer Software and Applications, Washington.