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

Nội dung text: Luận văn Mô hình hóa các hệ thống dựa trên các thành phần

1. ĐẠ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
2. ĐẠ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
3. 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.
4. 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
5. 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
6. 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 | Px ( )} Tập h ợp t ất c ả x trong T sao cho P(x) {f (): x T | Px ()} 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 ⊢
7. 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.
8. 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 1
9. 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. 2
10. 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 • Nhi ều d ạng th ể hi ện • Xác định duy nh ất • Giao di ện • Kh ả n ăng s ử d ụng l ại • Client anonymity • Sẵn sàng để s ử d ụng 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 3
11. 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 • Th ực th ể th ời gian thi ết k ế (Design quá trình ho ạt độ ng c ủa h ệ th ống - time) • Có th ể ch ứa nhi ều l ớp • Mã l ệnh có s ẵn (H ộp tr ắng) • Mô t ả b ằng các giao di ện • Trong h ầu h ết các tr ường h ợp được thi ết k ế cho m ột h ệ th ống • Không có mã l ệnh (h ộp đen) • Ng ữ c ảnh phát tri ển không thay đổ i • Được phát tri ển riêng r ẽ được sau khi biên d ịch • Ng ữ c ảnh phát tri ển thay đổ i 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. 4
12. • 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. 5
13. • 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 6
14. 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 7
15. đặ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 ế D1, FP 1 là được làm m ịn t ừ thi ết k ế D2, FP 2 (có ngh ĩa là D1⊑ D 2 ) n ếu và ch ỉ n ếu 8
16. ∀′ ′ • ⇒ (,,,okok vv FP2 FP 1 ) 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 D1, FP 1 và D2, FP 2 là các thi ết k ế sau đó D1; D 2 ≙ , FP ∃ • ∧ = = Với FP≙ m FP1() m FP 2 () m v ới gi ả s ử là FP1 FP 1 ( v ) và FP2 FP 2 ( v ) . Từ đây v ề sau, tôi s ử d ụng F[ x1 \ 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 I( Ip , I r ) v ới Ip Fd p, Md p và = Ir Fd r, Md r . I p được g ọi là cung c ấp giao di ện c ủa I và I r đượ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 I, Init , MSpec , Invp , Inv r ,Pr o v ới • = =∪ =∪ I( Ip , I r ) là m ột giao di ện. L ấy Md Mdr Md p, Fd Fd rp 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 ứcop( in , out ) = ∪ α trong Md Mdr Md p v ới m ột thi ết k ế , FP v ới α ∪ ⊆ ( \ (in out )) Md p • Inv p và Inv r 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). Inv p đại di ện cho một thu ộc tính c ủa giá tr ị bi ến trong khai báo đặ c tính FD p mà có th ể d ựa 9
17. 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, Inv p được th ỏa mãn nh ất là b ởi Init. Inv r đại di ện cho thu ộc tính mà yêu c ầu giá tr ị c ủa bi ến trong FD r mà được cung c ấp. • Pro là m ột giao th ức, là t ập con c ủa d ạng th ức ∈ ∪ ∈ {?,!|mmmFdp }*{?,!| mmmFd r }* . Ch ỉ có hành vi c ủa các ∈ ∈ phép chi ếu trên {?,!|m m m Fd p }* và {?,!|m m m Fd r }* 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. Inv p 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 Processes 1). 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, 10
18. = Hợp đồ ng Ctr1(,), Ipr 11 I MSpec 11111 , Init , Inv pr , Inv , Pro được làm m ịn c ủa = đồng Ctr2(,), Ipr 22 I MSpec 22222 , Init , Inv pr , Inv , Pro được bi ểu di ễn là Ctr1⊑ Ctr 2 n ếu và ch ỉ n ếu: • ⊆ ⊆ = Fdp1 Fd p 2 , Fdr1 Fd r 2 , và Init2 Fdp 1 Init 1 Fd p 1 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. • ⊆ ⊆ MDp1 Md p 2 và MDr1 Md r 2 . • Đối v ới t ất c ả ph ươ ng th ức op được khai báo trong Md p1 thì ⇒ MSpec1() op⊑ MSpec 2 () op và Invp2 Inv p 1 . • Đối v ới t ất c ả ph ươ ng th ức op được khai báo trong Md r 2 thì ⇒ MSpec2() op⊑ MSpec 1 () op và Invr1 Inv r 2 . • ∈ ⊆ ∈ Pro1{?,!| m m m Fdp 12 } Pro {?,!| m m m Fd p 1 } và ∈ ⊆ ∈ Pro2{?,!| m m m Fdr 21 } Pro {?,!| m m m Fd r 2 } . Ta ch ứng t ỏ đị nh ngh ĩa này nh ư sau. Ctr 2 cung c ấp t ất c ả các d ịch v ụ mà Ctr 1 cung c ấp, th ậm chí còn t ốt h ơn và có th ể cung c ấp nhi ều h ơn, Ctr 2 nên c ần ít các d ịch ⇒ vụ h ơn Ctr 1. Điều ki ện Invr1 Inv r 2 nói lên r ằng thu ộc tính c ủa các bi ến đả m b ảo bởi Ctr 2 c ũng ch ắc ch ắn nh ư b ởi Ctr 1. Trong ph ần tóm t ắt, h ợp đồ ng Ctr 2 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 Ctr 1. Do vậy, ta dùng Ctr 2 để thay th ế Ctr 1 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 11
19. = = Lấy Ctri(,), I pi I ri MSpec i , Init i , Inv pi , Inv ri , Pro i ,1,2 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 Ctr 1 và Ctr 2 là h ợp đồ ng ∪∪ ∪ ∪ ∪ (Ip1212 I p , I r I r ), MSpec 1 MSpec 21 , Init Init 21 , Inv p Ctr∪ Ctr = 1 2 ∪ ∪ ∪ Invpr2, Inv 1 Inv r1 2 , Pro Pro 2 () Pro 12 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 Pro1 Pro 2 đã 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 = = Ctri(,), I pi I ri MSpec i , Init i , Inv pi , Inv ri , Pro i ,1,2 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 ư f( Fdp1 Fd p 2 ) suy ra Init1() f Init 2 () f và ∈ ∩ ∪ ∩ ⇔ op( Mdp1 Md p 2 )( Md r 1 Md r 2 ) suy ra MSpec1() op MSpec 2 () op . Gi ả ⊆ ⇒ định r ằng Ir1 I p 2 , Invp2 Inv r 1 , MSpec1() op⊑ MSpec 2 () op đối v ới t ất c ả ∈ op Md r1 . >> Cắm đầy đủ c ủa Ctr 1 t ới Ctr 2 được bi ểu di ễn là Ctr1 Ctr 2 được đị nh ngh ĩa là: ∪ (Ip1 I p 22 , I r ), MSpec 2 , Ctr>> Ctr = 1 2 ∧ Init11 Fdr⊎ Init 2, Inv ppr 1 Inv 2 , Inv 2, Pro ∪ Ở đây, ta nh ận th ấy t ập các yêu c ầu không ph ải là Ir1 I r 2 mà ch ỉ là Ir 2 b ởi vì do Ctr 2 được làm m ịn t ừ Ctr 1 nên Ctr 2 có đầy đủ t ập các yêu c ầu c ủa Ctr 1. Và vì th ế, Ctr 1 c ắm đầ y đủ vào Ctr 2 . Với (Init1⊎ Init 2 )( x ) được đị nh ngh ĩa là 12
20. = ∈ ∩ Init12() x Init () x nê'u x domInit ( 1 ) domInit ( 2 )  ∈ Init1() x nê'u x domInit ( 1 )\ domInit ( 2 )  ∈ Init2() x nê'u x domInit ( 2 )\ domInit ( 1 ) = Ta th ảo lu ận ở đây cách mà giao th ức Pro được tính toán t ừ Proi , i 1,2 v ới >> hợp đồ ng Ctr1 Ctr 2 . • >> Th ứ nh ất, hợp đồ ng ghép Ctr1 Ctr 2 c ũng ph ải cho phép các ph ươ ng th ức của m ột thành ph ần riêng bi ệt được s ử d ụng chúng theo cách nguyên b ản. ∪ Vậy Pro1 Pro 2 ph ải bao g ồm Pro . • Các ph ươ ng th ức m t ừ Ctr 2 thì không được yêu c ầu b ởi Ctr 1 có th ể được s ử dụng song song v ới các ph ươ ng th ức trong Ctr 1. V ậy Pro ph ải bao g ồm ∩ ∈ Pro( Pro2 {!,?| m m m Md p2 \ Md r 1 }*) . • ∩ Câu h ỏi ở đây là làm th ế nào mà m ột ph ươ ng th ức m trong Mdp2 Md r 1 l ại được s ử d ụng v ới m ột ph ươ ng th ức trong Md p1 . Câu tr ả l ời ph ụ thu ộc vào độ song song c ủa m. Vi ệc tính toán cho tr ường h ợp này r ất ph ức t ạp và được để mở t ại đây. Để an toàn, ta không cho phép chúng ch ạy song song (mặc dù nh ư v ậy thì hi ệu qu ả kém h ơn). Vậy ta đị nh ngh ĩa Pro nh ư sau: =∪∪ ∩ ∈ Pro Pro1 Pro 2 Pro 1 (Pr o2 {! m ,? mm | Mdp 2 \ Md r 1 }*) >> Khi Ctr1 Ctr 2 được đị nh ngh ĩa, ta nói r ằng Ctr 1 có kh ả n ăng k ết n ối v ới Ctr 2 . Chú ý r ằng khi kết h ợp hai h ợp đồ ng theo cách này thì thành ph ần k ết qu ả có th ể không được s ử d ụng để thay th ế Ctr 1. Lí do là nó có th ể yêu c ầu cái gì đó t ừ môi tr ường mà Ctr 1 không cung c ấp. Định lí 1 = ∅ Lấy Ctr 1 là kh ả k ết n ối v ới Ctr 2 . N ếu Ctr 2 là đóng (có ngh ĩa là Ir 2 ) thì >> Ctr1⊑ ( Ctr 1 Ctr 2 ) . Ch ứng minh: 13
21. Bằng vi ệc ki ểm tra tr ực ti ếp t ừ đị nh ngh ĩa c ủa toán t ử cắm(plug operator) và định ngh ĩa c ủa làm m ịn thi ết k ế. Định ngh ĩa có th ể được ch ỉnh s ửa trong tr ường h ợp ph ổ bi ến là Ir1 I p 2 và lí thuy ết v ẫn đúng. Bây gi ờ hãy hình th ức hóa khái ni ệm c ủa thành ph ần. B ằng tr ực giác, m ột thành ph ần b ị độ ng là m ột cài đặt c ủa m ột giao di ện s ử d ụng dịch v ụ t ừ các thành ph ần b ị độ ng khác thông qua các h ợp đồ ng c ủa chúng. V ới m ột trình bày đơ n gi ản, ta s ử d ụng m ột ki ểu ki ến trúc đơn gi ản v ới kh ởi t ạo ch ủ/khách và truy ền thông đồ ng b ộ. Định ngh ĩa 6 Một thành ph ần b ị độ ng là m ột t ập h ợp h ữu h ạn Comp= Ctr, Mcode v ới Comp được xác đị nh v ới tên c ủa thành ph ần g ồm có: • = Một h ợp đồ ng Ctr(,), Ipr I MSpec , Init , Inv pr , Inv , Pro • Mcode gán m ỗi ph ươ ng th ức op trong Md p m ột thi ết k ế xây d ựng t ừ các toán t ử c ơ b ản và ph ươ ng th ức trong Ir nh ư là ánh x ạ c ủa các v ết trong thi ết ∈ kế này mà b ấy kì op Md r được thay th ể b ởi ?op ! op t ừ b ắt đầu và k ết thúc ∈ hành động, {?!|m m m Md r } được bao g ồm trong Pro . Điều ki ện sau đây ph ải được th ỏa mãn b ởi Mcode : (MSpec ( op )⊑ Mcode ( op )) và Inv p được gi ữ b ởi b ất kì phép toán nào trong Mcode . • Cài đặt c ủa t ất c ả ph ươ ng th ức m ph ải t ươ ng thích v ới độ song song c ủa chúng được mô t ả trong Pro , ngh ĩa là ho ặc m ột ph ươ ng th ức m không ph ải là m ột ph ươ ng th ức đặ c bi ệt dùng chung ho ặc m ột s ố b ản sao thích h ợp c ủa m tồn t ại. Thành ph ần b ị độ ng Comp được nói là cài đặt b ởi Ctr . Vậy m ột thành ph ần ph ải được ki ểm ch ứng b ởi thi ết k ế c ủa nó. Ví d ụ nh ư cài đặt của các ph ươ ng th ức ph ải được ki ểm ch ứng thông qua các đặ c t ả c ủa chúng. Tính đúng đắn c ủa nó có th ể được ki ểm ch ứng riêng bi ệt t ừ môi tr ường. = = >> Lấy Compi Ctr i, Mcode i , i 1,2 là các thành ph ần, v ới Ctr1 Ctr 2 được ′ định ngh ĩa. L ấy được Mcode t ừ Mcode 1 b ằng vi ệc thay th ế m ỗi l ần xu ất hi ện c ủa ∈ ∩ op( Mdr1 Md p 2 ) b ằng Mcode2 ( op ) trong dãy c ủa Mcode 1 . Th ật d ễ dàng để 14
22. ki ểm tra toàn b ộ toán t ử cắm định ngh ĩa trong các h ợp đồ ng được mang theo trên các thành ph ần. Định lí 2: >>′ ∪ Ctr1 Ctr 2, Mcode 1 Mcode 221 Md \ Md là m ột thành ph ần. Ví d ụ: L ấy double_ quadr là m ột thành ph ần v ới m ột d ịch v ụ dquadr(: in real a,,; b c out : real x 1) mà đư a ra là m ột đáp án x1 c ủa ph ươ ng trình bậc 2 theo x2: ax4+ bx 2 + c = 0 . Thành ph ần double_ quadr yêu c ầu d ịch v ụ dquadr(: in real a,,; b c out : real x 1) t ừ thành ph ần khác mà khi được g ọi v ới các tham s ố a, b, c thích h ợp thì s ẽ tr ả l ại đáp án c ủa ph ươ ng trình ax2 + bx + c = 0 . Thành ph ần double_ quadr được mô t ả bằng đoạn mã bên d ưới. Ph ần ch ủ độ ng g ồm có vài ti ến trình và m ột giao di ện yêu c ầu, mà có th ể được gắn và ph ần b ị độ ng. M ột ti ến trình được mô t ả b ởi m ột ch ươ ng trình s ử d ụng các d ịch vụ t ừ ph ần b ị độ ng để ph ản ứng l ại các s ự ki ện t ừ môi tr ường c ủa h ệ th ống. Các s ự ki ện không được điều khi ển b ởi h ệ th ống. V ậy các s ự ki ện thú v ị t ừ môi tr ường và d ịch vụ h ệ th ống đi cùng nhau v ới các đặ c t ả c ủa nó và giao th ức t ươ ng tác hình thành h ợp đồng gi ữa h ệ th ống và môi tr ường c ủa nó. Th ực t ế, đây là m ột mô hình thành ph ần dùng để gi ải bài toán ph ươ ng trình b ậc 4 dạng đặ c bi ệt. N ếu ta đặ t X = x2 thì ph ươ ng trình s ẽ tr ở thành d ạng b ậc 2. component double_quadr { provide method { name { dquadr(in : real a, b, c; out : real x1) }, specification { ac ≤ 0 • ax1 4 + bx1 2 + c = 0 } } required method { name { quadr(in : real a, b, c; out : real x1) }, specification { ac ≤ 0 • ax1 2+bx1+c = 0 ∧x1 ≥ 0 } } protocol { (?dquadr!dquadr) ∗ ⊕ (?quadr!quadr) ∗} 15
23. implementation { name { dquadr(real in : a, b, c, real out : x1) }, code {quadr(in : a, b, c; out : x1); x1 := sqrt(x1) } } } Định ngh ĩa 7 = Một giao di ện h ệ th ống là m ột c ặp SI(, E Fd , SMd p ) v ới SMd p là m ột t ập hợp hữu h ạn các ph ươ ng th ức, Fd là m ột t ập h ợp hữu h ạn các đặ c tính, và E là t ập hợp hữu h ạn các s ự ki ện. Định ngh ĩa 8 Một hợp đồ ng hệ th ống là m ột t ập h ợp h ữu h ạn Sys Ctr= SI , SMSpec , Inv , Behav với • = SI(, E Fd , SMd p ) là m ột giao di ện h ệ th ống được đị nh ngh ĩa ở trên. • MSpec là m ột đặ c t ả ph ươ ng th ức k ết h ợp v ới m ỗi ph ươ ng th ức α op( in , out ) trong SMd p v ới m ột thi ết k ế ,FP v ới α ∪ ⊆ ( \ (in out )) F d . • Behav là m ột mô t ả hành bi bên ngoài. Nó là m ột t ập con hữu h ạn c ủa ∈ ∈ {e , m | e E và m SMd p }* . M ỗi y ếu t ố c ủa Behav được g ọi là m ột đặ c tả ti ến trình. M ột ngh ĩa không chính th ức c ủa dãy α trong Behav là n ếu môi tr ường h ệ th ống cung c ấp dãy các s ự ki ện nh ư là bi ến c ố trong α do v ậy h ệ th ống cung c ấp dãy các d ịch v ụ (ph ươ ng th ức) ch ỉ rõ b ởi α theo th ức t ự. Các ph ần t ử c ủa Behav được mô tả b ởi các lu ồng ch ươ ng trình đang ch ạy song song. M ột i ểu hi ện ng ữ ngh ĩa c ủa Behav có th ể được đị nh ngh ĩa trong logic th ời gian phù h ợp cho mi ền ứng d ụng đang nghiên c ứu. Định ngh ĩa 9 Một thành ph ần ch ủ độ ng ActComp= Ctr, SysCtr , Mcode bao g ồm 16
24. • = Một h ợp đồ ng Ctr(,), Ipr I MSpec , Init , Inv pr , Inv , Pro v ới giao di ện = ∅ ∅ cung c ấp r ỗng, I p ( , ) . • Một h ợp đồ ng h ệ th ống Sys Ctr= SI , SMSpec , Inv , Behav . • Một cài đặt ti ến trình Mcode gán m ỗi m ột ph ươ ng th ức op trong SMd p một thi ết k ế xây d ựng t ừ các toán t ử c ơ b ản và ph ươ ng th ức trong Ir nh ư ∈ là phép chi ếu v ết c ủa thi ết k ế này trong b ất kì phươ ng th ức op Md r được thay th ế b ởi ?op ! op (t ự b ắt đầ u và k ết thúc hành động), trên ∈ {?,!|m m m Md r } được bao g ồm trong Pro . Điều ki ện sau đây ph ải được th ỏa mãn b ởi Mcode:( SMspec () op⊑ Mcode ()) op cho t ất c ả ∈ op SMd p Một h ệ th ống trong mô hình thành ph ần này là m ột thành ph ần ch ủ độ ng được gắn vào m ột thành ph ần b ị động đóng. Định ngh ĩa 10 Một h ệ th ống là m ột c ặp c ủa m ột thành ph ần ch ủ độ ng ActComp= Ctr, SysCtr , Mcode và m ột thành ph ần b ị độ ng đóng Comp= Ctr′, Mcode ′ với Ctr>> Ctr ′ đã được đị nh ngh ĩa. Vậy m ột h ệ th ống thành ph ần là m ột h ệ th ống đóng không yêu c ầu b ất kì d ịch v ụ nào t ừ môi tr ường và cung c ấp d ịch v ụ c ủa nó cho môi tr ường nh ư là ph ản ứng c ủa nó đáp s ự ki ện kích thích từ môi tr ường. Đặ c t ả c ủa m ột h ệ th ống là h ợp đồ ng h ệ th ống Sys Ctr . Hai h ệ th ống là t ươ ng đươ ng nhau n ếu và ch ỉ n ếu chúng có cùng đặc t ả, ngh ĩa là chúng có giao di ện h ệ th ống t ươ ng đươ ng. Định lí sau đây cho th ấy đặ c tr ưng quan tr ọng nh ất c ủa l ập trình d ựa trên thành ph ần. Định lí 3 Lấy S= ( ActComp , Comp ′ ) là m ột h ệ th ống làm thành t ừ thành ph ần ch ủ độ ng ActComp= Ctr, SysCtr , Mcode và thành ph ần b ị độ ng Comp′= Ctr ′, Mcode ′ . 17
25. Lấy Comp′′= Ctr ′′, Mcode ′′ là m ột thành ph ần b ị động, Ctr′⊑ Ctr ′′ . Nên (ActComp , Comp ′′ ) c ũng là m ột h ệ th ống t ươ ng đươ ng v ới S. 4. MÔ HÌNH THÀNH PH ẦN TH ỜI GIAN TH ỰC Các mô hình được trình bày trong ph ần tr ước có th ể được m ở r ộng với m ột s ố đặc tính v ề th ời gian để tr ở thành mô hình thành ph ần cho h ệ th ống th ời gian th ực. Trong ph ần này, ta th ảo lu ận v ề cách th ức th ực hi ện. Ph ần quan tr ọng c ủa vi ệc m ở rộng nằm ở các d ịch v ụ th ời gian th ực, các giao th ức t ươ ng tác th ời gian th ực và các hợp đồ ng th ời gian th ực. Các đặc t ả c ủa ph ươ ng th ức ph ải có thêm ràng bu ộc v ề th ời gian. 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 ụ. Các h ệ th ống th ời gian th ực có m ột s ố ràng bu ộc v ề m ặt th ời gian trên các d ịch vụ nh ư là th ời gian đáp ứng và ràng bu ộc v ề tài nguyên nh ư là yêu c ầu b ộ nh ớ, b ăng thông và tiêu th ụ điện n ăng. S ử d ụng lí thuy ết lập trình th ống nh ất để xác đị nh các d ịch vụ nh ư thi ết k ế giúp ta d ễ dàng m ở r ộng nên g ọi là “thi ết k ế có nhãn ràng bu ộc v ề th ời gian” mà c ũng có th ể xác đị nh các yêu c ầu tài nguyên và các tr ường h ợp th ời gian th ực hi ện x ấu nh ất cho m ột d ịch v ụ nh ư là m ột m ối quan h ệ gi ữa ti ền và h ậu điều ki ện cho các thành ph ần ch ức n ăng của d ịch v ụ. Ti ền điều ki ện cho m ột ph ươ ng th ức là m ột vị từ trên các bi ến ch ươ ng trình c ũng nh ư các bi ến tài nguyên, và hậu điều ki ện cho m ột ph ươ ng th ức là m ột m ối quan h ệ trên các bi ến ch ươ ng trình và các tr ường h ợp th ời gian th ực hi ện dur x ấu nh ất và các bi ến tài nguyên. So v ới cách ti ếp c ận otomat thì thi ết k ế có nhãn ràng bu ộc v ề th ời gian th ể hi ện t ốt h ơn. Ta có thi ết k ế có nhãn ràng bu ộc v ề th ời gian D= α, FP , FR v ới α là t ập các bi ến ch ươ ng trình được s ử d ụng b ởi ph ươ ng th ức, FP bi ểu di ễn đặ c t ả ch ức n ăng và FR bi ểu di ễn đặ c t ả phi ch ức n ăng. Trong thi ết k ế trên, FP đã được ch ỉ ra ở ph ần tr ước. FR là m ột v ị t ừ c ủa d ạng th ức q•n S≙ q⇒ S v ới q là tài nguyên ti ền điều ki ện cho ph ươ ng th ức trong giao di ện được đề c ập là gi ả đị nh trên các tài nguyên được s ử dụng b ởi ph ươ ng th ức và được đạ i di ện nh ư là v ị t ừ trên các bi ến trong RES ( RES = {res1 , ,res n } là t ập c ố đị nh các bi ến s ố nguyên). S là h ậu điều ki ện có ràng bu ộc v ề th ời gian cho ph ươ ng th ức mà quan h ệ v ới m ỗi l ượng th ời gian l tiêu t ốn cho vi ệc th ực thi ph ươ ng th ức và tài nguyên được s ử d ụng cho ph ươ ng th ức. S được đạ i di ện cho m ột v ị t ừ trên các bi ến trong RES , α và l. Ta l ấy m ột ví d ụ mô t ả cho ý ngh ĩa 2 của FR . L ấy α ≙{x,y}, FP ≙ x ≥ 0 • f y= x và FR≙ P133+ P 266 = 1 • r 18
26. ((P 133= 1⇒ l≤ 0.001) ∧ ( P 133 = 0⇒ l ≤ 0.0005)) . Khi ấy α,FP , FR đại di ện cho thi ết k ế có nhãn ràng bu ộc v ề th ời gian để tính toán y= x cho m ột s ố x không âm v ới th ời gian không quá 0.001 đơn v ị th ời gian khi th ực hi ện b ằng b ộ x ử lí 133 MHz và không quá 0.0005 đơ n v ị th ời gian khi th ực hi ện v ới b ộ x ử lí 266MHz. Làm m ịn thi ết k ế có nhãn ràng bu ộc v ề th ời gian Cũng gi ống v ới thi ết k ế trong mô hình thành ph ần, thi ết k ế có nhãn ràng bu ộc v ề th ời gian c ũng có khái ni ệm làm m ịn. Nó ch ỉ m ở r ộng thêm m ột ph ần nh ỏ so v ới khái ni ệm làm m ịn thi ết k ế được nêu ra ở ph ần tr ước. = α = α M ột thi ết k ế D2, FP 2 , FR 2 được g ọi là làm m ịn t ừ D1, FP 1 , FR 1 (bi ểu di ễn là D1⊑ D 2 ) n ếu và ch ỉ n ếu ∀′ ′ • ⇒ ∧ ∀ • ⇒ (,,,okokvv FP21 FP )(, rl FR 21 FR ) Với v, v ’ là các véc t ơ c ủa bi ến ch ươ ng trình, r bi ểu th ị m ột véc t ơ c ủa bi ến tài ∧ nguyên, r = (res1 , ,res n ) . Ph ần đầ u c ủa phép toán VÀ ( ) là mu ốn nói lên thành ph ần ch ức n ăng D2 là b ản làm m ịn c ủa ph ần ch ức n ăng D1. Ph ần ti ếp theo c ủa phép toán VÀ nói r ằng n ếu yêu c ầu phi ch ức n ăng c ủa D2 được th ỏa mãn thì yêu c ầu phi ch ức n ăng c ủa D1 c ũng được th ỏa mãn. V ậy D2 có th ể cài đặt D1. Thành ph ần tu ần t ự. = α = α Lấy D1 1, FP 1 , FR 1 và D2 2, FP 2 , FR 2 là hai thi ết k ế có nhãn ph ụ α thu ộc th ời gian. V ậy, D1; D 2 ≙ , Fp , FR v ới • = ′ = FP1 FP 1 ( v ) và FP2 FP 2 ( v ) • ∃• ∧ ∧=+ FR≙ ll12,([] FRl/l 11 FRl/l 22 [] l l 12 l ) Từ đây v ề sau, ta s ẽ s ử d ụng F[ x1 /x ] để bi ểu di ễn bi ểu th ức k ết qu ả c ủa vi ệc thay th ế x b ằng x1 trong bi ểu th ức F. T ừ đó tài nguyên được s ử d ụng cho D1 có th ể được s ử d ụng l ại cho D2 khi mà D1 k ết thúc. Phân tách thành ph ần song song. = α = α Lấy D1 1, FP 1 , FR 1 và D2 2, FP 2 , FR 2 là các thi ết k ế có nhãn ph ụ α∩ α = ∅ α thu ộc th ời gian. Gi ả thi ết r ằng 1 2 . V ậy D1|| D 2 ≙ ,, FP FR khi 19
27. • α α∪ α ∧ ≙ 1 2 và FP≙ FP1 FP 2 FR≙ ∃ ll,,, rr • ( FR[l/lr ,/ r] ∧ • 1212 11 1 v ới r và r là các véc t ơ ∧= ∧=+ 1 2 FRllrr222[ /, .] l max{,} ll 12 rrr) 12 của bi ến tài nguyên và r1+r 2 đã được đị nh nghĩa. = + Điều ki ện r r1 r 2 bi ểu th ị s ố l ượng các bi ến tài nguyên đủ để th ực thi D1 và D2 song song m ột cách độ c l ập. L ệnh composed được hoàn thành khi c ả hai l ệnh thành ph ần được hoành thành. Để lí gi ải hai định ngh ĩa này, ta có th ể s ử d ụng ng ữ ngh ĩa mang tính ho ạt độ ng cho ch ươ ng trình được đị nh ngh ĩa nh ư là m ột h ệ th ống chuy ển ti ếp có nhãn (,S→ ,) C v ới m ỗi tr ạng thái s∈ S là m ột t ập h ợp h ữu h ạn. (v , r ,) t . Trong đó v là m ột véc t ơ các giá tr ị c ủa bi ến ch ươ ng trình, r là m ột véc t ơ các giá tr ị c ủa bi ến tài nguyên và t là m ột s ố th ực để ch ỉ th ời gian th ực. C là m ột t ập l ệnh. Lấy ng ữ ngh ĩa c ủa c∈ C là thi ết k ế α,FP , FR v ới FP= p R và FR= p S . ⊢f r⊢ n Vậy có m ột phép chuy ển (,,)vrt→c (,,) vrt′ ′ ′ n ếu và ch ỉ n ếu ∧′′ ∧=∧ ∧=−∧ ′ ′ pv()(,) Rvv r r prr () l t t Slrvv (,,,) thông qua s ự thông d ịch c ủa các thi ết k ế. Vi ệc đị nh ngh ĩa phân tách thành ph ần song song và thành ph ần tu ần t ự hi ển nhiên trong h ệ th ống chuy ển ti ếp nhãn trùng v ới đị nh ngh ĩa đã cho ở trên. Đối v ới h ợp đồ ng trong h ệ th ống d ựa trên thành ph ần th ời gian th ực có s ự khác bi ệt so v ới h ệ th ống d ựa trên thành ph ần đơn thu ần. Ta có đị nh ngh ĩa v ề h ợp đồ ng có nhãn ràng bu ộc v ề th ời gian. Định ngh ĩa Một h ợp đồ ng có nhãn ràng bu ộc v ề th ời gian là m ột t ập h ợp h ữu h ạn I,, Rd MSpec ,, Init Inv v ới • I= Fd, Md là m ột giao di ện. • Rd là m ột khai báo tài nguyên, nó là m ột t ập con c ủa RES . • Init là m ột kh ởi t ạo, k ết h ợp v ới m ỗi bi ến trong Fd và m ỗi bi ến c ục b ộ v ới cùng m ột ki ểu giá tr ị. Bi ến trong Rd v ới ki ểu s ố nguyên. 20
28. • MSpec là đặc t ả ph ươ ng th ức k ết h ợp v ới m ỗi ph ươ ng th ức op( in , out ) trong Md v ới m ột thi ết k ế có nhãn ràng bu ộc v ề th ời gian α,FP , FR , trong đó (α \ (in∪ out )) ⊆ Fd . • Inv là m ột v ị t ừ trên các đặc tính trong h ợp đồ ng ( được g ọi là b ất bi ến h ợp đồng). Inv đại di ện cho m ột thu ộc tính b ất bi ến c ủa giá tr ị bi ến trong khai báo đặc tính Fd mà có th ể tin c ậy t ại b ất kì th ời điểm nào mà mó có th ể truy c ập t ừ bên ngoài. T ừ đây, Inv được th ỏa mãn m ột cách đặ c bi ệt b ởi Init . Ta nh ấn m ạnh ở đây là các bi ến tài nguyên được khai báo trong Rd là bi ến n ội trong m ột h ợp đồ ng (bi ến c ục b ộ). Inv 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. Trong tr ường h ợp h ợp đồng không đả m b ảo b ất kì m ột thu ộc tính b ất bi ến nào c ủa các giá tr ị c ủa nó thì Inv là đúng. Các hợp đồ ng này c ũng c ần được làm m ịn. T ừ th ực ti ễn nghiên c ứu vấn đề , ta có định ngh ĩa v ề làm m ịn h ợp đồ ng nh ư sau: Hợp đồ ng có ràng bu ộc v ề th ời gian = Ctr2 Fd 222, Md ,, Rd MSpec 222 ,, Init Inv là được làm m ịn b ằng h ợp đồ ng = Ctr1 Fd 111, Md ,, Rd MSpec 111 ,, Init Inv , (được bi ểu di ễn là Ctr1⊑ Ctr 2 ) n ếu và ch ỉ n ếu: • ⊆ ⊆ = ≤ Fd1 Fd 2 , Rd1 Rd 2 và Init21| Fd Init 1121 |,| Fd Init Rd Init 11 | Rd đối v ới các hàm f, f1 , f 2 và t ập A. f| A bi ểu th ị h ạn ch ế c ủa f trên A và ≤ ≤ f1 f 2 bi ểu th ị r ằng f1 và f2 có cùng mi ền và fx1() fx 2 () v ới m ọi x trong mi ền c ủa chúng. • ⊆ Md1 Md 2 . • Với m ọi ph ươ ng th ức op được khai báo trong Md 1 thì ⇒ Mspec1() op⊑ Mspec 2 () op và Inv2 Inv 1 . 21
29. Ta lý gi ải định ngh ĩa này nh ư sau. Ctr 2 cung c ấp t ất c ả các d ịch v ụ mà Ctr 1 cung cấp và có th ể cung c ấp nhi ều h ơn n ữa. Ctr 2 ph ải có ít nh ất cùng tài nguyên nh ư là Ctr 1 ⇒ có. Điều ki ện Inv2 Inv 1 nói lên r ằng thu ộc tính c ủa các bi ến được đả m b ảo b ởi Ctr 1 thì c ũng ch ắc ch ắn được đả m b ảo b ởi Ctr 2 . V ật có th ể thay th ế Ctr 1 b ằng Ctr 2 mà không b ị m ất b ất kì m ột d ịch v ụ nào. = = Đặt Ctri Fd iii, Md , Rd , Mspec ii , Init ,1,2 i là các h ợp đồ ng có ràng bu ộc về th ời gian t ươ ng thích v ới t ập h ợp các đặ c tính và ph ươ ng th ức. Có ngh ĩa là ∈ ∩ = ∈ ∩ f Fd1 Fd 2 bao hàm c ả Init1() f Init 2 () f và op Md1 Md 2 bao hàm c ả ⇔ ∪ MSpec1() op MSpec 2 () op . Kết h ợp h ợp đồ ng Ctr1 Ctr 2 được đị nh ngh ĩa nh ư (Fd∩ Fd , Md ∩ Md ), Rd ∪ Rd , sau: Ctr∪ Ctr = 1 21 21 2 1 2 ∪ ∧ MSpec1 MSpec 21, Init⊎ Init 212 , Inv Inv với (Init1⊎ Init 2 )( x ) được đị nh ngh ĩa là ∈ ∩ max{ Init1 ( x ), Init 2 ( x )} nê'u x dom(Init1 ) dom(Init 2 )  ∈ Init1( x ) nê'u x dom(Init1 )\ dom(Init 2 )  ∈ Init2 ( x ) nê'u x dom(Init2 )\ dom(Init 1 ) ∪ Khi Ctr1 Ctr 2 được đị nh ngh ĩa thì ta có th ể nói Ctr 1 và Ctr 2 có th ể rút g ọn. Chú ý r ằng khi kết h ợp 2 hợp đồ ng, lượng tài nguyên có s ẵn để kết h ợp được đị nh ngh ĩa nh ư là v ới thành ph ần h ợp đồ ng l ớn nh ất. Định ngh ĩa này ph ản ánh cái nhìn m ột ph ươ ng th ức trong kết h ợp h ợp đồ ng ph ải có ít nh ất cùng th ời gian th ực hi ện nh ư là nó có trong các h ợp đồ ng thành ph ần, được cung c ấp đúng m ẫu. Đúng m ẫu có ngh ĩa là th ực thi ph ụ thu ộc th ời gian t ốt h ơn n ếu có nhi ều tài nguyên được cung c ấp và được hình th ức hóa. Một thi ết k ế có ràng bu ộc v ề th ời gian α,FP , FR được g ọi là đúng ∀ • ≥ ⇒ ⇒ mẫu n ếu và ch ỉ n ếu FR th ỏa mãn r,( r1 r r 1 ([/ FR r RES ] FR [/ r1 RES ])) . Với r và r1 là các véc t ơ giá tr ị c ủa các bi ến tài nguyên. 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. Giao th ức t ươ ng tác cho các thành ph ần th ời gian th ực ph ải mang theo không ch ỉ các thông tin theo th ứ t ự th ời gian c ủa hành động giao ti ếp mà còn c ả ràng bu ộc th ời gian c ủa chúng. Nh ư trong lí thuy ết otomat có nhãn ràng bu ộc v ề th ời gian, ta có th ể gán nhãn cho m ột bi ến c ố c ủa m ột hành động giao ti ếp v ới th ời gian x ảy ra. M ột chu ỗi 22
30. các ho ạt độ ng truy ền thông được gán nhãn theo các này được g ọi là “từ th ời gian” (t ừ có nhãn ràng bu ộc v ề th ời gian). Nó bi ểu di ễn hành vi c ủa h ệ th ời gian th ực là m ột dãy ti ến hành trong đó m ỗi bi ến c ố đề u có nhãn th ời gian ch ỉ bi ểu di ễn kho ảng th ời gian trôi qua k ể t ừ bi ến c ố li ền tr ước. M ột t ập h ợp c ủa chu ỗi có nhãn th ời gian của các hành động có th ể giao ti ếp có th ể bi ểu th ị m ột gi ả thi ết b ằng m ột thành ph ần v ề hành vi th ời gian th ực trong môi tr ường c ủa nó. Ngôn ng ữ có nhãn ràng bu ộc v ề thời gian được nghiên c ứu k ĩ và hi ểu rõ, từ đây có th ể s ử d ụng chúng cho các đặc t ả c ủa các giao th ức tươ ng tác, các ti ến trình có nhãn ràng bu ộc th ời gian th ực thu ận l ợi h ơn. Đối v ới hi ệu qu ả trong vi ệc ki ểm ch ứng m ột ph ươ ng th ức th ời gian th ực trong các thành ph ần, các giao th ức trong ràng bu ộc ph ải không có b ất k ỳ thông tin v ề th ời gian, và thông tin th ời gian cho m ột giao th ức được b ắt ngu ồn t ừ nh ững đặ c t ả c ủa ph ươ ng th ức th ời gian th ực t ừ các giao th ức. 4.3. Các h ợp đồ ng th ời gian th ực. Các hợp đồ ng th ời gian th ực được đị nh ngh ĩa theo cùng m ột cách nh ư đối v ới các h ợp đồ ng trong ph ần tr ước. Các đị nh ngh ĩa c ủa giao di ện được m ở r ộng b ằng cách cho phép c ủa các khai báo c ủa tài nguyên được nhóm l ại vào trong tài nguyên có th ể tiêu th ụ được và tài nguyên không th ể tiêu th ụ được. Nh ững b ất bi ến h ợp đồ ng giao di ện ph ải m ở r ộng để mô t ả nh ững nh ững s ự ràng bu ộc trên tài nguyên. Trong các thi ết kế có nhãn ràng bu ộc v ề th ời gian c ủa h ợp đồ ng th ời gian th ực được s ử d ụng thay vì các thi ết k ế. M ột thành ph ần th ời gian th ực là m ột cài đặt c ủa m ột h ợp đồ ng th ời gian th ực. Ta đư a ra đây m ột ví d ụ v ề h ệ th ống thành ph ần th ời gian th ực d ựa trên mô hình đã được nghiên c ứu ở trên. Ta có ví d ụ minh h ọa sau đây. Ở đây, ng ưỡng tài nguyên đặc tính ch ỉ rõ b ộ nh ớ thi ết l ập cho thành ph ần, và s.event ch ỉ rõ tín hi ệu t ừ l ập l ịch đị nh kì g ửi đến ti ến trình. Ta s ử d ụng bi ểu th ức chính quy có nhãn rang bu ộc v ề th ời gian để bi ểu di ễn hành vi có ràng bu ộc v ề th ời gian c ủa ti ến trình. Mô hình h ệ th ống thành ph ần này là m ột b ộ điều khi ển đị nh kì thu th ập tín hi ệu điều khi ển thông qua tác t ử d ựa trên d ữ li ệu chúng c ảm nh ận được. Th ời gian định kì c ủa vòng điều khi ển là 100ms . component Actuator1 { provided feature int p1; inv p1 > 0 ; 23
31. resource int threshold = 20; provided method { name getdata() , specification true • p10 = portvalue ∧ p10 > 0 ∧ dur = 0 }; provided method { name execute() , specification p1 = valid ˫ ( actionresult ∧ dur = 30) }; }; component Actuator2 { provided feature int p1; inv p1 > 0; resource int threshold = 30; provided method { name getdata(), specification true ˫ p10 = portvalue ∧ p10 > 0 ∧ dur = 0 }; provided method { name execute() , specification p1 = valid ˫ ( actionresult ∧ dur = 30) }; }; active component Composition { process { 24
32. name main , specification ((s.event; actuator1.execute()||actuator2.execute(); actuator1.getdata; actuator2.getdata; ), dur ≤ 100 )∗ } 4.4. Thành ph ần b ị độ ng Định ngh ĩa Một thành ph ần b ị độ ng th ời gian th ực là m ột t ập h ợp h ữu h ạn Comp= Ctr,, Dep SDep , Mcode , SInv v ới Comp được xác đị nh v ới tên c ủa thành ph ần, nó bao g ồm: • Một h ợp đồ ng Ctr= Fd, Md ,, Rd MSpec ,, Init Inv . • Tập h ợp Dep c ủa tên các thành ph ần, m ỗi ph ần t ử c ủa Dep là m ột tên c ủa thành ph ần mà Comp ph ụ thu ộc vào. • SDep là t ập h ợp các bi ến trong ∏ ( đại di ện cho s ự t ươ ng tác v ới b ộ l ập lịch). • SInv là m ột v ị t ừ trên các bi ến v∈ SDep ( để bi ểu di ễn gi ả thi ết thông tin mà bộ l ập l ịch có th ể tin c ậy khi m ột ph ươ ng th ức trong Comp được g ọi). • Mcode gán m ỗi ph ươ ng th ức op trong Md m ột thi ết k ế được xây d ựng t ừ các toán t ử c ơ b ản và các l ời g ọi ph ươ ng th ức t ừ d ạng th ức call( Comp ,, C op 1 ) , v ới op 1 là m ột ph ươ ng th ức trong thành ph ần C trong Dep . Chú ý r ằng các tên ph ươ ng th ức, bi ến tài nguyên và bi ến c ục b ộ được sử d ụng trong đặ c t ả và cài đặt c ủa ph ươ ng th ức op1( in , out ) trong thành ph ần b ị độ ng C là c ục b ộ trong C và có ti ền t ố là “ Ci ” để ch ống l ại s ự l ẫn l ộn với các bi ến được s ử d ụng trong các thành ph ần b ị độ ng khác. L ấy Env bi ểu ị ị ừ ∧ ừ đ ở đ ử ụ th v t ∧U∈ Dep (Inv ( Ctr ( U )) SInv ( U )) (t ây tr i, ta s d ng Ctr( U ) để bi ểu th ị h ợp đồ ng c ủa thành ph ần U, Inv( Ctr ( U )) để bi ểu th ị b ất bi ến c ủa hợp đồ ng thành ph ần U, Dep( U ) bi ểu th ị t ập h ợp tên thành ph ần mà U ph ụ 25
33. thu ộc và SInv( U ) bi ểu th ị b ất bi ến l ập l ịch h ệ th ống c ủa thành ph ần U). Điều ki ện sau đây ph ải được th ỏa mãn b ởi Mcode : Env
    (MSpec ( op )⊑ Mcode ( op )) và Inv được chi ếm gi ữ b ởi b ất kì phép toán nào được s ử d ụng trong Mcode . L ấy C∈ Dep và op∈ C . Do v ậy call( Comp ,,) C op được đị nh ngh ĩa nh ư Schedule( Comp ,)|| C Ci op , v ới Schedule( Comp , C ) là m ột thi ết k ế s ử d ụng các bi ến trong SDep( C ) (giá tr ị các bi ến này đạt di ện cho nh ững l ời g ọi hi ện t ại đế n m ột ph ươ ng th ức trong C. Ta mong đợi ti ền điều ki ện c ủa Schedule( Comp , C ) được bao hàm b ởi SInv( C ) ). T ừ lu ật phân tách song song, Schedule( Comp ,)|| C Ci op bao hàm đặc t ả ch ức n ăng c ủa Ci op nh ưng không c ần thêm th ời gian để th ực hi ện. Thành ph ần Comp nói lên r ằng nó được cài đặt b ởi h ợp đồ ng Ctr . Trong định ngh ĩa c ủa thành ph ần Comp , nó yêu c ầu MSpec() op⊑ Mcode () op cho t ất c ả các ph ươ ng th ức op trong h ợp đồ ng c ủa Comp theo gi ả đị nh ∧ Đ ề ĩ đượ ấ ấ ả ∧U∈ Dep (Inv ( Ctr ( U )) SInv ( U )) . i u này có ngh a là c cung c p t t c các thành ph ần mà Comp ph ụ thu ộc vào ph ải đả m nh ững b ất bi ến c ủa chúng, b ất kì ph ươ ng th ức nào c ủa thành ph ần Comp được cài đặt đúng đắn. C ũng nh ư v ậy, ta yêu cầu b ất kì phép toán nào trong Comp ph ải đả m b ảo b ất bi ến c ủa Comp . B ởi v ậy op có th ể được s ử d ụng nh ư là m ột dịch v ụ thích hợp v ới đặ c t ả MSpec( op ) . Có m ột câu hỏi được đặ t ra là làm th ế nào để ch ắc ch ấn r ằng ∧ ∧U∈ Dep (Inv ( Ctr ( U )) SInv ( U )) được đả m b ảo? Cài đặt c ủa op tin c ậy vào các ph ươ ng th ức trong thành ph ần v ới tên trong Dep . Nh ưng cài đặt c ủa các ph ươ ng th ức cu ối cùng l ại tin c ậy vào op . Tình hu ống này đã đư a đến lí lu ận vòng quanh và nó có th ể là nguyên nhân làm cho op được cài đặt không chính xác. Tình hu ống này s ẽ không x ảy ra n ếu cài đặt t ốt cho ph ươ ng th ức được đị nh ngh ĩa. Định ngh ĩa v ề cài đặt t ốt. Các ph ươ ng th ức được cài đạt t ốt được đị nh ngh ĩa đệ quy nh ư sau: • Nếu op là m ột ph ươ ng th ức trong m ột thành ph ần v ới mã l ệnh Mcode( op ) được biên so ạn t ừ các l ệnh c ơ b ản thì op là được cài đặt t ốt. 26
34. • Nếu op là m ột ph ươ ng th ức trong m ột thành ph ần v ới mã l ệnh Mcode( op ) được biên so ạn t ừ các l ệnh c ơ b ản và các lời g ọi ph ươ ng th ức cho m ột ph ươ ng th ức được cài đặt t ốt thì op là được cài đặt t ốt. Vậy ph ươ ng th ức được cài đặt t ốt không ch ứa các l ời g ọi ph ươ ng th ức đệ quy, mặc dù các ph ươ ng th ức ch ứa các l ời g ọi ph ươ ng th ức đệ quy có th ể k ết thúc và có ng ữ ngh ĩa được đị nh ngh ĩa t ốt. Từ các k ết qu ả trên, ta đư a ra gi ải quy ết v ấn để kết h ợp thành ph ần. L ấy = = Ci Ctr ii, Dep , SDep i , Mcode ii , Inv ,1,2 i là các thành ph ận b ị độ ng có các h ợp ≡ đồng có th ể t ổ h ợp và th ỏa mãn Mcode1() op Mcode 2 () op đối v ới t ất c ả ∈ ∩ ∪ op Md1 Md 2 . T ổ h ợp C1 C 2 được đị nh ngh ĩa là: ∪∪ ∪ ∪ ∪ Ctr12121 Ctr,, Dep Dep SDep SDep 2 , Mcode 1 Mcode 21 , SInv SInv 2 Cần l ưu ý m ột vài điểm sau: • Các ph ươ ng th ức trong các thành ph ần được đị nh ngh ĩa nh ư các thi ết k ế v ới ti ền điều ki ện, h ậu điều ki ện và các quan h ệ trên l ượng th ời gian để th ực thi các ph ươ ng th ức, tài nguyên s ẵn có. Điều này phù h ợp cho vi ệc ch ỉ rõ các h ệ th ống ng ừng ho ạt độ ng. nh ưng nó không đủ m ạnh để bi ểu di ễn ho ạt độ ng c ủa các ch ươ ng trình không d ừng ho ặc h ệ th ống t ươ ng tác. • Định ngh ĩa c ủa m ột thành ph ần Comp yêu c ầu Mspec() op⊑ Mcode () op với gi ả đị nh ∧ (Inv ( Ctr ( U ))∧ SInv ( U )) . Điều ki ện Inv( Ctr ( U )) trên U∈ Dep các bi ến được s ử d ụng để cài đặt đặ c t ả ch ức n ăng cho ph ươ ng th ức op, được đảm b ảo b ởi t ất c ả các thành ph ần U. Điều ki ện SInv( U ) trên các bi ến SDep( U ) ch ỉ được s ử d ụng b ởi b ộ l ập l ịch và được s ử d ụng để cài đặt đặ c t ả phi ch ức n ăng c ủa ph ươ ng th ức. B ởi v ậy, n ếu SInv( U ) được ki ểm ch ứng nh ư là m ột b ất bi ến toàn c ục cho h ệ th ống đáp ứng không ràng bu ộc v ề th ời gian thì nó c ũng phải là m ột b ất bi ến c ủa h ệ th ống có ràng bu ộc th ời gian n ữa. Ki ểm ch ứng c ủa b ất bi ến SInv( U ) cho h ệ th ống đáp ứng không ràng bu ộc v ề th ời gian được th ực hi ện v ới các k ĩ thuy ệt truy ền th ống. Ví d ụ nh ư khi không cần thi ết ph ải l ập l ịch (t ức là s ử d ụng song song c ủa các d ịch v ụ được ch ấp nh ận ho ặc các d ịch v ụ ch ỉ đự c g ọi b ởi duy nh ất m ột thành ph ần t ại m ột th ời điểm, SDep( U ) = ∅ v ới t ất c ả U) và sau đó ta có th ể có 27
35. Schedule( Comp ,) C= ∅ , skip ,0 l = (sau khi ta gi ả đị nh r ằng các tính toán luôn luôn c ần th ời gian và t ừ đây v ề sau, đặ c t ả th ời gian cho b ộ l ập l ịch trong tr ường h ợp này ph ải được thay đổ i thành l>0 ∧ l ≤ d v ới d là l ươ ng th ời gian nh ỏ nh ất c ần để th ực hi ện l ệnh v ới gi ả thi ết v ề các tài nguyên trong h ệ th ống). Ti ền điều ki ện cho Schedule( Comp , C ) là đúng và SInv( C ) có th ể đúng là b ất bi ến t ầm th ường. Thêm m ột ví d ụ khác, gi ả đị nh rằng b ộ l ập l ịch sử d ụng chính sách “ đế n tr ước ph ục v ụ tr ước” (FIFO) và l ượng th ời gian l ớn nh ất mà m ỗi l ần m ột thành ph ần s ử d ụng m ột d ịch v ụ c ủa thành ph ần Comp là a, và có kho ảng n thành ph ần khác có th ể s ử d ụng các d ịch v ụ c ủa Comp . Vậy ta có Schedule( Com )= SDep ( U ), FP , l ≤ n x a . Li ệu có ph ải có các lời g ọi đồ ng th ời t ới m ột thành ph ần ho ặc không ph ụ thu ộc vào n ếu có các ph ươ ng th ức ch ủ độ ng đồ ng th ời trong h ệu th ống. N ếu nghôn ng ữ cho phép một ph ươ ng th ức được cài đặt v ới các l ệnh song song ho ặc n ếu có nhi ều h ơn một lu ồng đang ch ạy song song trong h ệ th ống. Từ ph ần đã nói ở trên ta có lí do để đị nh ngh ĩa m ột thành ph ần Comp 2 được làm mịn b ởi Comp 1 n ếu và ch ỉ n ếu Comp 2 t ốt h ơn Comp 1 theo ngh ĩa Comp 2 cung c ấp nhi ều hơn các d ịch v ụ c ủa Comp 1 nh ưng c ần ít d ịch v ụ h ơn Comp 1 và điều ki ện l ập l ịch trong Comp 2 kém h ơn trong Comp 1 (có ngh ĩa là Comp 2 có b ất bi ến m ạnh h ơn cho b ộ l ập lịch, c ũng đồ ng ngh ĩa b ộ l ập l ịch ho ạt độ ng v ới Comp 1 thì c ũng ho ạt độ ng v ới Comp 2). Vậy ta có đị nh ngh ĩa cho làm m ịn thành ph ần nh ư sau: ( định ngh ĩa 11) = = Lấy Compi Ctr ii, Dep , SDep i , Mcode ii , SInv ,1,2 i là các thành ph ần b ị động. Comp 1 được g ọi là làm m ịn b ởi Comp 2 ( được bi ểu th ị là Comp1⊑ Comp 2 ) n ếu và ch ỉ n ếu: • Ctr1⊑ Ctr 2 (t ức là Comp 2 cung c ấp nhi ều d ịch v ụ h ơn Comp 1). • ⊆ ⊆ ⇒ Dep2 Dep 1 , SDep2 SDep 1 và SInv1 SInv 2 (t ức là Comp 2 không cần nhi ều d ịch v ụ t ừ h ệ th ống nh ư Comp 1 và c ần gi ả thi ết y ếu h ơn v ề l ập lịch h ệ th ống). 4.5. Thành ph ần ch ủ độ ng Thành ph ần ch ủ độ ng được đị nh ngh ĩa theo cách gi ống nh ư thành ph ận b ị độ ng được đị nh ngh ĩa ngo ại tr ừ r ằng thành ph ần ch ủ độ ng ph ải có khai báo lu ồng song và các khái báo bi ến c ố. Thành ph ần ch ủ độ ng được điều khi ển b ởi c ả các bi ến c ố t ừ môi 28
36. tr ường và đồng h ồ bên trong nó. M ột lu ồng T được đị nh ngh ĩa always D follows e với e là m ột bi ến c ố d ạng bi ểu th ức nh ị phân và D là m ột ph ươ ng th ức. Ý ngh ĩa c ủa bi ểu di ễn “ D follows e ” là e⇒ ok∧ D . Nói chung thì lu ồng T đang l ắng nghe các bi ến c ố c ủa c ự ki ện e. B ất kì khi nào mà bi ến c ố e x ảy ra, ph ươ ng th ức D s ẽ được g ọi. Định ngh ĩa 12 Một h ệ th ống d ựa trên thành ph ần là m ột t ập S c ủa các thành ph ần sao cho b ất kì thành ph ần ch ủ độ ng U∈ S nào, b ất kì V sao cho U Dep* V mà V∈ S chi ếm gi ữ. Trong m ột h ệ th ống d ựa trên thành ph ần, ta có th ể thay th ế m ột thành ph ần b ị động b ằng m ột thành ph ần t ốt h ơn mà không vi ph ạm các yêu c ầu. thật v ậy, ta có đị nh lí sau. Định lí 4 Lấy S là m ột h ệ th ống d ựa trên thành ph ần. Comp 1 và Comp 2 là các thành ph ần ∈ bị độ ng sao cho Comp1⊑ Comp 2 và Comp1 S . S 1 có được b ằng vi ệc thay th ế Comp 1 b ằng Comp 2 và đồng th ời thay th ế m ỗi bi ến c ố c ủa Comp 1 trong h ệ th ống S bằng m ột bi ến c ố c ủa Comp 2 . Do v ậy, S 1 c ũng là m ột h ệ th ống d ựa trên thành ph ần và cung c ấp nhi ều d ịch v ụ h ơn S. Ta s ẽ ch ứng minh đị nh lí này nh ư sau: Điều duy nh ất c ần để ch ứng minh là sau khi thay th ế các bi ến c ố c ủa Comp 1 bằng các bi ến c ố c ủa Comp 2 thì k ết qu ả v ẫn là m ột t ập h ợp các thành ph ần c ủa h ệ th ống. Có ngh ĩa là ta ph ải th ể hi ện điều đó cho b ất kì phương th ức op nào trong h ợp đồng c ủa m ột thành ph ần k ết qu ả C, Mspec() op⊑ Mcode () op theo gi ả thi ết ∧ (Inv ( Ctr ( U ))∧ SInv ( U )) . T ừ đị nh ngh ĩa 11 ở trên v ề làm m ịn thành ph ần, nó U∈ Dep( C ) kéo theo Schedule( Comp , Comp1 )|| Comp 1i op⊑ Schedule ( Comp , Comp2 )|| Co mp 2 i op cho b ất kì ph ươ ng th ức op nào trong Comp 1 . T ừ s ự đơn điệu c ủa các phép toán trong vi ệc s ử d ụng ngôn ng ữ l ập trình theo quan h ệ làm m ịn, và t ừ th ực t ế là ⇒ SInv( Comp2 ) SInv ( Comp 1 ) , ta có Mspec() op⊑ Mcode () op gi ữ v ới gi ả thi ết ∧ (Inv ( Ctr ( U ))∧ SInv ( U )) . U∈ Dep( C ) 29
37. 5. ỨNG D ỤNG MÔ HÌNH THÀNH PH ẦN TRONG H Ệ TH ỐNG NHÚNG Từ quá trình nghiên c ứu v ề mô hình h ệ th ống d ựa trên thành ph ần và mô hình th ời gian th ực ta có th ể xây d ựng m ột mô hình thành ph ần trên h ệ th ống nhúng. Hi ện nay, h ầu h ết các công vi ệc c ủa con ng ười đã được áp d ụng công ngh ệ, t ự độ ng hóa nh ằm m ục đích nâng cao hi ệu qu ả công vi ệc, đả m b ảo an toàn cho con ng ười. Cùng với m ục đích đó, h ệ th ống hướng d ẫn xe (Car Navigation System – vi ết t ắt là CNS) được xây d ựng nh ằm d ẫn đường cho các lái xe đi qua m ột khu v ực. Để t ươ ng tác v ới lái xe, h ệ th ống ph ải có m ột thi ết b ị hi ển th ị để th ể hi ện bản đồ c ủa khu v ực xung quanh xe, m ột bàn phím để th ực hi ện các l ệnh c ơ b ản nh ư hi ển th ị b ản đồ , phóng to/thu nh ỏ và tìm đường đi t ới đích. Một thành ph ần đặ t c ơ s ở thi ết k ế cho CNS mà được th ể hi ện trong hình 6, g ồm có nh ững thành ph ần chính sau đây, trong đó quan h ệ Dep gi ữa nh ững thành ph ần được đạ i di ện cho b ởi nh ững m ũi tên trong hình. Hình 6: S ơ đồ thành ph ần cho H ệ th ống h ướng d ẫn xe • Thành ph ần GPS : Thành ph ần này có m ột ph ươ ng th ức get_pos(out : src) v ới đặ c t ả {src}, true src′ = current_position,0 <l≤ 1 . M ặc dù mã ch ươ ng trình không ⊢f được trình bày ở đây nh ưng ta gi ả đị nh r ằng mã ch ươ ng trình không ch ứa b ất kì l ời g ọi nào đến m ột ph ươ ng th ức c ủa thành ph ần khác. Thành ph ần khác duy nh ất có th ể s ử dụng thành ph ần này là Controller . Ở đây không ch ỉ rõ tài nguyên c ụ th ể được s ử dụng nh ưng gi ả đị nh r ằng ti ền điều ki ện tài nguyên cho ph ươ ng th ức get_pos(out : src) là true . • Thành ph ần RouteDB : Khai báo tài nguyên c ủa thành ph ần này bao g ồm b ộ nh ớ các bi ến tài nguyên (kh ởi t ạo 4 MB) và b ộ x ử lí 75 MHz (kh ởi t ạo là 1). Thành ph ần có 2 ph ươ ng th ức: get_ map (:, in src in : dstn ,: out map ) v ới đặ c t ả là 30
38. {,,},srcdstnmap true map′ = map ___ for the area ,0 < l ≤ 1 ⊢ f và find_ route (:,: in src in dstn ,: out route ) v ới đặ c t ả là {,src dstn , route }, true route ′ = ⊢ route_ to _ the_destination , . 75MHz proc es1 or=∧ memory = 4 n,0 <≤ l 11 ⊢ Thành ph ần khác duy nh ất có th ể s ử d ụng thành ph ần này là Controller . Đoạn mã ch ươ ng trình cho find_ route (:,: in src in dstn ,: out route ) là get_map(src,dstn,map); compute(src,dstn,map,route); Gi ả đị nh r ằng compute(src,dstn,map,route) c ần 10 giây để m ột b ộ x ử lí 75MHz s ử d ụng 4MB để th ực hi ện. Do đó đoạn mã này là m ột b ản làm m ịn đặ c t ả của find_ route (:,: in src in dstn ,: out route ) . • Thành ph ần ch ủ độ ng Controller : Thành ph ần này có m ột bi ến c ố find_ route _ command _ arrival và m ột ph ươ ng th ức find_ route _ handle . Tài nguyên được khai báo c ủa thành ph ần này là bi ến 75MHz _ processor được kh ởi t ạo là 1. Đoạn mã c ủa ph ươ ng th ức này nh ư sau: dstn:= read _ dstn ; (Schedule ( Controller , GPS )|| GPS . get _os()); p src (Schedule ( Controller , RouteDB )|| RouteDB . find _ route ( src , dstn , route )); display_ route ( dstn ); Đặc t ả th ời gian c ủa ph ươ ng th ức này là 0<l ≤ 14 . Gi ả đị nh r ằng m ỗi m ột dstn:= read _ dstn và display_ route ( dstn ) có th ời gian tiêu dùng nh ỏ h ơn 1 v ới dùng m ột b ộ x ử lí 75 MHz. Ta gi ả đị nh r ằng l ệnh Schedule( Controller , RouteDB ) và Schedule( Controller , RouteDB ) không t ốn th ời gian, ngh ĩa là l= d (ta không th ể gi ả đị nh l = 0 vì gi ả đị nh tr ước đó) là h ậu điều ki ện c ủa chúng cho đặ c t ả có ràng bu ộc th ời gian (ti ền điều ki ện c ủa chúng được đưa ra sau đó nh ư là n ất bi ến cho c ả ba thành ph ần). V ới d là th ời gian nh ỏ nh ất để th ực hi ện m ột l ệnh. Nó được suy ra tr ực ti ếp t ừ lu ật thành ph ần liên ti ếp và song song mà mã l ệnh c ủa ph ươ ng th ức này là b ản 31
39. làm m ịn c ủa đặ c t ả c ủa nó. M ột lu ồng c ủa thành ph ần này là always find _ route _ handle . after find _ route _ command _ arrival Vậy trong mô hình này c ủa h ệ th ống d ựa trên thành ph ần ta có th ể s ử d ụng UTP và các lu ật b ổ sung cho đặ c t ả th ời gian th ực cho các thi ết k ế để ki ểm ch ứng n ếu m ột ph ươ ng th ức được cài đặt đúng hay không. Tuy nhiên, để mô hình này h ỗ tr ợ ch ứng th ực thu ộc tính ph ụ thu ộc th ời gian và theo th ời gian th ực. Ta ph ải đưa ra m ột ngh ĩa hình th ức cho các lu ồng và m ột đặ c t ả hình th ức cho các thu ộc tính th ời gian th ực. 32
40. KẾT LU ẬN Sau khi nghiên c ứu các khái ni ệm v ề h ệ th ống d ựa trên thành ph ần, mô hình thành ph ần, các khái ni ệm v ề h ệ th ống d ựa trên thành ph ần th ời gian th ực, tôi đã n ắm rõ được các khái ni ệm. Tôi đã trình bày v ề mô hình thành ph ần, ki ến trúc c ủa mô hình thành ph ần. V ới mô hình được trình bày ở trên thì nó có th ể được m ở r ộng m ột cách d ễ dàng điều khi ển các thu ộc tính phi ch ức n ăng c ủa thành ph ần nh ư ch ất l ượng d ịch v ụ. Đặc tính chính c ủa mô hình thành ph ần được trình bày ở trên n ằm ở ng ữ ngh ĩa hình th ức c ủa nó trong UTP. Nó đóng vai rò nh ư là m ột n ền t ẳng xho vi ệc phát tri ển m ẫu ngôn nh ữ cho l ập trình d ựa trên thành ph ần. M ẫu ngôn ng ữ này được áp cho các ngôn ng ữ l ập trình khác để thi ết k ế, l ập trình d ựa trên thành ph ẫn d ễ dàng h ơn. C ũng trong mô hình đó, các thành ph ần được xác đị nh tính đúng đắ n b ằng thi ết k ế. điều đó c ũng có ngh ĩa là cài đặt d ịch v ụ th ỏa mãn các yêu c ầu c ủa nó. Điều đó được đẳ m b ảo ch ắc ch ắn b ằng c ả ki ểm ch ứng mô hình ho ặc ch ứng minh đị nh lý. Ngoài ra, tôi c ũng trình bày v ề mô hình thành ph ần th ời gian th ực. Mô hình này h ỗ tr ợ đặ t ả, làm m ịn thành ph ần và ki ểm ch ứng m ột vài thu ộc tính th ời gian th ực, điều mà mô hình tr ước không có. Mô hình c ũng h ỗ tr ợ s ự tách biệt gi ữa đặ c t ả ch ức n ăng t ừ đặ c t ả phi ch ức n ăng c ủa các thành ph ần, mà có th ể đơn gi ản hóa ki ểm ch ứng yêu c ầu ch ức n ăng, và trong nhi ều rường h ợp có th ể đơn gi ản hóa c ả các ki ểm ch ứng yêu c ầu phi ch ức n ăng n ữa. Dựa trên các ki ến th ức thu được tôi đã phân tích và trình bày m ột ví d ụ v ề áp d ụng mô hình dựa trên thành ph ần. Vi ệc nghiên c ứu cá khái ni ệm, đị nh ngh ĩa trong mô hình thành ph ần và h ệ th ống d ựa trên thành ph ần giúp cho thi ết k ế, phân tích và b ảo trì các hệ th ống l ớn m ột cách d ễ dàng h ơn. 33
41. TÀI LI ỆU THAM KH ẢO [1] R. Alur and D.L. Dill. A Theory of Timed Automata. Theoretical Computer Science, pages 183–235, 1994. [2] E. Asarin, P. Caspi, and O. Maler. A Kleene Theorem for Timed Automata. LICS’97, pages 160–171. IEEE computer Society Press, 1997. [3] C.A.R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998. [4] Dang Van Hung. Toward a formal model for component interfaces for real- time systems. In FMICS ’05,pages 106–114, New York, 2005. ACM Press. [5] Dang Van Hung. Toward a Formal Model for Component Interfaces for Real- time Systems. FMICS’05, September 5–6, 2005, Lisbon, Portugal. [6] Pham Hong Thai, Dang Van Hung, Towards a Template Language for Component-based Programming. WORLDCOMP’07 Conference, June 25-28, 2007, USA. [7] Hung Le Dang, Dang Van Hung. Timing and Concurrency Specification in Component-based Real-Time Embedded Systems development. Proceedings of TASE’07, June 6-8, 2007, Shanghai, China. [8] Kurt Wallnau, Scott Hissam, and Robert Seacord, Component-Based Software Engineering (series), 2000 [9] Ananda Basu, Marius Bozga, and Joseph Sifakis. Modeling Heterogeneous Real-time Components in BIP. Proceedings of SEFM’06, pages 3–12, September 2006. IEEE Computer Society. [10] He Jifeng, Zhiming Liu, and Xiaoshan Li. A Theories of Contracts. Electronic Notes of Theoretical Computer Science, Volume 160 , pp. 173-195, 2006. [11] Barbora Zimmerová, Component-Based Systems (CBSs) (slide bài gi ảng), 2005