Tài liệu 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 002

ĐẠ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 ĐẠ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.TS. Nguyễn Việt Hà Hà Nội - 2015 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.TS. 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 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. 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. Giới thiệu .......................................................................................................1 1.1. Bối cảnh ....................................................................................................................1 1.2. Một số nghiên cứu liên quan ....................................................................................2 1.3. Nội dung nghiên cứu ................................................................................................3 1.4. Cấu trúc luận văn ......................................................................................................4 Chƣơng 2. Kiến thức cơ sở ..............................................................................................5 2.1. Kiểm chứng phần mềm.............................................................................................5 2.1.1. Kiểm chứng hình thức ...........................................................................................5 2.1.1.1. Kiểm chứng mô hình ..........................................................................................5 2.1.1.2. Chứng minh định lý ............................................................................................5 2.1.2. Kiểm chứng tại thời điểm thực thi.........................................................................6 2.2. Một số vấn đề trong chƣơng trình tƣơng tranh.........................................................6 2.3. Sự tƣơng tranh trong Java.........................................................................................7 2.4. Lập trình hƣớng khía cạnh........................................................................................8 2.4.1. Thực thi cắt ngang ...............................................................................................11 2.4.2. Điểm nối ..............................................................................................................12 2.4.3. Hƣớng cắt ............................................................................................................12 2.4.4. Mã hành vi ...........................................................................................................12 2.4.5. Khía cạnh .............................................................................................................14 2.4.6. Cơ chế hoạt động của AspectJ .............................................................................15 2.5. Kết luận...................................................................................................................16 Chƣơng 3. Ràng buộc thời gian giữa các thành phần trong chƣơng trình tƣơng tranh .17 iv 3.1. Giới thiệu ................................................................................................................17 3.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 ..........17 3.3. Phƣơng pháp đặc tả và kiểm chứng ràng buộc thời gian .......................................19 3.3.1. Mô tả phƣơng pháp ..............................................................................................19 3.3.2. Đặc tả ràng buộc thời gian ...................................................................................19 3.3.3. Biểu thức chính quy thời gian .............................................................................21 3.3.4. Phƣơng pháp sinh mã aspect ...............................................................................21 3.3.4.1. Đọc và phân tích biểu thức chính quy thời gian ...............................................21 3.3.4.2. Sinh mã aspect ..................................................................................................22 3.4. Kết luận...................................................................................................................22 Chƣơng 4. Thực nghiệm ................................................................................................ 26 4.1. Xây dựng công cụ TVG .........................................................................................26 4.1.1. Đọc và phân tích biểu thức chính quy thời gian ..................................................27 4.1.2. Sinh mã aspect .....................................................................................................30 4.2. Kiểm chứng một số chƣơng trình ...........................................................................33 4.2.1. Kiểm chứng chƣơng trình tuần tự .......................................................................33 4.2.2. Kiểm chứng chƣơng trình tƣơng tranh ................................................................ 36 Chƣơng 5. Kết luận........................................................................................................40 Phụ lục ...........................................................................................................................41 Phụ lục A. Công cụ sinh mã kiểm chứng TVG .............................................................41 A.1. Giới thiệu ...............................................................................................................41 A.2. Hƣớng dẫn sử dụng................................................................................................ 41 A.2.1. Các yêu cầu cài đặt .............................................................................................41 A.2.2. Các chức năng chính ...........................................................................................42 A.2.3. Hƣớng dẫn thực hiện ..........................................................................................42 TÀI LIỆU THAM KHẢO .............................................................................................44 Tiếng Việt ......................................................................................................................44 Tiếng Anh ......................................................................................................................44 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 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 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. ....................4 Hình 2.1 – Ví dụ sử dụng phƣơng thức run ....................................................................7 Hình 2.2 – Xung đột các tiến trình trong Java .................................................................8 Hình 2.3 – Sử dụng synchoronized để giải quyết tƣơng tranh ........................................8 Hình 2.4 – Xử lý cắt ngang trong lập trình OOP...........................................................10 Hình 2.5 – Xử lý cắt ngang trong lập trình AOP...........................................................10 Hình 2.6 – Biểu diễn một khía cạnh với mã hành vi trƣớc và sau ................................ 13 Hình 2.7 – Cấu trúc cơ bản của một khía cạnh. ............................................................14 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..17 Hình 3.2 – Mô tả quá trình chạy các phƣơng thức. .......................................................18 Hình 3.3 – Phƣơng pháp kiểm chứng ràng buộc thời gian. ...........................................20 Hình 3.4 – Thuật toán đọc biểu thức chính quy thời gian. ............................................23 Hình 3.5 – Ví dụ một mẫu aspect. .................................................................................24 Hình 3.6 – Thuật toán Sinh mã aspect. ..........................................................................25 Hình 4.1 – Cài đặt công cụ TVG bằng Netbean 7.0.1 ...................................................26 Hình 4.2 – Một đoạn mã aspect sinh ra từ công cụ TVG. .............................................27 Hình 4.3 – Pattern kiểm tra từng thành phần trong TRE ..............................................28 Hình 4.4 – Lớp TimingMethod .....................................................................................28 Hình 4.5 – Quá trình đọc và phân tích biểu thức TRE. .................................................30 Hình 4.6 – Tạo mã aspect từ các mẫu đã định nghĩa .....................................................31 Hình 4.7 – Template aspectHead...................................................................................32 Hình 4.8 – Template aspectTail.....................................................................................32 Hình 4.9 – Mã nguồn một chƣơng trình tuần tự ............................................................34 Hình 4.10 – Kết quả thực nghiệm ca kiểm thử đúng chƣơng trình tuần tự. ..................35 Hình 4.11 – Kết quả thực nghiệm ca kiểm thử sai chƣơng trình tuần tự. .....................35 Hình 4.12 – Mã nguồn một chƣơng trình tƣơng tranh. .................................................38 Hình 4.13 – Kết quả thực nghiệm ca kiểm thử đúng chƣơng trình tƣơng tranh ...........39 Hình 4.14 – Kết quả thực nghiệm ca kiểm thử sai chƣơng trình tƣơng tranh ...............39 viii Hình A.1 – Giao diện chính của công cụ sinh mã TVG ................................................41 Hình A.2 – Đặc tả ràng buộc thời gian các thành phần bằng TRE ...............................42 Hình A.3 – Đan mã aspect với mã chƣơng trình Java viết bằng Eclipse ......................43 1 Chƣơng 1. Giới thiệu 1.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ế. Các phần mềm (chương trình) tƣơng tranh gồm hai hoặc nhiều tiến trình cộng tác với nhau để thực hiện cùng một nhiệm vụ [19]. 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 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. 1.2. 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. SACRES [4] là một môi trƣờng kiểm chứng cho các hệ thống nhúng, cho phép ngƣời sử dụng đặc tả ràng buộc thời gian bằng các biểu đồ thời gian dạng ký hiệu (symbolic timing diagrams). 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. Wegener [33] đề xuất phƣơng pháp để kiểm chứng ràng buộc thời gian trong các hệ thống thời gian thực dựa trên kỹ thuật kiểm chứng tiến hóa (evolutionary testing). Trong đó, vi phạm ràng buộc thời gian đƣợc định nghĩa là đầu ra (output) đƣợc đƣa ra quá nhanh hoặc quá chậm so với đặc tả. Do đó, nhiệm vụ của ngƣời kiểm thử là thiết kế các đầu vào (input) với thời gian thực hiện nhanh nhất hoặc chậm nhất để phát hiện các vi phạm. Việc thiết kế đầu vào đƣợc quy về bài toán tối ƣu trong tính toán tiến hóa để tự động tìm đầu vào với thời gian thực hiện nhanh nhất và chậm nhất. Tuy nhiên phƣơng pháp này chƣa kiểm chứng đƣợc ràng buộc thời gian giữa các thành phần. Guo và Lee [20] đề xuất phƣơng pháp kết hợp giữa đặc tả và kiểm chứng ràng buộc thời gian cho các hệ thống thời gian thực. Trong đó, ràng buộc thời gian cùng với yêu cầu hệ thống đƣợc đặc tả bằng môđun TER nets [30]. Giống nhƣ [4] 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. Trong [10] phƣơng pháp sử dụng biểu đồ thời gian của UML đƣợc đề xuất để ƣớc lƣợng thời gian thực thi trong trƣờng hợp xấu nhất của các thành phần hệ thống ở thời điểm thiết kế. Thời gian thực thi đƣợc ƣớc lƣợng dựa trên biểu đồ ca sử dụng kết hợp với các thông tin về hành vi của ngƣời sử dụng hệ thống trong tƣơng lai. Phƣơng pháp này cũng không kiểm chứng ràng buộc thời gian thực thi giữa các thành phần. Jin [35] đề xuất phƣơng pháp hình thức để kiểm chứng tĩnh thứ tự thực hiện của các phƣơng thức (Method Call Sequence – MCS) trong chƣơng trình Java tuần tự phƣơng pháp này sử dụng ôtômát hữu hạn trạng thái để đặc tả giao thức, các chƣơng trình Java đƣợc biến đổi thành các văn phạm phi ngữ cảnh (context free grammar – CFG) sử dụng công cụ Accent. Ngôn ngữ sinh ra bởi ôtômát L(A) đƣợc so sánh với ngôn ngữ sinh ra bởi CFG L(G), Nếu 𝐿 𝐺 ⊆ 𝐿(𝐴) thì chƣơng trình Java tuân theo đặc tả giao thức, và ngƣợc lại. Ƣu điểm của phƣơng pháp này đó là các vi phạm có thể đƣợc phát 3 hiện sớm, tại thời điểm phát triển hoặc biên dịch chƣơng trình. Do đó sự thực thi của chƣơng trình không bị ảnh hƣởng. Deline và Fahndrich [30] đề xuất phƣơng pháp kiểm chứng vào thời điểm thực thi sự tuân thủ cài đặt và đặc tả MCS. Phƣơng pháp này sử dụng máy trạng thái để đặc tả MCS. Đặc tả MCS sau đó đƣợc biên dịch sang mã nguồn và đan xen với mã nguồn chƣơng trình để kiểm chứng động sự tuân thủ của cài đặt so với đặc tả MCS. Các mệnh đề tiền và hậu điều kiện của các phƣơng thức trong MCS cũng đƣợc đặc tả và kiểm chứng. Tuy nhiên, phƣơng pháp này chƣa kiểm chứng đƣợc ràng buộc thời gian giữa các thành phần. Yoonsik và Perumandla [8, 9] mở rộng ngôn ngữ đặc tả, và trình biên dịch JML để biểu diễn giao thức tƣơng tác bằng biểu thức chính quy. Sau đó, biểu thức chính quy đƣợc biên dịch thành mã thực thi để chạy đan xen với chƣơng trình gốc để kiểm chứng sự tuân thủ giữa cài đặt so với đặc tả giao thức tƣơng tác. Các hành vi của chƣơng trình gốc sẽ không bị thay đổi ngoại trừ thời gian và kích thƣớc. Nhƣ [35] phƣơng pháp này chƣa kiểm chứng đƣợc ràng buộc thời gian giữa các thành phần so với đặc tả. 1.3. Nội dung nghiên cứu Trong luận văn này, tác giả tập trung nghiên cứu phƣơng pháp để kiểm chứng ràng buộc thời gian chƣơng trình tƣơng tranh ở pha cài đặt mã nguồn chƣơng trình. Sử dụng phƣơng pháp lập trình hƣớng khía cạnh (AOP) để 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 (Hình 1.1) cụ thể là thời gian thực thi của các phƣơng thức trong chƣơng trình. Các vi phạm sẽ đƣợc phát hiện tại thời điểm thực thi chƣơng trình. Trong hƣớng tiếp cận này, ràng buộc về thời gian giữa các phƣơng thức của một ứng dụng hƣớng đối tƣợng (OOP) viết bằng ngôn ngữ Java sẽ đƣợc đặc tả bằng biểu thức chính quy thời gian. Từ các đặc tả đầu vào này mã khía cạnh (aspect) sẽ đƣợc tự động sinh ra đan với mã của các thành phần chƣơng trình từ đó kiểm chứng sự tuân thủ ràng buộc thời gian so với đặc tả. Khi đó, trong quá trình chạy của chƣơng trình, các đoạn mã aspect sẽ tự động kiểm tra thời gian thực thi các thành phần trong chƣơng trình và thông báo lỗi khi có vi phạm xảy ra. Tác giả tập trung vào việc xây dựng công cụ TVG (Timed Verify Generator) để sinh mã aspect kiểm chứng một cách tự động từ đặc tả ràng buộc thời gian. Đầ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. 4 1.4. Cấu trúc luận văn Nội dung luận văn đƣợc trình bày trong năm chƣơng. Chƣơng 1 giới thiệu về đề tài nghiên cứu. Chƣơng này trình bày ngữ cảnh, các nghiên cứu liên quan, lý do lựa chọn đề tài, nội dung nghiên cứu của đề tài và cấu trúc nội dung của luận văn. Chƣơng 2 trình bày các kiến thức nền phục vụ cho đề tài. Chƣơng này mô tả các kiến thức cơ bản về kiểm chứng phần mềm, một số vấn đề trong chƣơng trình tƣơng tranh, sự tƣơng tranh trong Java và phƣơng pháp lập trình hƣớng khía cạnh. Chƣơng 3 trình bày nội dung chính nghiên cứu của luận văn là phƣơng pháp đặc tả và kiểm chứng các ràng buộc thời gian giữa các thành phần tuần tự và song song trong chƣơng trình tƣơng tranh. Chƣơng 4 giới thiệu về công cụ và kết quả thực nghiệm của phƣơng pháp. Chƣơng 5 đƣa ra kết luận, định hƣớng phát triển cho đề tài. Cuối cùng là tài liệu tham khảo đƣợc sử dụng trong luận văn. Đặc tả yêu cầu Bản thiết kế Sai Kiểm chứng thiết kế Đúng Cài đặt chƣơng trình Đúng Sai Kiếm chứng chƣơng trình Lập trình hƣớng khía cạnh Đúng 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. 5 Chƣơng 2. Kiến thức cơ sở 2.1. Kiểm chứng phần mềm Kiểm chứng phần mềm (software verification) là tập các nguyên lý, phƣơng pháp và công cụ để đảm bảo tính đúng đắn của các sản phẩm phần mềm. Trong mục này, luận văn sẽ giới thiệu khái quát hai phƣơng pháp kiểm chứng phần mềm là kiểm chứng hình thức và kiểm chứng tại thời điểm thực thi chƣơng trình. 2.1.1. Kiểm chứng hình thức 2.1.1.1. Kiểm chứng mô hình Phƣơng pháp kiểm chứng mô hình (model checking) đƣợc sử dụng để xác định tính hợp lệ của một hay nhiều tính chất mà ngƣời dùng quan tâm trong một mô hình phần mềm cho trƣớc. Cho mô hình M và thuộc tính p cho trƣớc, nó kiểm tra thuộc tính p có thỏa mãn trong mô hình M hay không, ký hiệu 𝑀 ⊨ 𝑝 [5]. Về mặt thực thi kiểm chứng mô hình sẽ duyệt qua các trạng thái, các đƣờng thực thi có thể có trong mô hình 𝑀 để xác định tính khả thỏa của p. Trong đó các thuộc tính đƣợc đặc tả bằng logic thời gian LTL hoặc CTL [5]. Mô hình M là một cấu trúc Kripke gồm bốn thành phần M = (S, S0, L, R) với 𝑆 là một tập hữu hạn các trạng thái, S0 ∈ S là trạng thái đầu, 𝑅 ⊂ 𝑆 × 𝑆 là quan hệ chuyển trạng thái, 𝐿 ∶ 𝑆 → 2𝐴𝑃 là hàm gán nhãn với AP là tập hữu hạn các mệnh đề nguyên tử đƣợc xây dựng từ hệ thống. Một bộ kiểm chứng mô hình [21, 29] (model checker) sẽ kiểm tra tất cả các trạng thái có thể có của mô hình để tìm ra tất cả các đƣờng thực thi có thể gây ra lỗi. Do đó không gian trạng thái thƣờng là vô cùng lớn nếu không muốn nói là vô hạn. Vì vậy việc duyệt qua tất cả các trạng thái là bất khả thi. Để đối phó với bài toán bùng nổ không gian trạng thái đã có một vài các nghiên cứu liên quan đến các kỹ thuật làm giảm không gian trạng thái nhƣ Abtraction, Slicing [15, 34]. 2.1.1.2. Chứng minh định lý Phƣơng pháp chứng minh định lý (theorem proving) [32] sử dụng các kỹ thuật suy luận để chứng minh tính đúng đắn của một công thức hay tính khả thỏa một công thức F với tất cả các mô hình, ký hiệu ⊨ 𝐹. Trong đó, Pi với 𝑖 = 1 … 𝑛 là tập các tiên đề, C là tập các định lý. Một 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. 6 P1, P2,…,Pn ├ name C 2.1.2. Kiểm chứng tại thời điểm thực thi Kiểm chứng tại thời điểm thực thi (runtime verification) [18] là kỹ thuật kết hợp giữa kiểm chứng hình thức và thực thi chƣơng trình để phát hiện các lỗi của hệ thống dựa trên quá trình quan sát input/output khi thực thi chƣơng trình. Các hành vi quan sát đƣợc sẽ đƣợc theo dõi và kiểm tra có thỏa mãn với đặc tả yêu cầu của hệ thống. So sánh với phƣơng pháp kiểm chứng tĩnh thì kiểm chứng tại thời điểm thực thi đƣợc thực hiện trong khi thực thi hệ thống. Vì vậy phƣơng pháp này còn đƣợc gọi là kiểm thử bị động (passive testing). Kiểm chứng tại thời điểm thực thi nhằm đảm bảo sự tuân thủ giữa cài đặt hệ thống phần mềm so với đặc tả thiết kế của nó. Các trƣờng hợp thƣờng lựa chọn kiểm chứng tại thời điểm thực thi. - Không thể đảm bảo đƣợc tính đúng đắn giữa sự cài đặt chƣơng trình so với đặc tả thiết kế của nó. Nhiều thông tin chỉ có sẵn hoặc thu thập đƣợc tại thời điểm thực thi chƣơng trình. Các hành vi của hệ thống phụ thuộc vào môi trƣờng khi nó đƣợc thực thi. Với các hệ thống an toàn và bảo mật cao. 2.2. Một số vấn đề trong chƣơng trình tƣơng tranh Trong các chƣơng trình tƣơng tranh, có hai thuộc tính cơ bản cần đảm bảo là an toàn (safety) và thực hiện đƣợc (liveness) [6, 31]. Thuộc tính an toàn đảm bảo chƣơng trình luôn thỏa mãn (luôn đúng) các ràng buộc của nó. Ví dụ nhƣ ràng buộc sự xung đột (interference) giữa các tiến trình. Thuộc tính thực hiện đƣợc đảm bảo chƣơng trình cuối cùng sẽ thỏa mãn (sẽ đúng) các ràng buộc của nó. Sự xung đột (interference) xảy ra khi hai hoặc nhiều tiến trình đồng thời truy cập một biến chia sẻ, trong đó ít nhất một tiến trình ghi và các tiến trình khác không có cơ chế để ngăn chặn sự truy cập đồng thời này. Khi đó giá trị của biến chia sẻ và kết quả của chƣơng trình sẽ phụ thuộc vào sự đan xen (interleaving) hay thứ tự thực hiện của các tiến trình. Sự xung đột còn đƣợc gọi là cạnh tranh dữ liệu (datarace). Tắc nghẽn xảy ra khi hệ thống (chương trình) không thể đáp ứng đƣợc bất kỳ tín hiệu hoặc yêu cầu nào. Có hai dạng tắc nghẽn, dạng một xảy ra khi các tiến trình dừng lại và chờ đợi lẫn nhau, ví dụ một chƣơng trình nắm giữ khóa mà các tiến trình khác mong muốn và ngƣợc lại. Dạng hai xảy ra khi một tiến trình chờ đợi một tiến trình 7 khác không kết thúc. Một thuộc tính khác tƣơng tự nhƣ khóa chết khi các tiến trình liên tục thay đổi trạng thái của nó để đáp ứng với những thay đổi của những tiến trình khác mà không đạt đƣợc mục đích cuối cùng. Sự đói (starvation) liên quan đến tranh chấp tài nguyên, vấn đề này xảy ra khi một tiến trình không thể truy cập tài nguyên chia sẻ. 2.3. Sự tƣơng tranh trong Java Java là ngôn ngữ lập trình hƣớng đối tƣợng hỗ trợ lập trình tƣơng tranh với cơ chế đồng bộ hóa giữa các tiến trình, mô phỏng bộ nhớ chia sẻ, môi trƣờng lập trình trực quan và hệ thống thƣ viện phong phú với nhiều giao diện lập trình tƣơng tranh khác nhau. Java đƣợc biết đến nhƣ một ngôn ngữ lập trình tƣơng tranh đƣợc sử dụng rộng rãi trong công nghiệp phần mềm. Đặc biệt từ phiên bản 5.0, Java hỗ trợ thƣ viện APIs bậc cao java.util.concurrent khiến việc cài đặt chƣơng trình tƣơng tranh trở nên khá dễ dàng. Sự tƣơng tranh trong Java [28] đƣợc thực hiện thông qua cơ chế giám sát các tiến trình, hành vi của tiến trình đƣợc mô tả trong phƣơng thức run. Một ví dụ sử dụng phƣơng thức run đƣợc trình bày trong Hình 2.1. Runnable task = () -> { String threadName = Thread.currentThread().getName(); System.out.println("Hello " + threadName); }; task.run(); Thread thread = new Thread(task); thread.start(); System.out.println("Done!"); Hình 2.1 – Ví dụ sử dụng phƣơng thức run Sự thực thi của một tiến trình có thể đƣợc điều khiển bởi một tiến trình khác thông qua các phƣơng thức stop, suspend và resum. Tuy nhiên, với các hệ thống lớn gồm nhiều tiến trình thì việc sử dụng các phƣơng thức này để điều khiển sự thực thi của các tiến trình là không an toàn, do chúng ta khó có thể kiểm soát tất cả các tiến trình. Một ví dụ cho vấn đề này đƣợc trình bày trong Hình 2.2. Kết quả trả về của phƣơng thức trong ví dụ Hình 2.2 là 9965 do có sự xung đột giữa các tiến trình. Do đó, Java cung cấp một mô hình tƣơng tranh để giải quyết sự đồng bộ hóa giữa các tiến trình. Khi nhiều tiến trình cùng muốn truy cập vào dữ liệu chia sẻ trong một vùng giới hạn đƣợc đánh dấu bằng từ khóa synchoronized thì tại một thời điểm khóa của vùng xung đột chỉ cho phép một tiến trình đƣợc phép truy cập. Một ví dụ sử dụng synchoronized để giải quyết tƣơng tranh đƣợc trình bày trong Hình 2.3. Thay vì gọi 8 phƣơng thức increment() chúng ta gọi phƣơng thức đã đƣợc thêm từ khóa synchoronized cụ thể là phƣơng thức incrementSync() Kết quả trả về lúc này sẽ là 10000 do quá trình xung đột giữa các tiến trình đã đƣợc giải quyết. int count = 0; void increment() { count = count + 1; } ExecutorService executor = Executors.newFixedThreadPool(2); IntStream.range(0, 10000) .forEach(i -> executor.submit(this::increment)); stop(executor); System.out.println(count); // 9965 Hình 2.2 – Xung đột các tiến trình trong Java void incrementSync() { synchronized (this) { count = count + 1; } } Hình 2.3 – Sử dụng synchoronized để giải quyết tƣơng tranh Một tiến trình sẽ sử dụng phƣơng thức wait để chờ khi nó không thể truy cập vào vùng xung đột mà bị chiếm giữ bởi tiến trình khác. Các tiến trình có thể đƣợc đánh thức bằng các phƣơng thức notify hoặc notifyAll. Chiến lƣợc giám sát ở mức thấp của Java không tránh đƣợc các lỗi liên quan về tƣơng tranh nhƣ khóa chết, xung đột. 2.4. Lập trình hƣớng khía cạnh Lập trình hƣớng khía cạnh (AOP) [3, 22, 23] đƣợc xây dựng trên các phƣơng pháp lập trình hiện tại nhƣ lập trình hƣớng đối tƣợng (OOP), lập trình hƣớng cấu trúc, bổ sung thêm các khái niệm và cấu trúc hóa các mối quan tâm khác nhau thành các mô-đun. Ở đây, một mối quan tâm thƣờng không phải là một chứng năng nghiệp vụ cụ thể và có thể đóng gói mà là một khía cạnh (thuộc tính) chung mà nhiều mô-đun phần mềm trong cùng hệ thống nên có. Chúng ta sẽ lấy một ví dụ để thấy đƣợc sự khác nhau giữa AOP và OOP. Ở đây tác giả sẽ sử dụng lớp Point với cấu trúc đƣợc định nghĩa trong Hình 2.4. Khi chúng ta di chuyển Point từ một vị trí này sang vị trí khác tức là phải đặt lại giá trị của x và y, ta phải cập nhật lại thông qua phƣơng thức display.update(this). Nhƣ vậy, cùng một phƣơng thức display.update(this) ta phải viết lại ở ba vị trí khác 9 nhau ứng với ba sự thay đổi. Hãy tƣởng tƣợng đối với mã nguồn chƣơng trình đủ lớn và có hàng nghìn lần thay đổi tƣơng tự nhƣ thay đổi ở trên dòng mã display.update(this) sẽ phải xuất hiện ở hàng nghìn chỗ khác nhau. Chƣa kể tới vấn đề bảo trì và nâng cấp, một ví dụ là khách hàng yêu cầu ngoài việc hiển thị thông tin chúng ta cần lƣu ra một file log.txt. Lúc này lập trình viên phải dò lại tất cả mã nguồn và chèn thêm vào đó dòng lệnh lƣu vết ra file log.txt. Lập trình hƣớng đối tƣợng OOP có thể giải quyết rất tốt các chức năng chính của hệ thống nhƣng nó lại gặp rất nhiều khó khăn trong việc giải quyết các chứng năng cắt ngang hệ thống. Khi sử dụng OOP để thực hiện các chức năng cắt ngang hệ thống sẽ gặp phải hai vấn đề chính là: Chồng chéo mã nguồn (Code tangling) và dàn trải mã nguồn (Code scattering). - - Chồng chéo mã nguồn: Mô-đun chính của hệ thống ngoài việc thực hiện các yêu cầu chính, nó còn phải thực hiện các yêu cầu khác nhƣ: tính đồng bộ, bảo mật, lƣu vết, lƣu trữ. Nhƣ vậy, trong một mô-đun có rất nhiều loại mã khác nhau. Điều này làm cho tính mô-đun hóa của hệ thống giảm đi, khả năng sử dụng lại mã nguồn thấp, khó bảo trì hệ thống Dàn trải mã nguồn: Cùng một mã nguồn của các chức năng cắt ngang hệ thống đƣợc cài đặt lặp đi lặp lại rất nhiều lần ở nhiều mô-đun chính của hệ thống. Điển hình nhƣ ví dụ trong Hình 2.4. Nền tảng cơ bản của AOP khác với OOP là cách quản lý các chức năng cắt ngang hệ thống. Việc thực thi của từng chức năng cắt ngang AOP bỏ qua các hành vi đƣợc tích hợp vào nó. Với AOP, chúng ta có thể cài đặt các mối quan tâm chung cắt ngang hệ thống bằng các mô-đun đặc biệt gọi là khía cạnh (aspect) thay vì dàn trải chúng trên các mô-đun nghiệp vụ liên quan. Nhờ mã đƣợc tách riêng biệt, các vấn đề đan xen trở nên dễ kiểm soát hơn. Các khía cạnh của hệ thống có thể thay đổi, thêm hoặc xóa lúc biên dịch và có thể tái sử dụng. Một trình biên dịch đặc biệt là Aspect Weaver thực hiện các thành phần riêng lẻ thành một hệ thống thống nhất. Quay trở lại với ví dụ trong Hình 2.4. Nếu sử dụng lập trình hƣớng khía cạnh AOP, các chức năng cắt ngang hệ thống: Cập nhật hình, lƣu vết sẽ đƣợc giải quyết theo cách sau: Thay vì tích hợp trực tiếp trong mô-đun nghiệp vụ chính, lập trình viên sẽ tách chúng thành các mô-đun mới gọi là aspect. Hình 2.5 mô tả mã nguồn cho việc thực thi chức năng cập nhật bằng cách sử dụng AOP. Sau khi đã định nghĩa một aspect nhƣ vậy thì bất cứ khi nào có sự thay đổi về hình (setX, setY, moveBy) chƣơng trình sẽ tự động gọi chức năng cập nhật cụ thể ở đây là phƣơng thức display.update(this). Đơn giản chúng ta chỉ cần cài đặt các aspect mà không cần phải thay đổi mã nguồn của chƣơng trình chính. 10 package Test; public class Point { private int x = 0, y = 0; int getX(){return x;} int gety(){return y;} void moveBy(int dx, int dy) { x = x + dx; y = y + dy; display.update(this); } void setX(int x) { this.x = x; display.update(this); } void setY(int y) { this.y = y; display.update(this); } } Hình 2.4 – Xử lý cắt ngang trong lập trình OOP package Test; import org.aspectj.lang.JoinPoint; public aspect TestAspect { pointcut updateDisplay(): execution(void *.setX(int)) || execution(void *.setY(int)) || execution(void *.moveBy(int, int)); after(): updateDisplay() { display.update(this); } } Hình 2.5 – Xử lý cắt ngang trong lập trình AOP AOP là một kỹ thuật đầy triển vọng, hứa hẹn đem lại nhiều lợi ích cho việc phát triển phần mềm, sau đây là một số lợi ích cụ thể khi chúng ta sử dụng AOP: - Mô-đun hóa những vấn đề đan xen nhau: AOP xác định vấn đề một cách riêng biệt, cho phép mô-đun hóa những vấn đề liên quan đến nhiều đối tƣợng.