Luận văn: Đặc tả và kiểm chứng ràng buộc thời gian chương trình tương tranh

Luận văn thạc sĩ: Nghiên cứu đặc tả, kiểm chứng ràng buộc thời gian trong chương trình tương tranh. Giải pháp nâng cao độ tin cậy, hiệu năng hệ thống.

• Tác giả: Phạm Thanh Hải
• Người hướng dẫn: PGS. Nguyễn Việt Hà
• Trường học: Trường Đại học Công nghệ - Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tà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
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CÁM ƠN
• LỜI CAM ĐOAN
• MỤC LỤC
• DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT
• DANH SÁCH BẢNG
• DANH SÁCH HÌNH VẼ
• 1. Chƣơng 1. Một số nghiên cứu liên quan
• 1.1. Nội dung nghiên cứu
• 1.2. Cấu trúc luận văn
• 1.3. Kiến thức cơ sở
• 1.4. Kiểm chứng phần mềm
• 1.5. Kiểm chứng hình thức
• 1.6. Kiểm chứng mô hình
• 1.7. Chứng minh định lý
• 1.8. Kiểm chứng tại thời điểm thực thi
• 1.9. Một số vấn đề trong chƣơng trình tƣơng tranh
• 1.10. Sự tƣơng tranh trong Java
• 1.11. Lập trình hƣớng khía cạnh
• 1.12. Thực thi cắt ngang
• 1.13. Cơ chế hoạt động của AspectJ
• 1.14. Ràng buộc thời gian giữa các thành phần trong chƣơng trình tƣơng tranh
• 2. 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
• 3. Phƣơng pháp đặc tả và kiểm chứng ràng buộc thời gian
• 3.1. Mô tả phƣơng pháp
• 3.2. Đặc tả ràng buộc thời gian
• 3.3. Biểu thức chính quy thời gian
• 3.4. Phƣơng pháp sinh mã aspect
• 3.5. Đọc và phân tích biểu thức chính quy thời gian
• 3.6. Xây dựng công cụ TVG
• 3.7. Đọc và phân tích biểu thức chính quy thời gian
• 4. Kiểm chứng một số chƣơng trình
• 4.1. Kiểm chứng chƣơng trình tuần tự
• 4.2. Kiểm chứng chƣơng trình tƣơng tranh
• 4.3. Công cụ sinh mã kiểm chứng TVG
• 4.4. Hƣớng dẫn sử dụng
• 4.4.1. Các yêu cầu cài đặt
• 4.4.2. Các chức năng chính
• 4.4.3. Hƣớng dẫn thực hiện
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Về Kiểm Chứng Ràng Buộc Thời Gian Chương Trình

Phần mềm đóng vai trò quan trọng trong xã hội. Quá trình phát triển phần mềm bao gồm 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ì. Trong đó, kiểm thử, phát hiện và sửa lỗi phần mềm rất quan trọng để đảm bảo chất lượng. Lỗi hệ thống gây hậu quả nghiêm trọng, không chỉ thiệt hại kinh tế mà còn tổn hại đến sinh mạng con người. Lỗi phần mềm được phát hiện càng muộn, hậu quả càng nghiêm trọng. Vì vậy, nhiều phương pháp đã được đề xuất và phát triển để giảm lỗi phần mềm. Các phương pháp kiểm chứng như chứng minh định lý và kiểm chứng mô hình đã được ứng dụng thành công để kiểm chứng mô hình thiết kế. Tuy nhiên, việc cài đặt mã nguồn chương trình có thể vi phạm các ràng buộc thiết kế. Do đó, phần mềm vẫn có thể có lỗi. Các phương pháp kiểm chứng tại thời điểm thực thi như kiểm thử phần mềm bằng các bộ dữ liệu kiểm thử thường chỉ phát hiện các lỗi về giá trị đầu ra 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ẻ hoặc cơ chế truyền thông điệp. 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 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.

1.1. Các Hướng Tiếp Cận Chính trong Kiểm Chứng Phần Mềm

Các phương pháp kiểm chứng phần mềm được chia thành hai loại chính: kiểm chứng hình thức và kiểm chứng tại thời điểm thực thi. Kiểm chứng hình thức bao gồm chứng minh định lý và kiểm chứng mô hình. Kiểm chứng tại thời điểm thực thi theo dõi hành vi của chương trình trong quá trình chạy để phát hiện lỗi, một phương pháp kiểm chứng hình thức là Model checking. Phương pháp này kiểm tra các trạng thái và đường thực thi có thể có để xác định các lỗi. Nó sử dụng logic thời gian để đặc tả các thuộc tính cần kiểm tra. Các hệ thống gọi là đúng (sound) nếu tất cả các định lý của nó đƣợc chứng minh. Các phƣơng pháp chứng minh định lý nhƣ B [27], Event-B [26] đã đƣợc sử dụng thành công để đặc tả và kiểm chứng tính đúng đắn của mô hình thiết kế phần mềm.

