Khóa luận Mô hình hóa các hệ thống dựa trên các thành phần

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nguyễn Văn Nghiệp MÔ HÌNH HÓA CÁC HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN 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 - 2009 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nguyễn Văn Nghiệp MÔ HÌNH HÓA CÁC HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN 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: TS. Đặng Văn Hưng HÀ NỘI - 2009 TÓM TẮT NỘI DUNG KHÓA LUẬN Mục đích của khóa luận là nghiên cứu và tìm hiểu các khái niệm liên quan đến thành phần phần mềm, hệ thống dựa trên thành phần và hệ thống dựa trên thành phần thời gian thực. Đầu tiên tôi sẽ trình bày tổng quan về việc xây dựng hệ thống dựa trên thành phần và các lợi ích của nó trong việc phân tích, thiết kế các hệ thống thông tin. Tôi sẽ trình bày việc mô hình hóa hình thức hệ thống dựa trên thành phần dựa trên nền tảng của UTP (Unifying Theory of Programming). Tôi sẽ trình bày về các khái niệm trong mô hình hệ thống dựa trên thành phần như: giao diện, hợp đồng, thành phần, kết hợp thành phần. Các định nghĩa này sẽ đóng vai trò nền tảng cho việc phát triển các khuôn mẫu cho thành phần. Một hợp đồng được định nghĩa sẽ bao hàm đặc tả của các phương thức, một thành phần được định nghĩa là một cài đặt của một hợp đồng. Cài đặt này có thể yêu cầu các dịch vụ từ các thành phần khác với một vài giả thiết về lập lịch cho việc giải quyết xung đột các phương thức dùng chung và sử dụng các tài nguyên hiện có trong xử lí song song. Trong khóa luận tôi sẽ trình bày sâu hơn về mô hình thành phần thời gian thực dựa trên các khái niệm, các định nghĩa đã được nêu ra trước đó. Với phần này, tôi đưa ra một mô hình giao diện thành phần cho hệ thống dựa trên thành phần thời gian thực. Cùng với đó, đặc tả phương thức sẽ được mở rộng với một ràng buộc về thời gian là một quan hệ giữa tài nguyên có sẵn và lượng thời gian tiêu tốn để thực thi phương thức. Với mô hình đó, nó hỗ trợ sự phân tách giữa yêu cầu chức năng, yêu cầu phi chức năng và kiểm chứng hợp phần hình thức của hệ thống dựa trên thành phần thời gian thực. Cuối cùng tôi cho một ví dụ minh họa cho mô hình được nghiên cứu trong luận văn này. LỜI CẢM ƠN. Em xin chân thành cảm ơn các thầy giáo, cô giáo trong khoa đã giúp đỡ em trong thời gian học tập tại khoa để em có những kiến thức nền tảng cho việc nghiên cứu khoa học để áp dụng vào việc nghiên cứu những lý thuyết, kiến thức liên quan đến đề tài khóa luận tốt nghiệp. Đặc biệt, em xin gửi lời cảm ơn sâu sắc đến Tiến sĩ Đặng Văn Hưng, người đã luôn quan tâm, giúp đỡ, hướng dẫn em trong suốt quá trình nghiên cứu và trình bày khóa. Thầy đã giúp em rất nhiều trong việc tiếp cận các vấn đề mà em còn chưa hiểu rõ, thầy luôn nhiệt tình chỉ dạy cho em những kinh nghiệm quý báu khi tiếp cận các vấn đề mới. Em cũng xin cảm ơn tới gia đình. Gia đình là nguồn lực động viên em khi làm khóa luận này. Sinh viên Nguyễn Văn Nghiệp MỤC LỤC LỜI MỞ ĐẦU ................................................................................................................1 1. TỔNG QUAN VỀ HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN ...................3 1.1. Hệ thống dựa trên thành phần là gì?................................................................3 1.1.1. Thành phần phần mềm. .........................................................................................3 1.1.2. Hệ thống dựa trên thành phần ..............................................................................4 1.2. Hệ thống thời gian thực là gì? ...........................................................................6 2. KIẾN TRÚC HỆ THỐNG DỰA TRÊN THÀNH PHẦN......................................7 3. TÌM HIỂU MÔ HÌNH THÀNH PHẦN ..................................................................8 3.1 Thiết kế dưới dạng công thức logic....................................................................8 3.2 Giao diện và hợp đồng ........................................................................................9 3.3. Kết hợp hợp đồng. ............................................................................................11 4. MÔ HÌNH THÀNH PHẦN THỜI GIAN THỰC.................................................18 4.1. Các thiết kế có nhãn ràng buộc về thời gian sử dụng như dịch vụ..............18 4.2. Sử dụng các ngôn ngữ hình thức có nhãn ràng buộc về thời gian để đặc các giao thức tương tác thời gian thực và đặc tả tiến trình. ......................................22 4.3. Các hợp đồng thời gian thực. ..........................................................................23 4.4. Thành phần bị động .........................................................................................25 4.5. Thành phần chủ động ......................................................................................28 5. ỨNG DỤNG MÔ HÌNH THÀNH PHẦN TRONG HỆ THỐNG NHÚNG .......30 KẾT LUẬN ..................................................................................................................33 BẢNG KÍ HIỆU, VIẾT TẮT = Bằng P Q∧ P và Q P Q∨ P hoặc Q P¬ Phủ định P P Q⇒ Nếu P thì Q :x T P∃ • Tồn tại x trong tập T sao cho P :x T P∀ • Mọi x trong T sao cho P ∈ Thuộc ∉ Không thuộc {} Tập rỗng { }a Tập đơn chứa duy nhất phần tử a { : | ( )}x T P x Tập hợp tất cả x trong T sao cho P(x) { ( ) : | ( )}f x T P x Tập hợp giá trị của hàm f(x) sao cho P(x) S T∪ S hợp T S T∩ S giao T \S T S trừ T S T⊆ S chứa trong T S T⊇ S chứa T Dãy rỗng a Dãy chứa duy nhất a ok Chương trình đã khởi động ok′ Chương trình đạt đến trạng thái ổn định [ ]P Q⇒ P bao hàm Q mọi nơi P Q⊢ Quan hệ ok P ok Q′∧ ⇒ ∧ P Q⊒ P là một bản làm mịn của Q có nghĩa là [ ]P Q⇒ ( , ) ( )s P t,Q⊑ ( , )t Q được làm mịn từ ( , )s P ||P Q Phân tách hợp phần song song của P và Q M Hợp phần song song với toán tử M :x e= Gán giá trị e cho biến x. 1 LỜI MỞ ĐẦU Từ khi máy tính được phát minh, chế tạo thành công, con người đã được hưởng những thành quả của khoa học máy tính. Các hệ thống thông tin được xây dựng nhằm giúp cho việc tính toán trở nên nhanh chóng và hiệu quả hơn. Các chương trình phần mềm được thiết kế và cài đặt với mục đích hỗ trợ tốt hơn cho con người trong nhu cầu công việc hàng ngày. Ban đầu, công việc thiết kế, lập trình các hệ thống chưa được hỗ trợ nhiều. Từ việc lập trình bằng ngôn ngữ máy đến lập trình bằng ngôn ngữ bậc cao. Con người tiếp cận lập trình hướng cấu trúc với cách thể hiện phù hợp với kiến trúc máy tính thời điểm đó. Và sau đó là tiến thêm một bước nữa trong việc phát triển các hệ thống thông tin, đó là lập trình hướng đối tượng. Bằng việc sử dụng các lớp, các đối tượng trong lập trình, các hệ thống được xây dựng lên đã trở nên linh hoạt hơn, đáp ứng được như cầu sử dụng. Trước những phát triển không ngừng của công nghệ phần mềm, một mô hình hệ thống mới đã được nghiên cứu, phát triển. Đó là mô hình hệ thống dựa trên thành phần. Ngày nay, kĩ thật sử dụng hướng đối tượng và dựa trên thành phần ngày càng trở nên phổ biến và sử dụng rộng rãi trong việc mô hình hóa và thiết kế các hệ thống phần mềm phức tạp. Chúng cung cấp sự hỗ trợ có hiệu quả tới sự phân hoạch một ứng dụng vào trong những đối tượng và những thành phần, mà có thể được hiểu rõ bằng việc sử dụng lại và mở rộng những thiết kế và những cài đặt hiện có. Những phân tích và kiểm chứng các hệ thống đó cũng có thể dễ dàng hơn vì kiến trúc hợp thành phần hợp thành. Với sự ra đời của hướng nghiên cứu mới này, các hệ thống được xây dựng dễ dàng hơn, linh hoạt hơn rất nhiều. Đặc biệt, các hệ thống có tính bảo mật hiệu quả cao hơn rất nhiều so với các mô hình đã được nghiên cứu và phát triển trước đây. Nguyên tắc cơ bản của hệ thống dựa trên thành phần là cắm và chạy (plug and play) nên hệ thống là tổ hợp của rất nhiều thành phẩn. Hệ thống có thể mở rộng, bảo trì một cách dễ dàng. Hiện có các kĩ thuật hướng đối tượng và dựa trên thành phần đã được phát triển từ lâu như như CORBA, EJB, J2EE. Nhưng ngày nay, các ngôn ngữ mô hình hóa hình thức và nửa hình thức đang trở nên phổ biến và hỗ trợ phát triển hệ thống dựa trên mô hình như UML, JML, Alloy và BIP. Tiếp cận với xu hướng đó, khóa luận này xin được trình bày một số khái niệm về hệ thống dựa trên thành phần, các khái niệm cụ thể hơn trong mô hình hệ thống dựa trên thành phần thời gian thực. Bên cạnh đó, khóa luận sẽ đi sâu tìm hiểu về mô hình hệ thống dựa trên thành phần từ việc tìm hiểu mô hình thành phần. Sau khi nghiên cứu 2 các khái niệm đó, tôi sẽ trình bày về một ví dụ áp dụng mô hình này vào trong một hệ thống thực tế. Do thời gian và trình độ của sinh việc còn hạn chế nên trong khi trình bày và tìm hiểu các khái niệm chưa được thấu đáo. Khóa luận sẽ không tránh được một số lỗi. Rất mong nhận được sự đóng góp của đọc giả để sinh viên có được những kinh nghiệm trong việc nghiên cứu các vấn đề mang tính khoa học sau này. 3 1. TỔNG QUAN VỀ HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN 1.1. Hệ thống dựa trên thành phần là gì? 1.1.1. Thành phần phần mềm. Ngày nay, hầu hết các sản phẩm công nghiệp đều làm từ các thành phần cơ khí. Ví dụ như ô tô được lắp ráp từ động cơ, bánh xe, ghế ngồi… Còn với máy tính thì lại được lắp ráp từ bộ vi xử lí, ổ cứng, bộ nhớ trong (RAM), CD-Rom… Việc lắp ráp các thành phần cơ bản để tạo thành một sản phẩm hay đồ vật đã được loài người sử dụng từ hàng ngàn năm trước. Đối với ngành công nghiệp phần mềm, việc xây dựng các sản phẩm phần mềm từ các thành phần phần mềm (viết tắt là thành phần) cơ bản (Component) được áp dụng từ khá sớm. Theo G. Goos và C. Szyperski thì thành phần phần mềm là thành phần cơ bản được chỉ rõ bằng hợp đồng cho phần mềm mà có thể sẵn sàng được triển khai bởi bên thứ ba không có hiểu biết về cấu trúc bên trong của nó. Ta có thể tham khảo một mô hình của thành phần UML. Hình 1. Mô hình thành phần UML Các đặc trưng chính của thành phần được chỉ ra là: • Tính đóng gói • Xác định duy nhất • Khả năng sử dụng lại • Sẵn sàng để sử dụng • Nhiều dạng thể hiện • Giao diện • Client anonymity Bên cạnh đó, thành phần còn có các đặc tính khác như: • Độc lập về ngôn ngữ • Độc lập về nền tảng • Khả năng cấu hình 4 Hình 2: Tính đóng gói của thành phần Ta có thế có một sự so sánh giữa thành phần và lớp như sau: Thành phần (Component) Lớp (Class) • Có khả năng cung cấp dịch vụ trong quá trình hoạt động của hệ thống • Có thể chứa nhiều lớp • Mô tả bằng các giao diện • Không có mã lệnh (hộp đen) • Được phát triển riêng rẽ • Ngữ cảnh phát triển thay đổi sau khi biên dịch • Thực thể thời gian thiết kế (Design - time) • Mã lệnh có sẵn (Hộp trắng) • Trong hầu hết các trường hợp được thiết kế cho một hệ thống • Ngữ cảnh phát triển không thay đổi được sau khi biên dịch Sự khác biệt đã được thể hiện rõ trong bảng so sánh ở trên. Thành phần cho thấy sự linh động, tính đóng gói của nó. Nó có thể chạy trên nhiều hệ thống, nền tảng mà không gặp nhiều trở ngại lớn. Trong khi đó, lớp lại trở nên kém hiệu quả hơn, hạn chế trong nhiều trường hợp. 1.1.2. Hệ thống dựa trên thành phần Hệ thống dựa trên thành phần được xây dựng cơ bản từ các thành phần thương mại dựng sẵn (COTS components). Xây dựng hệ thống từ nhiều thành phần COTS giới thiệu kỹ thuật mới để giải quyết các vấn đề cốt lõi trong sự tiến hóa không đồng nhất và độc lập của các thành phần này. Với phát biểu trên, hệ thống dựa trên thành phần đem lại nhiều lợi ích cho người phát triển hệ thống. Các lợi ích đó được liệt kê dưới đây. 5 • Việc sử dụng các thành phần riêng biệt nên các thành phần được phát triển độc lập. Điều đó làm cho hình thành một thư viện các thành phần. Từ thư viện thành phần đó dẫn đến việc phát triển các hệ thống trở nên nhanh chóng. Bên cạnh đó, các thành phần này được kiểm chứng tính đúng đắn, kiểm thử các lỗi logic, … nên hạn chế được rủi ro cho hệ thống. Đây là một thế mạnh mà các hệ thống khác khó đạt được. • Các thành phần được tái sử dụng một cách hiệu quả. Mỗi lần phát triển một hệ thống mới không cần phải phát triển lại hoàn toàn mới các thành phàn mà vẫn có thể sử dụng các thành phần đã có để phát triển tiếp. Kết thúc quá trình phát triển hệ thống mới, các thành phần mới được đưa vào thư việc thành phần. Với việc tái sử dụng thanh phần, giá thành sẽ được giảm đi một cách đáng kể. Không những vậy, chất lượng cũng được nâng cao, đảm bảo yêu cầu của người sử dụng. Hình 3. Mô hình tái sử dụng thành phần • Dễ dàng bảo trì là một lợi ích rất làm cho hệ thống thành phần trở nên linh hoạt hơn. Các thành phần được phát triển riêng biệt nên khi bảo trì, toàn bộ hệ thống không bị ảnh hưởng nhiều, vẫn có thể hoạt động gần như bình thường. 6 • Tính cấu hình được của chương trình đem lại một thế mạnh về khả năng mở rộng hệ thống dễ dàng. Một hệ thống thông minh đòi hỏi phải có khả năng thay đổi cấu hình để phù hợp với ngữ cảnh. • Sự độc lập ngôn ngữ của các bộ phận trong hệ thống mới. Với các phương pháp phát triển hệ thống truyền thống thì các bộ phận của mộ hệ thống phải được phát triển trên cùng một ngôn ngữ lập trình. Nhưng với sự ra đời của phương pháp phát triển hệ thống dựa trên thành phần, các thành phần có thể được viết bằng các ngôn ngữ khác nhau. Bởi vì các thành phần tương tác với nhau bằng giao diện và hợp đồng. Vấn đề này sẽ được đề cập rõ hơn trong các phần sau. 1.2. Hệ thống thời gian thực là gì? Hệ thống thời gian thực là hệ thống mà các dịch vụ của các thành phần phải thỏa mãn ràng buộc về thời gian. Ví dụ Hệ hướng dẫn lái xe. Hệ thống này sẽ được làm rõ hơn trong phần 5 của khóa luận 7 2. KIẾN TRÚC HỆ THỐNG DỰA TRÊN THÀNH PHẦN Với định nghĩa của một hệ thống hướng thành phần như trên, kiến trúc của hệ thống dựa trên thành phần bao gồm các thành phần độc lập và giao tiếp với nhau qua các giao diện giao tiếp. Sự kết hợp đó sẽ tạo thành một hệ thống lớn. Hệ thống dựa trên thành phần được chia làm 2 phần: phần bị động và phần chủ động. Phần bị động: là một tổ hợp các thành phần liên kết với nhau. Phần chủ động: là một tập hợp các tiến trình phản ứng lại các tác động được gây ra từ các sự kiện bên ngoài. Chúng sử dụng các dịch vụ từ thành phần bị động để đáp ứng lại yêu cầu từ các tác nhân bên ngoài hệ thống thông qua giao diện thành phần. Kiến trúc của hệ thống được mô tả trong hình dưới. Hình 4: Kiến trúc hệ thống dựa trên thành phần. Đối với kiến trúc này, ta có thể lấy một ví dụ đối với các chương trình đa luồng (như chương trình Java). Ở đây, mỗi một tiến trình tương ứng với một luồng trong Java với thiết lập đa luồng được chập nhận. Điều đó có nghĩa là nhiều luồng được truy cập đến một dịch vụ của một thành phần con trong phần bị động một cách trực tiếp hoặc thông qua các dịch vụ khác. Làm thế nào để xử lý các trường hợp này để tăng hiệu suất và đặc biệt là tránh bế tắc từ các truy cập đồng thời tới các tài nguyên dùng chung là một vấn đề lớn. Nếu điều này xảy ra thì ngay cả tiền điều kiện của một dịch vụ được thỏa mãn thì dịch vụ cũng không thể ngắt vì dịch vụ đã rơi vào trạng thái bế tắc. Vì thế, không phải tất cả các hành vi truy cập dịch vụ liên tiếp đều được chấp nhận. Ngoài đặc tả với tiền điều kiện và hậu điều kiện của một dịch vụ ra, một hợp đồng cũng phải được bao gồm trong 8 đặc tả của việc cho phép truy cập dịch vụ liên tục. Đặc tả này cũng đóng vai trò như là một giả thiết rằng thành phần tạo nên môi trường cho chính nó,được ghi nhận bởi một giao thức gọi là giao thức tương tác. 3. TÌM HIỂU MÔ HÌNH THÀNH PHẦN 3.1 Thiết kế dưới dạng công thức logic Như đã nói ở phần trước, một thành phần cung cấp các dịch vụ cho các khách hàng. Các dịch vụ có thể dữ liệu hoặc các phương thức. Để xác định các chức năng cho các phương thức, ta sử dụng các kí hiệu UTP (Unified Theories of Programming) cơ bản, trong đó một phương thức được xác định như là có quan hệ với nhau với các dấu hiệu của dạng thức ( , )op in out với in và out là tập hợp các biến. Định nghĩa 1 Một thiết kế là một tập hợp hữu hạn , FPα với α là biểu thị cho tập hợp các biến chương trình được sử dụng bới phương thức, FP biểu thị cho đặc tả chức năng của phương thức trong bảng kí hiệu của UTP. • FP là một vị từ của dạng thức: Nếu điều khiển chuyển đến chương trình (ok là true) và tiền điều kiện p được thỏa mãn thì chương trình sẽ kết thúc tương ứng với ok’ là true và giá trị của biến chương trình tại thời điển kết thúc và thời điểm khởi hành thỏa mãn quan hệ R. Với p là tiền điều kiện của phương thức là giả thiết trên giá trị ban đầu của các biến trong tập hợp \ outα mà các phương thức có thể dựa vào khi kích hoạt và R là hậu điều kiện R bài liên quan đến quan sát ban đầu đến quan sát cuối cùng(được đại diện bởi những biến đầu tiên trong tập hợp { | \ ( )}x x in outα′ ∈ ∪ và các biến in out). Biến logic ok là biến đặc biệt biểu thị sự kết thúc của phương thức, ví dụ ok có giá trị true nếu và chỉ nếu phương thức bắt đầu chạy và ok′ có giá trị true nếu và chỉ nếu phương thức ngắt. Làm mịn thiết kế. Ta gọi lại định nghĩa làm mịn quan hệ cho thiết kế được trình bày trong UTP. Một thiết kế 1 1,D FPα= là được làm mịn từ thiết kế 2 2,D FPα= (có nghĩa là 1 2D D⊑ ) nếu và chỉ nếu 9 2 1( , , , )ok ok v v FP FP′ ′∀ • ⇒ với ,v v′ là các vectơ của các biến chương trình. Dãy thành phần Lấy 1 1,D FPα= và 2 2,D FPα= là các thiết kế sau đó 1 2; ,D D FPα≙ Với 1 2( ) ( )FP m FP m FP m∃ • ∧≙ với giả sử là 1 1( )FP FP v= và 2 2( )FP FP v= . Từ đây về sau, tôi sử dụng 1[ \ ]F x x để biểu diễn biểu thức kết quả từ việc thay thế x bởi x1 trong biểu thức F. 3.2 Giao diện và hợp đồng Chữ kí cho thành phần là giao diện của nó mà chỉ rõ những dịch vụ nào nó cung cấp và dịch vụ nào nó yêu cầu từ môi trường. Hợp đồng là đặc tả của giao diện. Từ thảo luận không chính thức trong phần trước, ta đưa ra định nghĩa chính thức của hai khái niệm trong lập trình dựa trên thành phần sau đây. Định nghĩa 2: Một giao diện là một cặp ( , )p rI I I= với ,p p pI Fd Md= và , r r r I Fd Md= . Ip được gọi là cung cấp giao diện của I và Ir được gọi là yêu cầu giao diện của I. Định nghĩa 3: Một hợp đồng là một tập hợp hữu hạn , , , , ,Prp rI Init MSpec Inv Inv o với • ( , )p rI I I= là một giao diện. Lấy ,r p r pMd Md Md Fd Fd Fd= ∪ = ∪ • Init là một khởi tạo mà kết hợp với mỗi biến trong Fd và mỗi biến cục bộ với một giá trị của cùng kiểu. • MSpec là đặc tả phương thức kết hợp với mỗi phương thức ( , )op in out trong r pMd Md Md= ∪ với một thiết kế , FPα với ( \ ( )) pin out Mdα ∪ ⊆ • Invp và Invr là vị từ trong cung cấp tính năng và yêu cầu tính năng tương ứng trong hợp đồng (được gọi là hợp đồng bất biến). Invp đại diện cho một thuộc tính của giá trị biến trong khai báo đặc tính FDp mà có thể dựa 10 vào trong bất kì thời điểm nào mà nó có khả năng truy cập từ các thành phần khác. Do vậy, Invp được thỏa mãn nhất là bởi Init. Invr đại diện cho thuộc tính mà yêu cầu giá trị của biến trong FDr mà được cung cấp. • Pro là một giao thức, là tập con của dạng thức { ?, !| }* { ?, !| }*p rm m m Fd m m m Fd∈ ∪ ∈ . Chỉ có hành vi của các phép chiếu trên { ?, !| }*pm m m Fd∈ và { ?, !| }*rm m m Fd∈ thuộc về Pro là được chấp nhận. Hợp đồng của một thành phần biểu diễn cái mà thành phần mong đợi từ môi trường và cái nó cung cấp cho môi trường. Các biến trong Fd là chỉ đọc đối với các hợp đồng khác. Invp trong một hợp đồng biểu diễn một thuộc tính của các biến trong hợp đồng mà nó cung cấp cho môi trường, và do vậy phải được đảm bảo bởi bất kì phương thức nào của hợp đồng. Có lẽ nó kém rõ ràng hơn một giao thức, và cách nó quan hệ với đặc tả của các dịch vụ. Ta cũng làm rõ khái niệm này như là một phần của nghiên cứu. Đối với phương thức m, kí hiệu ?m và !m như là sự dẫn ra (gán giá trị cho tham số) và kết thúc (lấy kết quả dịch vụ) của m. Ở đây sử dụng CSP (truyền thông liên tiến trình - Communicating Sequential Processes1). Sau đó nó yêu cầu mỗi ?m phải tương ứng với chính xác một !m theo sau, và ngược lại mỗi !m phải tương ứng đúng với một yêu cầu hành động !m. Đối với một phương thức m, nó có thể chấp nhận một vài luồng để sử dụng m tại cùng một thời điểm (ví dụ như vài bản sao của m). Trong trường hợp này, đối với một ?m và và tương ứng với !m có thể có vài xuất hiện của ?m giữa chúng. Số tối đa của các yêu cầu ?m không kết thúc tương ứng tại một thời điểm là độ đồng thời mà m có thể cung cấp và được chỉ rõ trong giao thức. Bình thường, bất kì phương thức m chỉ có thể được sử dụng lẫn nhau không bao gồm chính nó và các phương thức khác trong thành phần. Trong trường hợp này, giao thức có thể được chỉ ra như là một biểu thức chính quy {? ! | }*m m m Md∈ . Khi tất cả các phương thức m có thể được sử dụng lẫn nhau không bao gồm chính nó và song song với các phương thức khác, giao thức có thể được chỉ ra như là một biểu thức chính quy {? ! }*m Md m m∈ với biểu diễn sự chèn vào song song toán tử hợp. Định nghĩa 4: 1 Wikipedia, 11 Hợp đồng 1 1 1 1 1 1 1 1( , ), , , , ,p r p rCtr I I MSpec Init Inv Inv Pro= được làm mịn của đồng 2 2 2 2 2 2 2 2( , ), , , , ,p r p rCtr I I MSpec Init Inv Inv Pro= được biểu diễn là 1 2Ctr Ctr⊑ nếu và chỉ nếu: • 1 2p pFd Fd⊆ , 1 2r rFd Fd⊆ , và 2 1 1 1p pInit Fd Init Fd= với hàm f và một tập hợp A, f A biểu diễn cho sự thu hẹp (hạn chế) của f trên A. • 1 2p pMD Md⊆ và 1 2r rMD Md⊆ . • Đối với tất cả phương thức op được khai báo trong 1pMd thì 1 2( ) ( )MSpec op MSpec op⊑ và 2 1p pInv Inv⇒ . • Đối với tất cả phương thức op được khai báo trong 2rMd thì 2 1( ) ( )MSpec op MSpec op⊑ và 1 2r rInv Inv⇒ . • 1 1 2 1{ ?, !| } { ?, !| }p pPro m m m Fd Pro m m m Fd∈ ⊆ ∈ và 2 2 1 2{ ?, !| } { ?, !| }r rPro m m m Fd Pro m m m Fd∈ ⊆ ∈ . Ta chứng tỏ định nghĩa này như sau. Ctr2 cung cấp tất cả các dịch vụ mà Ctr1 cung cấp, thậm chí còn tốt hơn và có thể cung cấp nhiều hơn, Ctr2 nên cần ít các dịch vụ hơn Ctr1. Điều kiện 1 2r rInv Inv⇒ nói lên rằng thuộc tính của các biến đảm bảo bởi Ctr2 cũng chắc chắn như bởi Ctr1. Trong phần tóm tắt, hợp đồng Ctr2 cung cấp nhiều hơn, các dịch vụ tốt hơn và cần ít hơn các dịch vụ từ môi trường so với Ctr1. Do vậy, ta dùng Ctr2 để thay thế Ctr1 mà không mất bất kì dịch vụ nào. 3.3. Kết hợp hợp đồng. Các hợp đồng cáo thể được kết hợp lại theo nhiều cách để hình thành một hợp đồng mới. Một cách khó khăn hơn cho việc tính toán một hợp đồng đa hợp là tính toán về giao thức của nó. Điều này đã được loại bỏ trong lí thuyết hợp đồng. Cách đơn giản nhất để kết hợp hai hợp đồng là đặt chúng cạnh nhau nếu chúng có các tập hợp đặc tính và các phương thức rời nhau. Định nghĩa 5 12 Lấy ( , ), , , , , , 1,2i pi ri i i pi ri iCtr I I MSpec Init Inv Inv Pro i= = , là 2 hợp đồng có những tập hợp (yêu cầu và cung cấp) thuộc tính, phương thức riêng biệt. Phép kết hợp của Ctr1 và Ctr2 là hợp đồng 1 2 1 2 1 2 1 2 1 1 2 2 1 2 ( , ), , , , , ( ) p p r r p p r r 1 2 1 2 I I I I MSpec MSpec Init Init Inv Ctr Ctr Inv Inv Inv Pro Pro Pro Pro ∪ ∪ ∪ ∪ ∪ ∪ = ∪ ∪ ∪ Chỉ một điều cần thiết để giải thích trong định nghĩa trên là làm thế nào để giao thức cho hợp các hợp đồng được định nghĩa. Khi đặt các hợp đồng cạnh nhau, bởi vì chúng được giả định là độc lập, tất cả các phương thức và đặc tính của chúng có thể được sử dụng song song. Thành phần song song 1 2Pro Pro đã xác định chính xác vấn đề. Tuy nhiên, hợp đồng ghép cũng phải cho phép các phương thức trong một thành phần độc lập được sử dụng theo cách nguyên bản. Có một cách khác để kết hợp hợp đồng là kết nối các phương thức được yêu cầu của một hợp đồng đến với các phương thức cung cấp của hợp đồng khác. Lấy ( , ), , , , , , 1,2i pi ri i i pi ri iCtr I I MSpec Init Inv Inv Pro i= = là các hợp đồng có các tập hợp đặc tính và phương thức cung cấp phù hợp, các đặc tính và phương thức yêu cầu phù hợp, ví dụ như 1 2( )p pf Fd Fd∈ ∩ suy ra 1 2( ) ( )Init f Init f= và 1 2 1 2( ) ( )p p r rop Md Md Md Md∈ ∩ ∪ ∩ suy ra 1 2( ) ( )MSpec op MSpec op⇔ . Giả định rằng 1 2r pI I⊆ , 2 1p rInv Inv⇒ , 1 2( ) ( )MSpec op MSpec op⊑ đối với tất cả 1rop Md∈ . Cắm đầy đủ của 1Ctr tới 2Ctr được biểu diễn là 1 2Ctr Ctr>> được định nghĩa là: 1 2 2 2 1 2 1 1 2 1 2 2, ( , ), , , , p p r r p p r I I I MSpec Ctr Ctr Init Fd Init Inv Inv Inv Pro ∪ >> = ∧⊎ Ở đây, ta nhận thấy tập các yêu cầu không phải là 1 2r rI I∪ mà chỉ là 2rI bởi vì do 2Ctr được làm mịn từ 1Ctr nên 2Ctr có đầy đủ tập các yêu cầu của 1Ctr . Và vì thế, 1Ctr cắm đầy đủ vào 2Ctr . Với 1 2( )( )Init Init x⊎ được định nghĩa là 13 1 2 1 2 1 1 2 2 2 1 ( ) ( ) nê'u ( ) ( ) ( ) nê'u ( ) \ ( ) ( ) nê'u ( ) \ ( ) Init x Init x x dom Init dom Init Init x x dom Init dom Init Init x x dom Init dom Init = ∈ ∩  ∈  ∈ Ta thảo l