Luận văn Kiểm chứng đặt tả uml cho tác tử phần mềm

g hoàn chỉnh. - Thêm nữa, để quản lý trạng thái của SharedState, ta cần phải có dữ liệu của FSM mô tả biểu đồ trình tự UML. Vì vậy, trong aspect này sẽ chứa thêm phần mã nguồn tạo ra FSM từ biểu đồ trình tự UML như trong chương 4 đã trình bày. 5.4 Mở rộng Trong bài báo “Checking Interface Interaction Protocols Using Aspect-oriented Programming” [5] chưa xử lý các hàm trùng tên nhưng có các tham s ố truyền vào khác nhau hay kiểu dữ liệu trả về khác nhau và không kiểm tra điều kiện tiên quyết cần thiết trước khi hàm được gọi (precondition của hàm). Trong khóa luận của tôi, tôi đã mở rộng thêm hai phần này: - Kiểm tra precondition được mô tả trong biểu đồ trạng thái UML: Như trong phần 4.1.1, tôi có nói đến các quy tắc biểu diễn giao thức bằng biểu đồ trạng thái UML. Biểu thức điều kiện ở đây giống với biểu thức điều kiện trong mã nguồn của chương trình. Như v ậy, để kiểm tra xem có vi phạm điểu kiện hay không, tôi sẽ quy về một đoạn mã nguồn có thể là biểu thức, có thể chứa các lời gọi hàm và trả về kiểu boolean. Như vậy ta sẽ kiểm tra được vi phạm. Tuy nhiên, do việc mô tả precondition bằng cách rất hạn chế mà công cụ PVG chỉ tạo ra aspect với các mô tả có trong biểu đồ, do đó đôi khi precondition sẽ không kiểm tra được trong thực tế (ví dụ: precondition liên quan đến dữ liệu của nhiều lớp khác nhau chẳng hạn). Điều này có thể khắc phục bằng cách sửa lại mô-đun aspect do công cụ PVG tạo ra, thêm một số các đoạn mã để có thể kiểm tra được precondition trong mô-đun aspect. 52 - Thêm tham số truyền vào cho hàm: ở đây tôi sử dụng các thao tác với xâu khí tự trong Java, cắt chuỗi phương thức thành các phần nhỏ như: các chuỗi lưu tên hàm, tên tham số truyền vào, tên kiểu dữ liệu của tham số, tên tham số, kiểu giá trị trả về từ đó tạo ra các advice bằng cách thay thế các chuỗi con này vào trong các phần của aspect mẫu đã được định nghĩa từ trước. Khi cắt xâu ký tự mô tả phương thức thành nhiều phần nhỏ như vậy, việc tạo ra hai pointcut cho hai hàm trùng tên nhưng khác tham số truyền vào rất đơn giản, tôi chỉ cần thêm chuỗi mô tả kiểu của các tham số vào ngay sau xâu định nghĩa tên pointcut; như vậy sẽ giải quyết được mọi vấn đề của các hàm trùng tên, khác tham số truyền vào. 5.5 Sinh mã aspect kiểm chứng giao thức (AB)n Trong phần tìm hiểu của tôi, tôi sử dụng phương pháp tạo ra mã kiểm chứng ở trên để xây dựng thêm một chức năng khác cho công cụ “PVG”, đó là sinh mã aspect kiểm chứng giao thức (AB)n. Trong phần này tôi sẽ trình bày phần mở rộng này. 5.5.1 Giao thức (AB)n là gì? A và B là tên của các phương thức còn n là số lần các phương thức được gọi trong chương trình. Nói một cách đơn giản, (AB)n mô tả việc hàm A và B phải được gọi n lần trong mã nguồn của chương trình. Giao thức (AB)n được mô tả bằng biểu thức chính quy như sau: [A*B] n. Ở đây, * có thể là rỗng (null) hoặc là một dãy các phương thức khác. Ví dụ: - Giao thức: [void open() void close()]3 - mô tả việc gọi 3 cặp phương thức void open(), void close() trong chương trình; gi ữa hai phương thức này không có bất kỳ phương thức nào khác được gọi: - …open() close()…open() close()…open() close()… - Giao thức: [void open() * void close()]3 – mô tả việc gọi cặp hàm void open() và void close() trong chương trình như sau: - …open()…close()…open()…close()…open()…close(). Ở đây “…” đại diện cho một phương thức hay một chuỗi phương thức bất kỳ. Công cụ PVG chỉ hiểu giao thức (AB)n được định nghĩa theo đúng như biểu thức chính quy mô tả ở trên. 53 5.5.2 Thuật toán kiểm chứng giao thức (AB)n 5.5.2.1 [A * B] n Việc kiểm chứng giao thức [A * B] n nảy sinh hai vấn đề lớn: - Thứ nhất: phương thức A và B được gọi liên tiếp nhau (), tức là việc gọi hai phương thức A B phải tạo thành một dãy: A … B … A … B… Vấn đề này được giải quyết bằng một biến đếm kiểu nguyên num như sau: o Ban đầu đặt num = 0. o Trước khi gọi A, kiểm tra num, nếu num != 0 -> báo lỗi o Sau khi gọi A, tăng num lên 1. o Sau khi gọi B, giảm num đi 1. Và sau khi giảm n đi 1 kiểm tra num, nếu num != 0 -> báo lỗi. - Thứ hai: cặp (A B) được gọi đúng n lần. Việc gọi cặp (A B) đúng n lần nảy sinh ra hai trường hợp: gọi lớn hơn n lần và gọi nhỏ hơn n lần. Kiểm tra cặp A, B gọi đúng lớn hơn n lần rất đơn giản, ta cũng dùng một biến kiểu nguyên khác để kiểm tra (ví dụ: biến int count): o Sau khi gọi A, tăng biến count lên 1 và kiểm tra, nếu count > n thì báo lỗi. o Ở đây ta chỉ cần kiểm tra A có được gọi > n lần hay không mà không cần kiểm tra B vì nếu A đã được gọi > n lần thì ta đã bắt được lỗi và nếu A và B được gọi với số lần khác nhau, ta cũng đã b ắt được lỗi bằng biến num ở trên. Như vậy chỉ cần kiểm tra A là đủ. Kiểm tra (A B) được gọi < n lần khó khăn hơn, ta không thể dùng các join point tại các phương thức A và B kiểm tra được mà phải dùng một join point khác là điểm mà sau khi tất cả các hàm A, B được gọi. Để đơn giản, tôi tạo ra một phương thức mới trong mã nguồn của chương trình (void checkAnBn()). Phương thức này không ảnh hưởng gì đ ến chương trình, nó đư ợc gọi ở điểm kết thúc của chương trình. Sau khi tạo được một join point tại điểm kết thúc của chương trình thì vi ệc kiểm tra A có được gọi n lần hay không tôi cũng dùng chính ngay biến count ở trên để kiểm tra. Before advice sẽ kiểm tra xem, nếu count != n thì sẽ báo lỗi. Quay trở lại, ta có thể thấy việc tạo ra một phương thức mới làm điểm đánh dấu kết thúc chương trình sẽ giải quyết được tất cả vấn đề 54 liên quan tới việc gọi hàm A đúng n lần. Trong công cụ PVG tôi sử dụng cả hai cách đã được chỉ ra ở trên. 5.5.2.2 [A B] n [A B] n là mở trường hợp đặc biệt của [A * B] n khi * = null. Ở đây, ta phải gọi hai phương thức A, B theo một cặp (A B). Để kiểm chứng giao thức [A B] n ta cũng kế thừa từ thuật toán kiểm chứng giao thức [A * B] n, và mở rộng thêm một phần kiểm tra gọi hai phương thức A, B theo cặp (A B). Để làm được điều này, ta phải bắt được tất cả các điểm gọi hàm khác. Khi bắt được tất cả các điểm gọi hàm khác thì việc kiểm tra vi phạm sẽ rất đơn giản, ta chỉ cần dùng một biến check kiểu nguyên. Mỗi khi chương trình g ọi hàm, biến check được tăng lên 1. Sau khi chương trình gọi hàm A, biến check được đặt lại giá trị = 0. Và ta sẽ kiểm tra sau khi gọi hàm B, nếu biến check != 1 thì chương trình sẽ báo lỗi. Vì nếu check != 1 thì tức là đã có một hàm khác được gọi ở giữa A và B. 5.5.3 Sinh mã aspect kiểm chứng giao thức (AB)n Phương pháp này có ý tưởng hoàn toàn giống với phương pháp sinh aspect kiểm chứng từ biểu đồ UML, nó chỉ khác nhau ở các mẫu aspect được định nghĩa khác nhau. Đầu tiên là phân tích chuỗi [A * B] n lấy ra các phương thức A, B và biến n. Sau đó dùng các phương thức xử lý xâu ký tự, tách các hàm A, B này ra thành các phần: tên hàm, kiểu giá trị trả về, tham số… giống như khi xử lý tạo ra aspect từ biểu đồ UML. Sau đó tạo ra các aspect theo mẫu đã định nghĩa trước. 5.6 Kết luận Trong chương này, tôi đã trình bày phương pháp tự động sinh mô-đun aspect từ FSM mô tả biểu đồ UML. Nội dung chính của phương pháp chính là duyệt các trạng thái trong FSM, phân tích vào các vị trí thích hợp trong xâu aspect mẫu được khai báo từ trước. Xâu aspect mẫu sẽ tuân theo cú pháp của một aspect cơ bản, bao gồm tên aspect, vùng pointcut và vùng advice. Thuật toán duyệt các trạng thái trong máy trạng thái thực chất là việc duyệt các key của FSM, lấy dữ liệu của từng trạng thái, sử dụng các phương thức thao tác với xâu ký tự để tạo ra các aspect. Đồng thời, tôi đưa ra phương pháp kiểm chứng giao thức (AB)n – một mở rộng cho công cụ PVG có thể kiểm chứng giao thức (AB)n. Kết quả thu được sau bước này là mã aspect. Mã aspect này sẽ được đan vào chương trình chính để thực hiện chức năng kiểm chứng chương trình. 55 Chương 6. Thực nghiệm Để minh họa cho phương pháp xây dựng công cụ sinh aspect được giới thiệu trong các chương trước, chương này sẽ mô tả chi tiết các bước cài đặt mà tôi đã thực hiện và kết quả thực hiện kiểm chứng trên một số giao thức thực tế. 6.1 Xây dựng công cụ PVG Sau khi đặc tả giao thức cần kiểm chứng bằng UML, công cụ StarUML ( hỗ trợ xuất biểu đồ UML ra dạng XMI và đây chính là đầu vào cho công cụ PVG của tôi. Áp dụng phương pháp được giới thiệu ở các chương trước, tôi đã cài đ ặt thành công chương trình tự sinh mã aspect từ tài liệu XMI. Trong phương pháp này, tôi sử dụng công cụ Netbeans 6.5 với framework JDK để cài đặt công cụ. Giao diện làm việc trên Netbeans 6.5 được minh họa như sau: Hình 6.1: Cài đặt PVG bằng công cụ Netbeans 6.5 Thuật toán cơ bản của phương pháp này là việc phân tích tài liệu XMI, xây dựng các cấu trúc dữ liệu để mô tả biểu đồ UML bằng các đối tượng trong Java. Từ đó xây dựng máy trạng thái. Duyệt các trạng thái trong máy trạng thái, phân tích vào các vị trí thích hợp trong xâu aspect mẫu được khai báo từ trước. Xâu aspect mẫu sẽ tuân theo cú pháp của một aspect cơ bản, bao gồm tên aspect, vùng pointcut và vùng advice. Thuật toán duyệt các trạng thái trong máy trạng thái thực chất là việc duyệt các key của 56 FSM, lấy dữ liệu của từng trạng thái, sử dụng các phương thức thao tác với xâu ký tự để tạo ra các aspect tương ứng. Cài đặt công cụ thông qua một số bước như: - Bước 1: Tạo ra các cấu trúc dữ liệu mô tả biểu đồ trạng thái và biểu đồ trình tự UML. - Bước 2: Cài đặt thuật toán xây dựng FSM - Bước 3: Cài đặt thuật toán xây dựng bộ sinh tự động mã aspect - Bước 4: Tích hợp thành chương trình hoàn chỉnh. Hoàn tất quá trình cài đặt, tôi thu được công cụ tự sinh mã aspect kiểm chứng. 6.2 Kiểm chứng một số giao thức thực tế 6.2.1 Giao thức của các ứng dụng Applet 6.2.1.1 Giới thiệu Applet protocol Java Applet là một chương trình viết bằng ngôn ngữ Java và được kích hoạt nhờ các trình duyệt web. Hình vẽ dưới đây mô tả giao thức của các ứng dụng applet: Hình 6.2: Biểu đồ trạng thái mô tả giao thức applet Một applet thường có bốn phương thức chính: init, start, stop và destroy. - Init: Để khởi tạo applet mỗi khi applet được nạp hay được nạp lại. - Start: Kích hoạt applet bắt đầu hoạt động. - Stop: Cho phép tạm ngưng thực hiện các hoạt động của applet, nhưng có thể không hoàn trả tài nguyên hệ thống. - Destroy: Hủy applet, giải phóng tài nguyên hệ thống. 57 Các client đầu tiên sẽ gọi phương thức init, sau đó là cặp phương thức start – stop được gọi lặp đi lặp lại tùy mục đích sử dụng. Cuối cùng phương thức destroy được gọi khi client muốn hủy applet. Giao thức applet có thể được mô tả bởi biểu thức chính quy: init (start | stop) + destroy. 6.2.1.2 Kiểm chứng Applet protocol Với giao thức applet mô tả như phần trước, tôi sử dụng công cụ StarUML ( vẽ một biểu đồ trạng thái để mô tả lại giao thức applet dưới dạng biểu đồ trạng thái UML (Hình 6.2) sau đó xuất ra dạng tài liệu XMI làm đầu vào cho công cụ PVG của tôi. Lập trình viên mô tả lớp Applet gồm bốn phương thức: void init(), void start(), void stop() và void destroy(): public class Applet { public void init(){//do something} public void start(){//do something} public void stop(){//do something} public void destroy(){//do something} } Mã aspect sinh ra từ công cụ PVG: public aspect ProtocolChecker{ public final static int STATE_START = 0; public final static int STATE_destroy = STATE_START; public final static int STATE_stop = 2; public final static int STATE_start = 3; public final static int STATE_init = 4; private int state = STATE_START; /* public ProtocolChecker(){ System.out.println("Aspect instance is created: "+this); } */ pointcut pc_stop(): call (void stop()); before(): pc_stop() { if (!(state==STATE_start)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_stop() { state = STATE_stop; } pointcut pc_destroy(): call (void destroy()); before(): pc_destroy() { 58 if (!(state==STATE_stop)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_destroy() { state = STATE_destroy; } pointcut pc_init(): call (void init()); before(): pc_init() { if (!(state==STATE_START)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_init() { state = STATE_init; } pointcut pc_start(): call (void start()); before(): pc_start() { if (!(state==STATE_stop || state==STATE_init)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_start() { state = STATE_start; } } Sau khi sinh aspect kiểm chứng bằng công cụ PVG, tích hợp vào mã nguồn chương trình, tôi được kết quả kiểm thử với một số đầu vào khác nhau như sau: - CorrectTest1: o Chuỗi gọi: init(); start(); stop(); destroy(); o Kết quả: Hình 6.3: Applet – CorrectTest1 59 o Nhận xét: chuỗi gọi đúng với đặc tả giao thức, chương trình không báo lỗi. - CorrectTest2: o Chuỗi gọi: init(); start(); stop(); [start(); stop()]2 destroy(); o Kết quả: Hình 6.4: Applet – CorrectTest2 o Nhận xét: chuỗi gọi đúng với đặc tả giao thức, chương trình không báo lỗi. - WrongTest1: o Chuỗi gọi: init(); stop(); start(); destroy(); o Kết quả: Hình 6.5: Applet – WrongTest1 o Nhận xét: chuỗi gọi sai đặc tả, phương thức stop() được gọi trước phương thức start(), chương trình báo lỗi và chỉ ra dòng mã nguồn bị lỗi. - WrongTest2: o Chuỗi gọi: init(); destroy(); start(); init(); o Kết quả: 60 Hình 6.6: Applet – WrongTest2 o Nhận xét: chuỗi gọi sai đặc tả tại lời gọi ba phương thức destroy(); start(); init(); chương trình bắt được tất cả các lỗi. Như vậy, chỉ mới thực hiện bốn ca kiểm thử, ta có thể thấy rất rõ aspect do công cụ PVG tạo ra đáp ứng được yêu cầu kiểm chứng giao thức applet. Để chính xác hơn, ta hoàn toàn có thể định nghĩa các ca kiểm thử khác để kiểm chứng sự làm việc của aspect này. 6.2.2 Kiểm chứng giao thức biểu diễn giao thức ghi nợ ở một máy ATM 6.2.2.1 Đặc tả giao thức Hình 6.7: Giao thức ghi nợ đơn giản 61 Giao thức mô tả tương tác giữa hai lớp Account và DBManager. Khi một đối tượng Account gọi phương thức debit() một dãy các hàm được gọi phải tuân theo giao thức được định nghĩa để hoàn thành giao dịch: Account.debit() -> Account.getBalance() -> DBManager.queryB() -> Account.setBalance() -> DBManager.updateB(). 6.2.2.2 Kiểm chứng Mã aspect: import java.io.File; import java.util.*; import org.aspectj.lang.JoinPoint; import readXMI_SequenceDiagram.*; public aspect ProtocolChecker { int NUMBER_OF_CLASSES = 2; SharedStateManager sm = new SharedStateManager(NUMBER_OF_CLASSES); static HashMap> fsm = null; static HashSet entrySigs, exitSigs; ProtocolChecker(){ if (fsm == null) loadProtocol(); } pointcut pc_Account_debit(): call (void Account.debit()) ; before(): pc_Account_debit() { Object o = thisJoinPoint.getTarget(); if (!sm.isBinded(o)) sm.newSharedState(o); } after(): pc_Account_debit() { String s = thisJoinPoint.getSignature().toString(); Object o = thisJoinPoint.getTarget(); log("change state: " + sm.getSharedState(o).getState() + " ---> " + s); sm.setSharedState(o, s); } pointcut pc_DBManager_updateB_String(String str): args(str) && call (void DBManager.updateB(String)); before(String str): pc_DBManager_updateB_String(str) { Object o = thisJoinPoint.getTarget(); if (!sm.isBinded(o)) sm.bind(o); String s = thisJoinPoint.getSignature().toString(); if (! isValidState(o, s)) { log("Invalid change: " + sm.getSharedState(o).getState() + " ---> " + s); log(thisJoinPoint); } } after(String str): pc_DBManager_updateB_String(str){ String s = thisJoinPoint.getSignature().toString(); Object o = thisJoinPoint.getTarget(); log("change state: " + sm.getSharedState(o).getState() + " ---> " + s); if (exitSigs.contains(s)) sm.reset(o); } 62 pointcut pc_DBManager_queryB_String(String str): args(str) && call (int DBManager.queryB(String)); before (String str): pc_DBManager_queryB_String(str) { Object o = thisJoinPoint.getTarget(); if (!sm.isBinded(o)) sm.bind(o); String s = thisJoinPoint.getSignature().toString(); if (! isValidState(o, s)) { log("Invalid change: " + sm.getSharedState(o).getState() + " ---> " + s); log(thisJoinPoint); } } after(String str): pc_DBManager_queryB_String(str) { String s = thisJoinPoint.getSignature().toString(); Object o = thisJoinPoint.getTarget(); log("change state: " + sm.getSharedState(o).getState() + " ---> " + s); sm.setSharedState(o, s); } pointcut pc_Account_getBalance(): call (int Account.getBalance()); before (): pc_Account_getBalance() { Object o = thisJoinPoint.getTarget(); if (!sm.isBinded(o)) sm.bind(o); String s = thisJoinPoint.getSignature().toString(); if (! isValidState(o, s)) { log("Invalid change: " + sm.getSharedState(o).getState() + " ---> " + s); log(thisJoinPoint); } } after(): pc_Account_getBalance() { String s = thisJoinPoint.getSignature().toString(); Object o = thisJoinPoint.getTarget(); log("change state: " + sm.getSharedState(o).getState() + " ---> " + s); sm.setSharedState(o, s); } pointcut pc_Account_setBalance_int(int ba): args(ba) && call (void Account.setBalance(int)); before (int ba): pc_Account_setBalance_int(ba) { Object o = thisJoinPoint.getTarget(); if (!sm.isBinded(o)) sm.bind(o); String s = thisJoinPoint.getSignature().toString(); if (! isValidState(o, s)) { log("Invalid change: " + sm.getSharedState(o).getState() + " ---> " + s); log(thisJoinPoint); } } after(int ba): pc_Account_setBalance_int(ba) { String s = thisJoinPoint.getSignature().toString(); Object o = thisJoinPoint.getTarget(); log("change state: " + sm.getSharedState(o).getState() + " ---> " + s); sm.setSharedState(o, s); } void log(JoinPoint jp){ 63 String s = "WRONG: " + jp.getSourceLocation() + ":" + jp.getSignature(); System.out.println(s); } void log(String s) { System.out.println("INF: "+ s); } boolean isValidState(Object o, String st){ boolean b = fsm.containsKey(st); SharedState state = sm.getSharedState(o); String objState = state.getState(); if (b) b = fsm.get(st).contains(objState); return b; } public void loadProtocol(){ try{ File xmlFile = new File ("./src/model/sequence.xml"); SequenceDiagramFSM colfsm = new SequenceDiagramFSM(xmlFile); fsm = colfsm.fsm; entrySigs = colfsm.entrySigs; exitSigs = colfsm.exitSigs; } catch (Exception e) { e.printStackTrace(); } } } Tương tự như với giao thức applet. Lập trình viên sẽ xây dựng hai lớp là Account và DBManager như đã đặc tả. Mã aspect được sinh ra từ công cụ PVG sẽ được kết hợp với mã nguồn của chương trình. Sau đây là một số trường hợp kiểm chứng: - CorrecTest1: o Lời gọi hàm: Account.debit(); ccount.getBalance(); DBManager.queryB("str"); Account.setBalance(1); DBManager.updateB("str"); o Kết quả: called debit() called getBalance() called queryB() called setBalance() called updateB() o Nhận xét: chuỗi gọi hàm đúng với đặc tả giao thức, trong khi chạy không phát sinh lỗi. - WrongTest1: o Lời gọi hàm: 64 Account.debit(); DBManager.queryB("str"); Account.getBalance(); DBManager.queryB("str"); Account.setBalance(1); DBManager.updateB("str"); o Kết quả: Hình 6.8: Debit – wrongTest1 Nhật xét: Chuỗi gọi hàm sai đặc tả tại hai phương thức DBManager.queryB("str"); Account.getBalance();vì vậy khi chạy, chương trình thông báo lỗi tại vị trí gọi hai phương thức này. 6.2.3 Kiểm chứng giao thức [A*B] n Giả sử ta cần kiểm chứng giao thức được mô tả bằng biểu thức chính quy như sau: [void open() * void close()]3 Mã aspect sinh ra từ công cụ PVG: import org.aspectj.lang.JoinPoint; public aspect ABnChecker{ int num = 0; int count = 0; int number = 3; pointcut pc_open(): call (void open()); before(): pc_open() { if (num != 0){ log(thisJoinPoint); }} after(): pc_open() { count++; 65 num++; if(count > number) log(thisJoinPoint); } pointcut pc_close(): call (void close()); after(): pc_close() { num--; if(num != 0 || count > number){ log(thisJoinPoint); }} void log(JoinPoint jp){ String s = "WRONG: " + jp.getSourceLocation() + ":" + jp.getSignature(); System.out.println(s); } pointcut checkn() : call (void checkprotocolAnBn()); after(): checkn() { if(count != number){ System.out.println("protocol is false"); } } /* copy this method to source code public static void checkprotocolAnBn(){ } */ } Dưới đây là kết quả của một số ca kiểm thử được thực hiện sau khi tích hợp mã aspect vào chương trình chính: - WrongTest1: o Chuỗi gọi hàm: connectDB db = new connectDB(); db.open(); db.close(); db.open(); db.close(); o Kết quả: called open() called close() called open() called close() protocol is false - WrongTest2: o Chuỗi gọi hàm: connectDB db = new connectDB(); db.open(); db.open(); db.close(); 66 db.close(); db.open(); db.close(); o Kết quả: called open() WRONG: CheckAxBn.java:40:void connectDB.open() called open() called close() WRONG: CheckAxBn.java:41:void connectDB.close() called close() called open() called close() - Nhận xét: Cả hai ca kiểm thử, chuỗi gọi hàm đều sai với đặc tả và trong khi chạy, chương trình đều báo lỗi. 6.2.4 Kiểm chứng giao thức tương tác tác tử 6.2.4.1 Đặc tả giao thức Hình 6.9: Tương tác giữa hai tác tử Khach hang và Gio hang Hình vẽ trên mô tả kịch bản đặt hàng của khách hàng trong một hệ thống bán hàng. Có hai tác tử tham gia: Khach hang và Gio hang. Để đặt hàng, đầu tiên khách hàng gửi yêu cầu đặt hàng. Khi nhận được yêu cầu đặt hàng của khách hàng, giỏ hàng có thể chấp nhận yêu cầu, từ chối yêu cầu hoặc đưa ra một lời đề nghị sửa đổi cho 67 khách hàng. Nhận được lời đề nghị từ phía giỏ hàng, khách hàng có thể chấp nhận hoặc hủy bỏ lờ đề nghị. Sau đó, giỏ hàng có thể chấp nhận yêu cầu đặt hàng hoặc đưa ra thông báo lỗi trả về cho khách hàng. Giao thức cũng có thể định nghĩa bằng biểu đồ trạng thái UML như sau: Hình 6.9: Biểu đồ trạng thái biểu diễn giao thức tương tác tác tử Lập trình viên sẽ cài đặt agent Customer đại diện cho khách hàng có hai hành vi chính: - Gửi thông điệp yêu cầu đặt hàng. - Trả lời đề nghị từ phía giỏ hàng. Agent ShoppingCart đại diện cho agent Gio hang, cũng có hai hành vi chính: - Trả lời yêu cầu đặt hàng của khách hàng. - Gửi lời đề nghị cho khách hàng. Mã nguồn cụ thể tôi giới thiệu trong Phụ lục C và D của khóa luận. 6.2.4.2 Kiểm chứng Mã aspect sinh ra từ công cụ PVG: public aspect ProtocolChecker{ public final static int STATE_START = 0; public final static int STATE_refuseRequest = STATE_START; public final static int STATE_agreeRequest = STATE_START; public final static int STATE_sendSuggest = 2; public final static int STATE_refuseSuggest = 3; public final static int STATE_sendRequest = 3; public final static int STATE_agreeSuggest = 3; private int state = STATE_START; public ProtocolChecker(){ System.out.println("Aspect instance is created: "+this); 68 } pointcut pc_refuseSuggest(): call (void refuseSuggest()); before(): pc_refuseSuggest() { if (!(state==STATE_sendSuggest)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_refuseSuggest() { state = STATE_refuseSuggest; } pointcut pc_refuseRequest(): call (void refuseRequest()); before(): pc_refuseRequest() { if (!(state==STATE_refuseSuggest || state==STATE_sendRequest || state==STATE_agreeSuggest)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_refuseRequest() { state = STATE_refuseRequest; } pointcut pc_sendSuggest(): call (void sendSuggest()); before(): pc_sendSuggest() { if (!(state==STATE_refuseSuggest || state==STATE_sendRequest || state==STATE_agreeSuggest)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_sendSuggest() { state = STATE_sendSuggest; } pointcut pc_sendRequest(): call (void sendRequest()); before(): pc_sendRequest() { if (!(state==STATE_START)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_sendRequest() { state = STATE_sendRequest; } 69 pointcut pc_agreeSuggest(): call (void agreeSuggest()); before(): pc_agreeSuggest() { if (!(state==STATE_sendSuggest)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_agreeSuggest() { state = STATE_agreeSuggest; } pointcut pc_agreeRequest(): call (void agreeRequest()); before(): pc_agreeRequest() { if (!(state==STATE_refuseSuggest || state==STATE_sendRequest || state==STATE_agreeSuggest)){ System.out.print("Wrong at: "+thisJoinPointStaticPart.getSignature()); System.out.print(" In file: "+thisJoinPointStaticPart.getSourceLocation().getFileName()); System.out.println(" At line: "+thisJoinPointStaticPart.getSourceLocation().getLine()); }} after(): pc_agreeRequest() { state = STATE_agreeRequest; } } Tích hợp mã aspect này vào chương trình chính, tôi thực hiện một số ca kiểm thử và thu được kết quả như sau: - WrongTest1: Agent Customer gửi thông điệp trả lời đề nghị trước khi gửi thông điệp yêu cầu. o Kết quả: Hình 6.10: Agent – wrongTest1 o Nhận xét: Agent ShoppingCart vẫn xử lý yêu cầu từ phía Customer nhưng có hai dòng thông báo lỗi hiện lên báo sai đặc tả. Như vậy mã 70 aspect kiểm chứng đã phát hiện ra lỗi sai đặc tả và thông báo cho người dùng. - WrongTest2: Agent ShoppingCart gửi cả thông điệp chấp nhận đặt hàng và từ chối đặt hàng khi Customer gửi một yêu cầu đặt hàng. o Kết quả: Hình 6.11: Agent – wrongTest2 o Nhận xét: Mã aspect kiểm chứng bắt được lỗi sai đặc tả giao thức trong thời gian chạy. 6.3 Kết luận Trong chương này, tôi đã trình bày cách cài đ ặt công cụ PVG dựa vào phương pháp “kiểm chứng đặc tả UML cho tác tử phần mềm”. Mã aspect được sinh ra từ công cụ PVG sẽ được đan vào mã ngu ồn của chương trình chính thông qua trình biên d ịch AspectJ để kiếm chứng giao thức đặc tả trong thời gian chạy. Bước đầu tiến hành kiểm chứng một số giao thức thực tế, tôi thấy mã aspect do công cụ PVG tạo ra đã đáp ứng được các yêu cầu kiểm chứng. 71 Chương 7. Kết luận 7.1 Kết luận về khóa luận Trong quá trình thực hiện khóa luận này, tôi đã tìm hiểu những kiến thức cơ bản về kiểm chứng phần mềm – là một trong những công đoạn vô cùng quan trọng giúp phát hiện và sửa lỗi phần mềm nhằm đảm bảo chất lượng phần mềm. Đồng thời tôi đã xây dựng phương pháp kiểm chứng phần mềm dựa trên AOP từ đó xây dựng công cụ tự động sinh mô-đun kiểm chứng. Trong phương pháp kiểm chứng các đặc tả giao thức cho ứng dụng, các mô-đun aspect chứa mã kiểm chứng sẽ là các mô-đun cắt ngang hệ thống và tách biệt so với chương trình ban đầu. Từ biểu đồ trạng thái hay biểu đồ trình tự UML, AUML đặc tả giao thức, tôi xuất biểu đồ này ra dạng tài liệu XMI. Tiếp đó tiến hành phân tích tài liệu XMI để xây dựng máy trạng thái mô tả giao thức đã đư ợc định nghĩa. Từ máy trạng thái xây dựng được, tôi tiến hành duyệt các trạng thái của máy trạng thái và dùng các thuật toán thao tác với xâu ký tự để sinh ra mã aspect chứa nội dung kiểm chứng. Áp dụng tư tưởng của phương pháp này, tôi đã phát tri ển thêm phương pháp kiểm chứng cho giao thức (AB)n. Để minh họa cho phương pháp “kiểm chứng đặc tả UML cho tác tử phần mềm”, tôi đã th ực nghiệm và xây dựng thành công khi cài đặt được công cụ Protocol Verification Generator tự động sinh mã aspect từ tài liệu XMI mô tả giao thức. Tuy nhiên, tôi cũng v ấp phải một số khó khăn trong quá trình xây d ựng phương pháp sinh mã aspect. Tác tử phần mềm có thể tự đưa ra các hành động tùy vào sự thay đổi của môi trường nên khi hệ thống chứa càng nhiều tác tử thì đặc tả giao thức sẽ càng khó khăn; mặt khác công cụ PVG chỉ sinh ra aspect từ những thông tin trong tài liệu XMI. Chính vì vậy việc xây dựng các mô-đun kiểm chứng chỉ từ tài liệu XMI biểu diễn giao thức nhiều khi là không đủ để sinh ra các mô-đun aspect kiểm chứng hoàn chỉnh. Hơn nữa, hệ thống đa tác tử, chứa càng nhiều tác tử thì việc đặc tả sẽ càng gặp khó khăn vì các dữ liệu trong biểu đồ UML đặc tả giao thức phải giống với trong mã nguồn của chương trình. Một khó khăn nữa là các biểu đồ UML rất hạn chế trong việc đặc tả các biểu thức điều kiện, chính vì vậy đôi khi ta chỉ kiểm chứng được một vài nhánh của chương trình mà không thể kiểm chứng được tất cả các nhánh. 72 7.2 Hướng phát triển trong tương lai Từ những vấn đề tồn tại của khóa luận này, trong tương lai tôi sẽ tiếp tục hướng nghiên cứu này nhằm xây dựng hoàn thiện công cụ Protocol Verification Generator để đáp ứng mọi yêu cầu. Hướng nghiên cứu gần nhất là phát triển công cụ để PVG để có giải quyết triệt để các giao thức ràng buộc phức tạp như tiền điều kiện, hậu điều kiện, giao thức AnBn, giao thức AnBf(n) trong đó f(n) là một hàm nào đó phụ thuộc vào n, giao thức AnBmCf(n,m) trong đó f(n,m) là hàm phụ thuộc vào n và m. Bên cạnh đó, tôi sẽ nghiên cứu và tìm ra các phương pháp sinh mã aspect ki ểm chứng không chỉ phụ thuộc vào tài liệu XMI mà còn phụ thuộc vào các ràng buộc điều kiện được đặc tả bởi các dạng dữ liệu khác nhằm tăng tính ứng dụng của công cụ PVG đối với công nghệ sản xuất phần mềm hiện nay. 73 Phụ lục Phụ lục A: Tài liệu XMI mô tả biểu đồ trạng thái UML <XMI xmi.version = "1.1" xmlns:UML="href://org.omg/UML/1.3" timestamp = "Mon May 18 17:41:3 2009"> StarUML.XMI-Addin 1.0 <UML:Model xmi.id="UMLModel.2" name="Dummy Model" visibility="public" isSpecification="false" namespace="UMLProject.1" isRoot="false" isLeaf="false" isAbstract="false"> <UML:Model xmi.id="UMLModel.3" name="Model1" visibility="public" isSpecification="false" namespace="UMLModel.2" isRoot="false" isLeaf="false" isAbstract="false"> <UML:StateMachine xmi.id="UMLStateMachine.4" name="StateMachine1" visibility="public" isSpecification="false" context="UMLModel.3"> <UML:CompositeState xmi.id="UMLCompositeState.5" name="TOP" visibility="public" isSpecification="false" stateMachine="UMLStateMachine.4" isConcurrent="false"> <UML:Pseudostate xmi.id="UMLPseudostate.6" name="Initial" visibility="public" isSpecification="false" container="UMLCompositeState.5" outgoing="UMLTransition.11" kind="initial"/> <UML:SimpleState xmi.id="UMLCompositeState.7" name="State1" visibility="public" isSpecification="false" container="UMLCompositeState.5" outgoing="UMLTransition.12" incoming="UMLTransition.11"/> <UML:SimpleState xmi.id="UMLCompositeState.8" name="State2" visibility="public" isSpecification="false" container="UMLCompositeState.5" outgoing="UMLTransition.13" incoming="UMLTransition.12 UMLTransition.14"/> <UML:SimpleState xmi.id="UMLCompositeState.9" name="State3" visibility="public" isSpecification="false" container="UMLCompositeState.5" outgoing="UMLTransition.14 UMLTransition.15" incoming="UMLTransition.13"/> <UML:FinalState xmi.id="UMLFinalState.10" name="FinalState" visibility="public" isSpecification="false" container="UMLCompositeState.5" incoming="UMLTransition.15"/> 74 <UML:Transition xmi.id="UMLTransition.11" name="void init()" visibility="public" isSpecification="false" stateMachine="UMLStateMachine.4" source="UMLPseudostate.6" target="UMLCompositeState.7"/> <UML:Transition xmi.id="UMLTransition.12" name="void start(int a, int b)" visibility="public" isSpecification="false" stateMachine="UMLStateMachine.4" source="UMLCompositeState.7" target="UMLCompositeState.8"> <UML:BooleanExpression xmi.id="X.17" body="a >= b"/> <UML:Transition xmi.id="UMLTransition.13" name="void stop()" visibility="public" isSpecification="false" stateMachine="UMLStateMachine.4" source="UMLCompositeState.8" target="UMLCompositeState.9"/> <UML:Transition xmi.id="UMLTransition.14" name="void start()" visibility="public" isSpecification="false" stateMachine="UMLStateMachine.4" source="UMLCompositeState.9" target="UMLCompositeState.8"/> <UML:Transition xmi.id="UMLTransition.15" name="void destroy()" visibility="public" isSpecification="false" stateMachine="UMLStateMachine.4" source="UMLCompositeState.9" target="UMLFinalState.10"/> 75 Phụ lục B: Tài liệu XMI mô tả biểu đồ trình tự UML <XMI xmi.version = "1.1" xmlns:UML="href://org.omg/UML/1.3" timestamp = "Mon May 18 17:44:49 2009"> StarUML.XMI-Addin 1.0 <UML:Model xmi.id="UMLModel.2" name="Model1" visibility="public" isSpecification="false" namespace="UMLProject.1" isRoot="false" isLeaf="false" isAbstract="false"> <UML:Collaboration xmi.id="UMLCollaborationInstanceSet.3" name="CollaborationInstanceSet1" visibility="public" isSpecification="false"> <UML:Interaction xmi.id="UMLInteractionInstanceSet.4" name="InteractionInstanceSet1" visibility="public" isSpecification="false" context="UMLCollaborationInstanceSet.3"> <UML:Message xmi.id="UMLStimulus.5" name="debit" visibility="public" isSpecification="false" sender="UMLObject.15" receiver="UMLObject.15" interaction="UMLInteractionInstanceSet.4"> <UML:CallAction xmi.id="UMLCallAction.6" name="" visibility="public" isSpecification="false" isAsynchronous="false" stimulus="UMLStimulus.5"/> <UML:Message xmi.id="UMLStimulus.7" name="getBalance" visibility="public" isSpecification="false" sender="UMLObject.15" receiver="UMLObject.16" interaction="UMLInteractionInstanceSet.4"> <UML:CallAction xmi.id="UMLCallAction.8" name="" visibility="public" isSpecification="false" isAsynchronous="false" stimulus="UMLStimulus.7"/> <UML:Message xmi.id="UMLStimulus.9" name="queryB" visibility="public" isSpecification="false" sender="UMLObject.16" receiver="UMLObject.16" interaction="UMLInteractionInstanceSet.4"> <UML:CallAction xmi.id="UMLCallAction.10" name="" visibility="public" isSpecification="false" isAsynchronous="false" stimulus="UMLStimulus.9"/> <UML:Message xmi.id="UMLStimulus.11" name="setBalance" visibility="public" isSpecification="false" sender="UMLObject.15" receiver="UMLObject.16" interaction="UMLInteractionInstanceSet.4"> 76 <UML:CallAction xmi.id="UMLCallAction.12" name="" visibility="public" isSpecification="false" isAsynchronous="false" stimulus="UMLStimulus.11"/> <UML:Message xmi.id="UMLStimulus.13" name="updateB" visibility="public" isSpecification="false" sender="UMLObject.16" receiver="UMLObject.16" interaction="UMLInteractionInstanceSet.4"> <UML:CallAction xmi.id="UMLCallAction.14" name="" visibility="public" isSpecification="false" isAsynchronous="false" stimulus="UMLStimulus.13"/> <UML:ClassifierRole xmi.id="UMLObject.15" name="Account" visibility="public" isSpecification="false" message2="UMLStimulus.5 UMLStimulus.7 UMLStimulus.11" message1="UMLStimulus.5" isRoot="false" isLeaf="false" isAbstract="false"> <UML:MultiplicityRange xmi.id="X.26" lower="1" upper="1" multiplicity="X.25"/> <UML:ClassifierRole xmi.id="UMLObject.16" name="DBManager" visibility="public" isSpecification="false" message2="UMLStimulus.9 UMLStimulus.13" message1="UMLStimulus.7 UMLStimulus.9 UMLStimulus.11 UMLStimulus.13" isRoot="false" isLeaf="false" isAbstract="false"> <UML:MultiplicityRange xmi.id="X.28" lower="1" upper="1" multiplicity="X.27"/> <UML:TaggedValue xmi.id="X.17" tag="return" value="void" modelElement="UMLStimulus.5"/> <UML:TaggedValue xmi.id="X.18" tag="return" value="int" modelElement="UMLStimulus.7"/> <UML:TaggedValue xmi.id="X.19" tag="arguments" value="String str" modelElement="UMLStimulus.9"/> <UML:TaggedValue xmi.id="X.20" tag="return" value="int" modelElement="UMLStimulus.9"/> 77 <UML:TaggedValue xmi.id="X.21" tag="arguments" value="int ba" modelElement="UMLStimulus.11"/> <UML:TaggedValue xmi.id="X.22" tag="return" value="void" modelElement="UMLStimulus.11"/> <UML:TaggedValue xmi.id="X.23" tag="arguments" value="String str" modelElement="UMLStimulus.13"/> <UML:TaggedValue xmi.id="X.24" tag="return" value="void" modelElement="UMLStimulus.13"/> 78 Phụ lục C: Agent Customer (Customer.java) import jade.core.Agent; import jade.core.AID; import jade.core.behaviours.Behaviour; import jade.lang.acl.ACLMessage; import jade.proto.AchieveREInitiator; import jade.domain.FIPANames; import java.util.Date; import java.util.Vector; public class Customer extends Agent { private int nResponders; static String str = ""; static String request = "true"; protected void setup() { // Read name of ShoppingCart as arguments final Object[] args = getArguments(); if(args != null && args.length > 0) { nResponders = args.length; System.out.println("Requesting dummy-action to "+nResponders+" responders."); // Gui REQUEST final ACLMessage msg = new ACLMessage(ACLMessage.REQUEST); msg.addReceiver(new AID((String) args[0], AID.ISLOCALNAME)); msg.setProtocol(FIPANames.InteractionProtocol.FIPA_REQUEST); // We want to receive a reply in 10 secs msg.setReplyByDate(new Date(System.currentTimeMillis() + 10000)); msg.setContent(request); //agreeSuggest(); sendRequest(); // AddBehavior addBehaviour(new AchieveREInitiator(this, msg) { protected void handleInform(ACLMessage inform) { String tmp = inform.getContent(); if(tmp.equals("suggest")) { //agreeSuggest(); refuseSuggest(); ACLMessage msg1 = new ACLMessage(ACLMessage.REQUEST); msg1.addReceiver(new AID((String) args[0], AID.ISLOCALNAME)); msg1.setProtocol(FIPANames.InteractionProtocol.FIPA_REQUEST); // We want to receive a reply in 10 secs msg1.setReplyByDate(new Date(System.currentTimeMillis() + 10000)); msg1.setContent(request); sendRequest(); addBehaviour(new AchieveREInitiator(myAgent, msg1) { protected void handleInform(ACLMessage inform) { 79 System.out.println("Agent "+inform.getSender().getName()+" successfully performed the requested action"); } protected void handleRefuse(ACLMessage refuse) { System.out.println("Agent "+refuse.getSender().getName()+" refused to perform the requested action"); } protected void handleFailure(ACLMessage failure) { if (failure.getSender().equals(myAgent.getAMS())) { // FAILURE notification from the JADE runtime: the receiver // does not exist System.out.println("Responder does not exist"); } else { System.out.println("Agent "+failure.getSender().getName()+" failed to perform the requested action"); } } protected void handleAllResultNotifications(Vector notifications) { if (notifications.size() < nResponders) { // Some responder didn't reply within the specified timeout System.out.println("Timeout expired: missing "+(nResponders - notifications.size())+" responses"); } } }); // AddBehavior } else { System.out.println("Agent "+inform.getSender().getName()+" dat hang thanh cong"); } } protected void handleRefuse(ACLMessage refuse) { System.out.println("Agent "+refuse.getSender().getName()+" khong chap nhan"); nResponders--; } protected void handleFailure(ACLMessage failure) { if (failure.getSender().equals(myAgent.getAMS())) { // FAILURE notification from the JADE runtime: the receiver // does not exist System.out.println("Agent Giohang khong hoat dong"); } else { System.out.println("Agent "+failure.getSender().getName()+" loi trong xu ly yeu cau"); } 80 } protected void handleAllResultNotifications(Vector notifications) { if (notifications.size() < nResponders) { // Some responder didn't reply within the specified timeout System.out.println("Timeout expired: missing "+(nResponders - notifications.size())+" responses"); } } }); } else { System.out.println("Khong co Agent ShoppingCart nao fuc vu"); } } static void sendRequest() { System.out.println("called sendRequest"); } static void agreeSuggest() { System.out.println("agreeSuggest"); request = "true"; } static void refuseSuggest() { System.out.println("refuseSuggest"); request = "false"; } } 81 Phụ lục D: Agent ShoppingCart (ShoppingCart.java) import jade.core.Agent; import jade.core.AID; import jade.lang.acl.ACLMessage; import jade.lang.acl.MessageTemplate; import jade.proto.AchieveREResponder; import jade.domain.FIPANames; import jade.domain.FIPAAgentManagement.NotUnderstoodException; import jade.domain.FIPAAgentManagement.RefuseException; import jade.domain.FIPAAgentManagement.FailureException; public class ShoppingCart extends Agent{ protected void setup() { System.out.println("Agent "+getLocalName()+" waiting for requests..."); MessageTemplate template = MessageTemplate.and( MessageTemplate.MatchProtocol(FIPANames.InteractionProtocol.FIPA_REQUEST), MessageTemplate.MatchPerformative(ACLMessage.REQUEST) ); addBehaviour(new AchieveREResponder(this, template) { protected ACLMessage prepareResponse(ACLMessage request) throws NotUnderstoodException, RefuseException { System.out.println("Agent "+getLocalName()+": REQUEST received from "+request.getSender().getName()+". Action is "+request.getContent()); String strReq = request.getContent(); if(strReq.equals("true")) { System.out.println("Agent "+getLocalName()+": Agree"); ACLMessage agree = request.createReply(); agree.setPerformative(ACLMessage.AGREE); agree.setContent("ok"); agreeRequest(); return agree; } else if (strReq.equals("suggest")) { System.out.println("Agent "+getLocalName()+": Agree"); ACLMessage agree = request.createReply(); agree.setPerformative(ACLMessage.AGREE); agree.setContent("suggest"); sendSuggest(); return agree; } else { refuseRequest(); System.out.println("Agent "+getLocalName()+": Refuse"); throw new RefuseException("check-failed"); } 82 } }); } static void sendSuggest() { System.out.println("ShoppingCart gui mot loi de nghi cho Customer"); } static void agreeRequest() { System.out.println("ShoppingCart Chap nhan yeu cau dat hang"); } static void refuseRequest() { System.out.println("ShoppingCart Tu choi dat hang"); }} 83 Phụ lục E: Aspect Template static String aspectTemplate = "\r\n" + " pointcut pc_$METHODNAME$($METHOD_ARG$): $ARGS$ call ($METHOD_RETURN$ $METHOD_NAME$($METHOD_ARG_TYPE$));\r\n" + " before($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " if ($PRE-CONDITIONS$){\r\n" + " System.out.print(\"Wrong at: \"+thisJoinPointStaticPart.getSignature());\r\n"+ " System.out.print(\" In file: \"+thisJoinPointStaticPart.getSourceLocation().getFileName());\r\n"+ " System.out.println(\" At line: \"+thisJoinPointStaticPart.getSourceLocation().getLine());\r\n"+ " }}\r\n" + " after($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " state = STATE_$METHOD_STATE_NAME$;\r\n" + " }\r\n"; static String strPointcutEntry = " pointcut pc_$METHODNAME$($METHOD_ARG$): $ARGS$ call ($METHOD_RETURN$ $METHOD_NAME$($METHOD_ARG_TYPE$)) ;\r\n" + " before($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " Object o = thisJoinPoint.getTarget();\r\n"+ " if (!sm.isBinded(o)) \r\n"+ " sm.newSharedState(o);\r\n"+ " }\r\n" + " after($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " String s = thisJoinPoint.getSignature().toString();\r\n" + " Object o = thisJoinPoint.getTarget();\r\n" + " log(\"change state: \" + sm.getSharedState(o).getState() + \" ---> \" + s); \r\n" + " sm.setSharedState(o, s);\r\n" + " }\r\n"; static String strPointcutExit = " pointcut pc_$METHODNAME$($METHOD_ARG$): $ARGS$ call ($METHOD_RETURN$ $METHOD_NAME$($METHOD_ARG_TYPE$));\r\n" + " before($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " Object o = thisJoinPoint.getTarget();\r\n" + " if (!sm.isBinded(o))\r\n"+ " sm.bind(o);\r\n" + " String s = thisJoinPoint.getSignature().toString();\r\n"+ " if (! isValidState(o, s)) {\r\n" + " log(\"Invalid change: \" + sm.getSharedState(o).getState() + \" ---> \" + s); \r\n" + " log(thisJoinPoint);\r\n" + " }\r\n"+ " }\r\n" + " after($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$){\r\n" + " String s = thisJoinPoint.getSignature().toString();\r\n" + " Object o = thisJoinPoint.getTarget();\r\n" + " log(\"change state: \" + sm.getSharedState(o).getState() + \" ---> \" + s); \r\n" + " if (exitSigs.contains(s))\r\n" + 84 " sm.reset(o);\r\n" + " }\r\n"; static String strPointcut = " pointcut pc_$METHODNAME$($METHOD_ARG$): $ARGS$ call ($METHOD_RETURN$ $METHOD_NAME$($METHOD_ARG_TYPE$));\r\n" + " before ($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " Object o = thisJoinPoint.getTarget();\r\n" + " if (!sm.isBinded(o))\r\n"+ " sm.bind(o);\r\n" + " String s = thisJoinPoint.getSignature().toString();\r\n"+ " if (! isValidState(o, s)) {\r\n" + " log(\"Invalid change: \" + sm.getSharedState(o).getState() + \" ---> \" + s); \r\n" + " log(thisJoinPoint);\r\n" + " }\r\n"+ " }\r\n" + " after($METHOD_ARG$): pc_$METHODNAME$($METHOD_ARG_NAME$) {\r\n" + " String s = thisJoinPoint.getSignature().toString();\r\n" + " Object o = thisJoinPoint.getTarget();\r\n" + " log(\"change state: \" + sm.getSharedState(o).getState() + \" ---> \" + s); \r\n" + " sm.setSharedState(o, s);\r\n" + " }\r\n"; Tài liệu tham khảo [1] [2] [3] [4] A. Colyer, A. Clement, G. Harley and M. Webster. Eclipse AspectJ: Aspect- Oriented Programming with AspectJ and the Eclipse AspectJ Development Tools. Addison Wesley Professional Publisher, 2004. [5] Anh-Hoang Truong, Thanh-Binh Trinh, Dang Van Hung, Viet-Ha Nguyen, Nguyen Thi Thu Trang, and Pham Dinh Hung. “Checking Interface Interaction Protocols Using Aspect-Oriented Programming”. SEFM' 08, Cape Town, South Africa, November 10-14, 2008. [6] David Hunter, Kurt Cagle, Chris Dix, Roger Kovack, Jonathan Pinnock, Jeff Rafter. Beginning XML, 4th edition. Wiley Publishing Inc, 2007. [7] J. D. Gradecki and N. Lesiecki. Mastering AspectJ Aspect-Oriented Programming in Java. Wiley Publishing Inc, 2003. [8] James Odell, H. Van Dyke Parunak, Bernhard Bauer. Representing Agent Interaction Protocols in UML , 1999. [9] James Odell, H. Van Dyke Parunak, Bernhard Bauer. Extending UML for Agents, 2000. [10] M. Wooldridge, N. Jennings, D. Kinny: The Gaia Methodology for Agent- Oriented Analysis and Design. Autonomous Agents and Multi-Agent Systems. 3 (3): (2000). [11] OMG. Unified Modeling Language. OMG Version 1.5 – 2003. [12] R. Laddad. AspectJ in Action Practical Aspect-Oriented Programming. Manning Publications Co., 2003. [13] R. S. Pressman. Software Engineering, A Practitioner’s Approach, 5th edition. Thomas Casson, 2001. [14] Timothy J. Grose, Gary C. Doney, Stephen A. Brodsky. Mastering XMI: Java Programming with XMI, XML, and UML. Wiley Publishing Inc,2002. [15] Y. Cheon and A. Perumandla. Specifying and checking method call sequences of Java programs. Software Quality Control, 15(1):7–25, 2007.