1.2. Sự Quan Trọng Của Ràng Buộc Thời Gian Trong Hệ Thống

Trong các hệ thống thời gian thực và hệ thống nhúng, ràng buộc thời gian là yếu tố then chốt. Việc vi phạm ràng buộc thời gian có thể dẫn đến hậu quả nghiêm trọng. Ví dụ, trong hệ thống điều khiển máy bay, việc một tác vụ không hoàn thành đúng thời gian có thể gây ra tai nạn. Các kỹ thuật 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.

II. Các Thách Thức Kiểm Chứng Thời Gian Thực Chương Trình

Kiểm chứng chương trình tương tranh khó hơn so với chương trình tuần tự vì khả năng thực thi của các chương trình này. Với một chương trình tương tranh, việc thực thi hai lần với cùng một đầu vào không đảm bảo 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, tắc nghẽn 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, ví dụ 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 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.

2.1. Khó Khăn Trong Việc Đảm Bảo Tính Đúng Đắn Thời Gian

Đảm bảo tính đúng đắn về thời gian trong chương trình tương tranh là một thách thức lớn. Do tính không xác định trong việc thực thi các tiến trình, thời gian thực thi có thể thay đổi đáng kể. Các phương pháp kiểm thử truyền thống thường không đủ để phát hiện tất cả các vi phạm về ràng buộc thời gian. 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.

2.2. Các Vấn Đề Về Xung Đột và Tắc Nghẽn ảnh hưởng đến Thời Gian

Các vấn đề như xung đột dữ liệu (data races) và tắc nghẽn (deadlocks) có thể ảnh hưởng đáng kể đến thời gian thực thi của chương trình tương tranh. Xung đột xảy ra khi nhiều tiến trình truy cập cùng một dữ liệu chia sẻ. Tắc nghẽn xảy ra khi các tiến trình chờ đợi lẫn nhau, dẫn đến tình trạng hệ thống không thể tiếp tục hoạt động. 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.

2.3. Giới hạn của Kiểm Thử Truyền Thống

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ế.

III. Phương Pháp Đặc Tả Kiểm Chứng Ràng Buộc Thời Gian

Luận văn nghiên cứu một phương pháp kiểm chứng ràng buộc thời gian thực thi các thành phần cụ thể là các phương thức trong chương trình Java tuần tự và tương tranh. Sử dụng các biểu thức chính quy thời gian (Timing Regular Expression – TRE) để đặc tả các ràng buộc thời gian (Timing constraint – TC). Trong đó mỗi biểu thức chính quy có quy tắc biểu diễn nhƣ sau. Từ các đặc tả này mã aspect sẽ đƣợc tự động sinh ra đan với mã của các thành phần để từ đó kiểm chứng sự tuân thủ ràng buộc thời gian so với đặc tả. Phƣơng pháp này đã đƣợc thực nghiệm với nhiều chƣơng trình khác nhau. Kết quả thực nghiệm cho thấy phƣơng pháp đã phát hiện các vi phạm về ràng buộc thời gian giữa các thành phần so với đặc tả.

3.1. Sử Dụng Biểu Thức Chính Quy Thời Gian TRE

Phương pháp sử dụng biểu thức chính quy thời gian (TRE) để đặc tả ràng buộc thời gian. TRE cho phép định nghĩa các ràng buộc một cách linh hoạt và dễ dàng kiểm tra. Đầu vào của công cụ TVG là các biểu thức chính quy thời gian. Và đầu ra là các đoạn mã aspect kiểm chứng. Luận văn nghiên cứu một phương pháp kiểm chứng ràng buộc thời gian thực thi các thành phần cụ thể là các phương thức trong chương trình Java tuần tự và tương tranh.

3.2. Quy Trình Kiểm Chứng Ràng Buộc Thời Gian Chi Tiết

