Đề tài Kiểm chứng các giao thức bằng AOP

1 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Thân Văn Đức KIỂM CHỨNG CÁC GIAO THỨC BẰNG AOP KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin HÀ NỘI - 2010 2 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Thân Văn Đức KIỂM CHỨNG CÁC GIAO THỨC BẰNG AOP KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin Cán bộ hướng dẫn: Ths.Phạm Thị Kim Dung HÀ NỘI - 2010 3 Lời cảm ơn Trong quá trình thực hiện đề tài, tôi đã gặp rất nhiều khó khăn và bỡ ngỡ. Nếu không có sự giúp đỡ và lời động viên chân thành của nhiều người có lẽ tôi khó có thể hoàn thành tốt khóa luận này. Đầu tiên tôi xin tỏ lòng biết ơn sâu sắc đến Cô Phạm Thị Kim Dung đã tận tình hướng dẫn trong suốt quá trình viết khóa luận tốt nghiệp. Tôi muốn gửi lời cảm ơn đến các thầy giáo cô giáo trong hội đồng bảo vệ. Những ý kiến đóng góp của cô là vô cùng hữu ích, nó giúp tôi nhận ra các khuyết điểm của khóa luận. Tôi xin chân thành cảm ơn quý Thầy, Cô và bạn bè 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 truyền đạt kiến thức, sát cánh và trải nghiệm cùng tôi trong suốt 4 năm học tập. Với vốn kiến thức được tiếp thu trong quá trình học không chỉ là nền tảng cho quá trình nghiên cứu khóa luận mà còn là hành trang quí báu để tôi bước vào đời một cách vững chắc và tự tin. Con xin cảm ơn cha mẹ, những người đã có công sinh thành, dưỡng dục và nuôi dạy con nên người. Cuối cùng tôi kính chúc quý thầy, cô dồi dào sức khỏe, đạt được nhiều thành công trong công việc và cuộc sống. 4 TÓM TẮT NỘI DUNG Kiểm chứng phần mềm có một vai trò quan trọng trong việc đảm bảo tính đúng đắn của hệ thống phần mềm trong suốt quá trình thực thi,kiểm chứng giúp phát hiện, tìm ra lỗi và thông báo lỗi cho nhà phát triển. Phương pháp lập trình hướng khía cạnh (AOP) cùng với công nghệ AspectJ ra đời đã tạo ra một hướng phát triển mới cho kiểm chứng phần mềm, giúp nâng cao khả năng dò tìm lỗi, thông báo lỗi mà không ảnh hưởng tới mã nguồn hệ thống. Trong thực tế, biểu đồ UML là sự lựa chọn rất phổ biến cho việc mô hình hóa hệ thống phần mềm ở giai đoạn thiết kế hiện nay. Trong đó, biểu đồ tuần tự (sequence diagram) là một biểu đồ quan trọng, nó miêu tả các cách thức đối tượng tương tác và giao tiếp với nhau. Việc kiểm chứng thiết kế và kiểm chứng các giao thức ràng buộc trong biểu đồ trình tự là rất cần quan trọng vì nếu thiết kế biểu đồ tuần tự sai kéo theo các hoạt động của hệ thống hoặc trình tự hệ thống cần thực hiện sẽ bị sai dẫn tới toàn bộ hệ thống thiết kế sai. Trong phạm vi khóa luận, tôi xin trình bày phương pháp sinh mã aspect phục vụ cho mục đích kiểm chứng phần mềm từ biểu đồ tuần tự kết hợp với máy trạng thái và công cụ tự động sinh mã aspect dựa trên phương pháp này. Mã aspect tạo ra từ công cụ có thể dùng đan vào chương trình để thực hiện nhiệm vụ kiểm chứng các ràng buộc giữa các đối tượng và tính đúng đắn của hệ thống nhằm giảm thiểu tối đa lỗi khi viết mã cài đặt cho hệ thống. 5 MỤC LỤC Chương 1. Mở Đầu ....................................................................................................8 1.1. Đặt vấn đề .........................................................................................................8 1.2.Bài toán..............................................................................................................8 1.3. Tổng quan về phương pháp giải quyết bài toán..................................................9 1.4. Cấu trúc khóa luận.............................................................................................9 Chương 2. Ngôn ngữ UML và biểu diễn biểu đồ trong UML bằng XMI..............11 2.1. Giới thiệu chung về UML:...............................................................................11 2.2. Các loại biểu đồ UML .....................................................................................12 2.2.1. Nhóm biểu đồ về cấu trúc ........................................................................12 2.2.2. Nhóm biểu đồ hành vi ..............................................................................12 2.3. Biểu đồ tuần tự trong UML2.0(Sequence diagram) .........................................12 2.4. Một số thành phần chính trong biểu đồ tuần tự ................................................14 2.4.1. Đường đời (lifeLine) ................................................................................14 2.4.2. Thông điệp (Message)..............................................................................15 2.4.3. Đoạn gộp (Combind Fragment)................................................................16 2.5. Biểu diễn biểu đồ tuần tự :...............................................................................19 2.5.1. Biểu diễn Đường đời (LifeLine ):.............................................................19 2.5.2. Biểu diễn Thông điệp: ..............................................................................19 2.5.3. Lời chú giải (Comment) ...........................................................................19 2.5.4. Các đoạn gộp (CombindedFragment) .......................................................19 2.6. Sơ lược về XML..............................................................................................20 2.7. Biểu diễn tài liệu XML....................................................................................21 2.8. TƯƠNG TÁC VỚI TÀI LIỆU XML ...............................................................23 2.8.1 DOM........................................................................................................23 2.8.2 XML DOM :.............................................................................................23 2.8.3 XMI:.........................................................................................................25 2.9. Máy trạng thái FSM. .......................................................................................25 2.9.1. Tổng quan về các thành phần trong máy trạng thái FSM ..........................25 2.9.2. Xây dựng máy hữu hạn trạng thái từ các thành phần của biểu đồ ...................26 CHƯƠNG 3..............................................................................................................30 Aspect và lập trình hướng khía cạnh ......................................................................30 3.1 Tổng quan về lập trình hướng khía cạnh. ..........................................................30 3.2 Biên dịch AOP: ................................................................................................31 6 3.3 LỢI ÍCH CỦA AOP : .......................................................................................32 3.4 AspectJ.............................................................................................................32 3.4.1. Đặc tả ngôn ngữ: ......................................................................................32 3.4.2. Phần thực thi:...........................................................................................33 3.5. Một số khái niệm cơ bản trong AspectJ: ..........................................................33 3.5.1. Join point .................................................................................................33 3.5.2. Pointcut....................................................................................................33 3.5.3. Advice .....................................................................................................33 3.5.4. Aspect......................................................................................................34 3.6. Cơ chế họa động của AspectJ ..........................................................................35 3.6.1. Compile – time: .......................................................................................35 3.6.2. Link – time: .............................................................................................35 3.6.3. Load – time:.............................................................................................35 3.7. Sử dụng AOP Phát triển ứng dụng và phương pháp kiểm chứng dựa trên AOP ...............................................................................................................................36 CHƯƠNG 4..............................................................................................................38 PHƯƠNG PHÁP KIỂM CHỨNG CÁC GIAO THỨC BẰNG AOP ....................38 4.1 Biểu diễn giao thức...........................................................................................38 4.2. Tiền điều kiện và hậu điều kiện : .....................................................................39 4.2.1. Tiền điều kiện : ........................................................................................39 4.2.2. Hậu điều kiện :.........................................................................................39 4.2.3 Biểu diễn tiền điều kiện và hậu điều kiện trong biểu đồ trình tự : ..............39 4.3 Kiểm chứng giao thức: .....................................................................................40 Chương 5 Xây dựng công cụ sinh mã từ máy trạng thái ......................................42 5.1 Tổng quan về xây dựng công cụ sinh mã từ máy trạng thái...............................42 5.1.1 Lấy các thành phần trong tài liệu XMI. .....................................................42 5.1.2. Sinh mã Aspect từ biểu đồ tuần tự UML ..................................................45 5.2. Sinh mã kiểm chứng giao thức AnBm .............................................................46 Chương 6 Kết luận...................................................................................................49 6.1 Kết luận về khóa luận .......................................................................................49 6.2 Hướng phát triển trong tương lai : ....................................................................50 7 Danh mục ký hiệu, từ viết tắt UML Unified Modeling Language AOP Aspect-Oriented Programming FSM Finite State Machine OOP Object Oriented Programming XML eXtensible Markup Language XMI XML Metadata Interchange DOM Document Object Model SEQUENCE DIAGRAM BIỂU ĐỒ TUẦN TỰ 8 Chương 1. Mở Đầu 1.1. Đặt vấn đề Trong những năm cuối của thế kỉ XX, nhân loại đã được chứng kiến những tiến bộ vượt bậc của các ngành khoa học công nghệ như: công nghệ điện tử, công nghệ sinh học… và một ngành công nghệ mới không thể không nhắc tới đó là ngành công nghệ thông tin. Những tiến bộ của ngành công nghệ thông tin đã giúp ích được cho con người và những ngành khoa học khác là rất lớn. Ngành công nghệ phần mềm là sự áp dụng một cách tiếp cận có hệ thống, có kỷ luật và định lượng được cho những việc phát triển, hoạt động bảo trì phần mềm. Ngành công nghệ phần mềm bao trùm các kiến thức, các công cụ, và các phương pháp cho việc định nghĩa yêu cầu phần mềm và thực hiện các tác vụ thiết kế phần mềm, xây dựng phần mềm, kiểm thử phần mềm ,bảo trì phần mềm…. Trong các giai đoạn đó, giai đoạn kiểm thử phần mềm với các chức năng kiểm tra, phát hiện và sửa lỗi phần mềm là rất quan trọng để đảm bảo chất lượng của một phần mềm. Từ thực tế cho thấy, các lỗi của phần mềm gây thiệt hại rất lớn về thời gian, tiền bạc và công sức của con người. Lỗi phần mềm được phát hiện càng muộn càng gây thiệt hại nghiêm trọng, gây tổn thất về thời gian,công sức và có thể phải xây dựng lại toàn bộ hệ thống từ đầu. Vì vậy, việc tìm ra lỗi sớm và sửa lỗi sớm là rất cần thiết khi thiết kế một hệ thống phần mềm. Kiểm chứng phần mềm là kiểm tra phần mềm có được thiết kế đúng và thực thi đúng như đặc tả yêu cầu không. Với vai trò quan trọng như vậy, giai đoạn kiểm thử trong ngành công nghệ phần mềm được sự quan tâm và tìm hiểu của nhiều nhà nghiên cứu. Trên thực tế, đa số các thao tác kiểm chứng phần mềm là dựa trên việc kiểm tra đầu vào và đầu ra của chương trình, việc kiểm tra này được thực hiện nhiều lần thủ công và cố gắng tìm ra tất cả các trường hợp cho đầu vào để xem đầu ra có được kết quả như ý không. Vì vậy, việc kiểm tra như vậy không thể đánh giá hay thẩm định được quá trình hoạt động logic của chương trình theo đúng như đặc tả ban đầu hay không. Quá trình hoạt động logic ở đây có thể là các tương tác tuần tự giữa các đối tượng, các giao thức giữa các đối tượng…. nhằm đảm bảo hơn tính đúng đắn của sản phẩm phần mềm. Trong khóa luận này tôi xin trình bày phương pháp tự động sinh mã aspect kiểm chứng đặc tả giao thức dựa trên lập trình hướng khía cạnh ( Aspect-Oriented Programming). 1.2.Bài toán Hiện nay có nhiều phương pháp để kiểm chứng phần mềm như giả lập hay kiểm chứng mô hình. Trong phạm vi bài toán được đặt ra, tôi muốn đề cập tới phương pháp kiểm chứng phần mềm dựa trên phương pháp lập trình hướng khía cạnh. Việc kiểm chứng cụ 9 thể của bài toán là kiểm chức giao thức đặc tả hoạt động của các đối tượng trong Java. Giao thức có thể được mô tả bằng tay hoặc mô tả bằng biểu đồ trạng thái. Trong cách tiếp cận này, một ứng dụng hướng đối tượng được đặc tả bằng mô hình UML và được cài đặt bằng ngôn ngữ java. Từ biểu đồ trình tự UML sẽ là đầu vào để tạo ra mã kiểm chứng aspect. Mã này được đan vào chương trình bằng công cụ AspectJ để kiểm tra hoạt động của chương trình trong thời gian chạy. Trong quá trình chạy của chương trình, các đoạn mã aspect sẽ tự động kiểm tra các giao thức và đưa ra thông báo lỗi khi có bất kì vi phạm nào xảy ra. Từ một biểu đồ tuần tự UML, xuất ra tài liệu XMI đặc tả của biểu đồ này. Tài liệu XMI này chính là đầu vào cho công cụ cần xây dựng. Dựa vào các kiến thức UML, XML tôi sẽ phân tích tài liệu XMI, sử dụng máy trạng thái (FSM) mô tả biểu đồ tuần tự UML và sinh mã aspect phục vụ kiểm chứng. Mã aspect là kết quả sau cùng của công cụ. 1.3. Tổng quan về phương pháp giải quyết bài toán Bài toán bắt đầu với đầu vào là biểu đồ tuần tự UML, biểu đồ này đã được xuất ra dưới dạng XMI, file XMI này sẽ là đầu vào cho công cụ sinh mã kiểm chứng. Trong báo cáo “Checking implementations of UML 2.0 sequence diagrams”[4] đã xây dựng được công máy trạng thái. Dựa vào máy trạng thái này, tôi đã phát triển máy trạng thái để phù hợp với bài toán đặt ra. Máy trạng thái FSM sẽ duyệt tất cả các trạng thái. Dựa vào các kiến thức về AspectJ [2,3] tôi đã tìm hiểu để xây dựng công cụ tự động sinh mã aspect. Việc xây dựng công cụ tự động sinh aspect của tôi gồm các bước : - Phát triển máy trạng thái để sử dụng theo mục đích kiểm thử. Đầu tiên, tôi sẽ phải tìm hiểu về tài liệu XMI, cách sử dụng XML DOM để đọc tài liệu XMI này để phát triển thêm các yêu cầu về xử lý tiền điều kiện và hậu điều kiện. Phát triển thêm các phương thức để tiện cho việc lấy ra các trạng thái, quản lý các trạng thái và sử lý các String, các hiển thị theo đúng mục đích. - Xây dựng chức năng tự động sinh mã aspect từ FSM : Sử dụng máy trạng thái được sinh ra, duyệt qua từng trạng thái trong FSM, áp dụng cấu trúc cú pháp cài đặt mã aspect để tạo ra mã aspect hoàn chỉnh. 1.4. Cấu trúc khóa luận Chương 1 : Mở đầu. Chương 2 : Trình bày sơ qua các kiến thức về UML,XML,XMI. Trong biểu đồ UML tôi đi tìm hiểu chi tiết về biểu đồ tuần tự và các thành phần của nó. Đây là nền tảng để tìm hiểu cách biểu diễn và hoạt động của biểu đồ. Dựa vào những kiến thức về XML,XMI giúp tôi nắm được cấu trúc tài liệu, cách thao tác, sử lý tài liệu XMI để lấy ra những thông tin cần thiết cho việc phát triển máy trạng thái FSM. 10 Chương 3 : Trình bày về aspect và lập trình hướng khía cạnh. Nêu nên những ưu điểm của AOP, vai trò của nó trong sự phát triển của ngành công nghệ phần mềm. . Những kiến thức về AOP và aspect giúp tôi tạo ra các đoạn mã aspect theo đúng cú pháp phục vụ cho việc kiểm thử. Giới thiệu về AspectJ là một cài đặt của AOP cho ngôn ngữ lập trình Java. Chương 4 : Trình bày phương pháp giải quyết bài toán kiểm chứng các giao thức bằng AOP. Chương 5: Trình bày công cụ sinh mã Aspect và mã kiểm chứng giao thức AnBm. Chương 6 : Kết luận. 11 Chương 2. Ngôn ngữ UML và biểu diễn biểu đồ trong UML bằng XMI. 2.1. Giới thiệu chung về UML: [1] Ngôn ngữ UML(Unified Modeling Language) là một loại ký pháp mô hình hướng đối tượng. Ý tưởng về đối tượng bắt nguồn từ ngôn ngữ Simula, nhưng chỉ trụ vững được từ những năm 80, với sự xuất hiện của ngôn ngữ lập trình Smalltalk và C++.Khi lập trình hướng đối tượng phát triển thì có nhu cầu về mô hình hóa hướng đối tượng.Chính vì vây, dẫn tới sự xuất hiện của các phương pháp mô hình hóa đối tượng như OOAD của Grady Booch, OMT của Jim Rumbaugh, Fusion của Derek Coleman …. Do có nhiều chuẩn dẫn tới sự phân tán không hợp lý, có nhưng khi có các sự xung đột của các phương pháp với nhau.Và xu hương nhất thiết là cần hợp nhất các phương thức này lại. Tháng 1/1994 IG.booch và J.Rumbauch bắt đầu hợp tác, nhắm xây dựng một “Phương pháp hợp nhất ” trên cơ sở hai phương pháp Booch 93 và OMT-2. Năm 1995 I.Jacobsson và các phương pháp Objectory gia nhập,và từ đó họ được các đồng nghiệp gọi là “ba người bạn”(the three amigos).Họ quyết định thu hẹp mục tiêu, nhằm thành lập mô hình hóa hợp nhất. - Tháng 6/1996 ra đời phiên bản UML 0.9. - Tháng 1/1997 IBM và Softteam kết hợp các thành viên UML để đưa ra phiên bản 1.1 - Tháng 11/1997 UML 1.1 được công nhận là chuẩn cho các ngôn ngữ mô hình hóa và trao đặc quyền xét lại (Do OMG-Object Management Group công nhận) - Tháng 6/1998 ra đời UML 1.2 - Tháng 10/1998 ra đời UML 1.3 - Tháng 5/2001 ra đời UML 1.4 - Tháng 6/2003 thông qua dự thảo UML 2.0(dự kiến phe duyệt vào cuối năm 2004) Mỗi phiên bản sau đều có sự hiệu chỉnh, bổ sung so với phiên bản trước, chẳng hạn trong phiên bản UML 1.4 có 9 loại biểu đồ nhưng trong phiên bản 2.0 có tời 13 loại biểu đồ. Tuy nhiên cần chú ý: khi xem xét tiến trình RUP, phải hiểu rằng đây là một tiến trình mang tính “tổng quát”, tức là nó có thể đem áp dụng vào mọi dự án phần mềm, vì thế rất phức tạp. Trong những dự án nhỏ, chúng ta chủ yếu sử dụng ý tưởng của RUP và một số bước nào đó. 12 Ngôn ngữ mô hình hóa thống nhất (Unifield Modeling Language – UML) là một ngôn ngữ để biểu diễn mô hình theo hướng đối tượng được xây dựng bởi ba tác giả trên với chủ đích là: - Mô hình hoá các hệ thống sử dụng các khái niệm hướng đối tượng. - Thiết lập một kết nối từ nhận thức của con người đến các sự kiện cần mô hình hoá. - Giải quyết vấn đề về mức độ thừa kế trong các hệ thống phức tạp, có nhiều ràng buộc khác nhau. - Tạo một ngôn ngữ mô hình hoá có thể sử dụng được bởi người và máy. 2.2. Các loại biểu đồ UML Về biểu đồ UML có tất cả 12 loại biểu đồ được chia ra làm hai nhóm :Nhóm các biểu đồ về cấu trúc, và nhóm các biểu đồ hành vi.(theo UML 2.0) 2.2.1. Nhóm biểu đồ về cấu trúc - Biểu đồ lớp - Biểu đồ đối tượng - Biểu đồ thành phần - Biểu đồ bố trí - Biểu đồ gói - Biểu đồ cấu trúc đa hợp 2.2.2. Nhóm biểu đồ hành vi - Biểu đồ ca sử dụng - Biểu đồ trình tự - Biểu đồ giao tiếp - Biểu đồ máy trạng thái - Biểu đồ hoạt động - Biểu đồ bao quát tương tác 2.3. Biểu đồ tuần tự trong UML2.0(Sequence diagram) Biểu đồ tuần tự là biểu đồ theo thứ tự thời gian. Biểu đồ trình tự là một trong hai biểu đồ tương tác chính, với chủ đích làm nổi bật trình tự theo thời gian của các thông điệp.Nó trình bày một một tập hợp các đối tượng và các thông điệp được trao đổi giữa chúng.Các đối tượng là các cá thể có tên hay khuyết danh của các lớp, cũng có thể là các đối tác, các hợp tác, các thành phần, các nút. Biểu đồ trình tự được trình bày theo hai chiều. - Chiều ngang bố trí các đối tượng, các đối tượng bố trí theo hình chữ nhật, hoặc bằng biểu tượng, dàn t