Quy trình kiểm chứng bao gồm các bước: đặc tả ràng buộc, sửa lỗi, sinh mã, đan mã, và kiểm tra lỗi. Nếu có lỗi, hệ thống sẽ thông báo kết quả. Nếu không, chương trình được coi là đã được kiểm chứng. Đặc tả ràng buộc thời gian với cú pháp: Kiểu trả về phương thức_Tên phương thức(Tham số truyền vào:Tên tham số truyền vào)[Thời gian thực thi tối thiểu cho phép,Thời gian thực thi tối đa cho phép]. Các mã aspect có thể phát hiện đƣợc chính xác các thành phần vi phạm với các ràng buộc thời gian.

3.3. Thuật Toán Đọc Biểu Thức Chính Quy Thời Gian

Bƣớc 1: Phân tách biểu thức chính quy thời gian đầu vào thành các thành phần. Lƣu các thành phần vào một mảng dữ liệu. Bƣớc 2: Duyệt danh sách các phần tử trong mảng tiến hành bóc tách các biểu thức và toán tử. Ở đây tác giả quy định hai dạng biểu thức đơn (single) và khối biểu thức (block). Các biểu thức đơn là các biểu thức chỉ bao gồm một phƣơng thức thể hiện đoạn mã nguồn thực thi tuần tự, các khối biểu thức bao gồm từ hai phƣơng thức trở lên thể hiện đoạn mã nguồn tƣơng tranh. Thuật toán bóc tách biểu thức đƣợc trình bày trong Hình 3. Bƣớc 3: Sau khi đã bóc tách toàn bộ biểu thức chính quy thời gian và lƣu vào một HashMap. Tác giả tiến hành phân tích các biểu thức đơn và khối biểu thức từ đó lấy đƣợc các thông tin về ràng buộc thời gian của từng phƣơng thức.

IV. Ứng Dụng TVG Trong Kiểm Chứng Chƣơng Trình

Áp dụng các phƣơng pháp đƣợc giới thiệu từ Chƣơng 3 tác giả đã cài đặt thành công Công cụ tự động sinh mã Aspect từ biểu thức chính quy thời gian. Tác giả sử dụng công cụ Netbeans 7.1 cùng với JDK để cài đặt công cụ. Sau khi đặc tả ràng buộc thời gian bằng biểu thức chính quy thời gian đây là đầu vào cho công cụ TVG.

4.1. Cài Đặt Công Cụ TVG Timed Verify Generator

Tác giả đã cài đặt thành công công cụ TVG bằng Netbeans 7.1 và JDK. Công cụ này tự động sinh mã Aspect từ biểu thức chính quy thời gian, giúp đơn giản hóa quá trình kiểm chứng ràng buộc thời gian. Cài đặt công cụ TVG đƣợc tác giả thực hiện qua các bƣớc chính sau đây: Bƣớc 1: Phân tích biểu thức chính quy thời gian đầu vào. Từ đó xây dựng máy trạng thái. Bƣớc 2: Xây dựng các mẫu AspectJ tuân theo cú pháp Aspect cơ bản, bao gồm tên Aspect, vùng pointcut và vùng advise. Bƣớc 3: Duyệt qua máy trạng thái lấy dữ liệu từng trạng thái sử dụng các phƣơng thức thao tác với xâu ký tự để sinh mã Aspect.

4.2. Sinh Mã Aspect Từ Đặc Tả Ràng Buộc Thời Gian

Công cụ TVG sinh mã Aspect từ các đặc tả ràng buộc thời gian, cho phép kiểm tra các ràng buộc này trong quá trình thực thi. Mã Aspect được sinh ra sẽ tự động đan với mã của các thành phần trong chương trình để kiểm chứng ràng buộc thời gian giữa các thành phần. Mã nguồn của quá trình trên đƣợc trình bày trong Hình 4. Tác giả sử dụng một HashMap để tiến hành lƣu các thông tin đọc đƣợc từ biểu thức TRE đầu vào. Trong quá trình phân tích tác giả sử dụng một Stack để tiến hành bóc tách các thành phần trong biểu thức TRE.

4.3. Mã kiểm chứng cho các chương trình

Sau khi đã có đƣợc các thông tin về ràng buộc thời gian từ việc đọc biểu thức chính quy thời gian (TRE) đầu vào. Tác giả tiến hành sinh mã aspect kiểm chứng dựa trên những thông tin này. Tác giả sử dụng ba mẫu (template) đƣợc trình bày trong Hình 3.7 để tạo ra mã aspect kiểm chứng. Mẫu aspectHead đƣợc trình bày trong Hình 4.6 tạo ra phần đầu của mã aspect kiểm chứng: Thƣ viện aspectJ sử dụng, Tên của aspect kiểm chứng, và khai báo các tham số cần thiết.

V. Kết Quả Thực Nghiệm Kiểm Chứng Thời Gian Chương Trình

Với mỗi phƣơng thức trong chƣơng trình tác giả xây dựng một test đúng và một test sai. Trong đó với test đúng thì thành phần sẽ tuân thủ ràng buộc thời gian trong đặc tả và ngƣợc lại. Với mỗi phƣơng thức tác giả thiết lập hai biến số đại diện cho test đúng và test sai. Tác giả lần lƣợt truyền hai biến số này vào chƣơng trình và tiến hành chạy thử nghiệm.

5.1. Kiểm Chứng Mã nguồn chương trình tuần tự

Kết quả thực nghiệm cho thấy khi tiến hành đan mã aspect sinh ra từ công cụ TVG với mã nguồn chương trình và tiến hành chạy đối với ca kiểm thử đúng, thời gian thực thi các phƣơng thức đều thỏa mãn ràng buộc thời gian thực thi [1000, 5000] nano giây, [1000, 30000] nano giây, và [10000,30000] nano giây. Ngƣợc lại đối với ca kiểm thử sai thời gian thực thi của phƣơng thức đều vƣợt quá ràng buộc thời gian cho phép.

5.2. Kiểm Chứng chương trình tƣơng tranh

Kết quả thực nghiệm cho thấy khi tiến hành đan mã aspect sinh ra từ công cụ TVG với mã nguồn chương trình và tiến hành chạy đối với ca kiểm thử đúng, phƣơng thức firstSequence() đƣợc thực thi với thời gian là 40040 nano giây thỏa mãn ràng buộc thời gian thực thi [30000, 60000] nano giây. Tiếp theo phƣơng thức còn lại là secondSequence() đƣợc thi với thời gian 16761 nano giây thỏa mãn với ràng buộc thời gian là [10000, 30000] nano giây. Cuối cùng phƣơng thức Test.run() đƣợc thực hiện với thời gian là 29177 nano giây và phƣơng thức Test.run() đƣợc thực hiện với thời gian là 49973 nano giây thỏa mãn ràng buộc thời gian [20000, 300000] nano giây và [30000, 300000] nano giây.

VI. Kết Luận Hướng Phát Triển Trong Tương Lai

Luận văn đã nghiên cứu một phương pháp kiểm chứng tuân thủ giữa sự cài đặt của các thành phần phần mềm so với đặc tả các ràng buộc thời gian cụ thể là các phƣơng thức trong chƣơng trình Java. Hạn chế lớn nhất của phƣơng pháp này cũng nhƣ các phƣơng pháp kiểm chứng động khác là phải thực thi chƣơng trình, vi phạm chỉ đƣợc phát hiện trong bƣớc kiểm thử, mã aspect đƣợc đan vào tuy không thay đổi hành vi của chƣơng trình nhƣng sẽ tăng kích thƣớc của chƣơng trình.

6.1. Tổng Kết Đóng Góp Của Nghiên Cứu

Nghiên cứu đã đề xuất một phương pháp kiểm chứng ràng buộc thời gian cho chương trình tương tranh sử dụng biểu thức chính quy thời gian và lập trình hướng khía cạnh. Kết quả thực nghiệm cho thấy phương pháp có khả năng phát hiện các vi phạm về ràng buộc thời gian. Các mã aspect có thể phát hiện đƣợc chính xác các thành phần vi phạm với các ràng buộc thời gian.

6.2. Các Hướng Phát Triển Trong Tương Lai

Trong tƣơng lai tác giả sẽ mở rộng công cụ TVG để có thể kiểm chứng các hệ thống mã nguồn có quy mô lớn. Áp dụng TVG cho nhiều ngôn ngữ lập trình khác nhau. Kết hợp phƣơng pháp này với các phƣơng pháp kiểm thử tĩnh khác nhƣ kiểm chứng mô hình để tiến tới phát triển một phƣơng pháp kiểm chứng tự động hoàn toàn từ mức mô hình đến cài đặt.

Trích đoạn nội dung tài liệu

ĐẠ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 TIEU LUAN MOI download : [e-mail] ĐẠ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 TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : [e-mail] 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. TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : skknchat@gmail. 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 TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : [e-mail] 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 TIEU LUAN MOI download : [e-mail] 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).

Tuy nhiên phƣơng pháp này chỉ kiểm chứng ở mức mô hình, không phải mức cài đặt.