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

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 luận ở đây cách mà giao thức Pro được tính toán từ , 1,2iPro i = với hợp đồng 1 2Ctr Ctr>> . • Thứ nhất, hợp đồng ghép 1 2Ctr Ctr>> 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 1 2Pro Pro∪ phải bao gồm Pro . • Các phương thức m từ 2Ctr thì không được yêu cầu bởi 1Ctr có thể được sử dụng song song với các phương thức trong 1Ctr . Vậy Pro phải bao gồm 2 1( {! ,? | \ }*)2 p rPro Pro m m m Md Md∩ ∈ . • Câu hỏi ở đây là làm thế nào mà một phương thức m trong 2 1p rMd Md∩ lại được sử dụng với một phương thức trong 1pMd . 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: 2 2 1(Pr {! ,? | \ }*)1 2 1 p rPro Pro Pro Pro o m m m Md Md= ∪ ∪ ∩ ∈ Khi 1 2Ctr Ctr>> được định nghĩa, ta nói rằng 1Ctr có khả năng kết nối với 2Ctr . 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ế 1Ctr . Lí do là nó có thể yêu cầu cái gì đó từ môi trường mà 1Ctr không cung cấp. Định lí 1 Lấy 1Ctr là khả kết nối với 2Ctr . Nếu 2Ctr là đóng (có nghĩa là 2rI = ∅ ) thì 1 1 2( )Ctr Ctr Ctr>>⊑ . Chứng minh: 14 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à 1 2r pI I 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 ( , ), , , , ,p r p rCtr I I MSpec Init Inv Inv Pro= • Mcode gán mỗi phương thức op trong pMd một thiết kế xây dựng từ các toán tử cơ bản và phương thức trong r I như là ánh xạ của các vết trong thiết kế này mà bấy kì r op Md∈ được thay thể bởi ? !op op từ bắt đầu và kết thúc hành động, {? ! | } r m m m Md∈ đượ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à pInv đượ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 , , 1,2i i iComp Ctr Mcode i= = là các thành phần, với 1 2Ctr Ctr>> được định nghĩa. Lấy được Mcode′ từ 1Mcode bằng việc thay thế mỗi lần xuất hiện của 1 2( )r pop Md Md∈ ∩ bằng 2( )Mcode op trong dãy của 1Mcode . Thật dễ dàng để 15 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: 1 2 1 2 2 1, \Ctr Ctr Mcode Mcode 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ụ ( : , , ; : 1)dquadr in real a b c out real x mà đưa ra là một đáp án x1 của phương trình bậc 2 theo x2: 4 2 0ax bx c+ + = . Thành phần _double quadr yêu cầu dịch vụ ( : , , ; : 1)dquadr in real a b c out real x 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 2 0ax bx c+ + = . 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 • ax14 + bx12 + c = 0} } required method{ name{ quadr(in : real a, b, c; out : real x1)}, specification{ ac ≤ 0 • ax12+bx1+c = 0∧x1 ≥ 0} } protocol{ (?dquadr!dquadr)∗ ⊕ (?quadr!quadr)∗} 16 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 ( , , )pSI E Fd SMd= với pSMd 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 ys , , ,S Ctr SI SMSpec Inv Behav= với • ( , , )pSI E Fd SMd= 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 pSMd với một thiết kế , FPα với ( \ ( )) din out Fα ∪ ⊆ . • 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 { , | và }*pe m e E m SMd∈ ∈ . 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 17 • Một hợp đồng ( , ), , , , ,p r p rCtr I I MSpec Init Inv Inv Pro= với giao diện cung cấp rỗng, ( , )pI = ∅ ∅ . • Một hợp đồng hệ thống ys , , ,S 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 pSMd một thiết kế xây dựng từ các toán tử cơ bản và phương thức trong r I như là phép chiếu vết của thiết kế này trong bất kì phương thức r op Md∈ được thay thế bởi ? !op op (tự bắt đầu và kết thúc hành động), trên {? ,! | } r m m m Md∈ đượ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ả pop SMd∈ 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 ysS 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′ ′ ′= . 18 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 ( 1 nRES = {res ,...,res } 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 của FR. Lấy , 0{x,y} FP xα ≥≙ ≙ • f 2y x= và 133 266 1FR P P+ =≙ • r 19 (( 133 1 0.001) ( 133 0 0.0005))P l P l= ⇒ ≤ ∧ = ⇒ ≤ . 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ế 2 2 2, ,D FP FRα= được gọi là làm mịn từ 1 1 1, ,D FP FRα= (biểu diễn là 1 2D D⊑ ) nếu và chỉ nếu 2 1 2 1( , , , ) ( , )ok ok v v FP FP r l FR 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, 1 nr = (res ,...,res ). 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 1 1 1 1, ,D FP FRα= và 2 2 2 2, ,D FP FRα= là hai thiết kế có nhãn phụ thuộc thời gian. Vậy, 1 2; , ,D D Fp FRα≙ với • 1 1( )FP FP v′= và 2 2( )FP FP v= • 1 2 1 2 2 1 2, ( [ ] [ ] )1FR l l FR l / l FR l / l l l l∃ • ∧ ∧ = +≙ Từ đây về sau, ta sẽ sử dụng 1[ ]F x / 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 1 1 1 1, ,D FP FRα= và 2 2 2 2, ,D FP FRα= là các thiết kế có nhãn phụ thuộc thời gian. Giả thiết rằng 1 2α α∩ = ∅ . Vậy 1 2|| , ,D D FP FRα≙ khi 20 • 1 2α α α∪≙ và 1 2FP FP FP∧≙ • 1 2 1 2 1 1 2 2 2 1 2 1 2 , , , ( , / [ / , . ] max{ , } 1FR l l r r FR [l / l r r] FR l l r r l l l r r r ) ∃ • ∧ ∧ = ∧ = + ≙ với r1 và r2 là các véc tơ của biến tài nguyên và r1+r2 đã được định nghĩa. Điều kiện 1 2r r r= + biểu thị số lượng các biến tài nguyên đủ để thực thi 1D và 2D 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 fFP p R= ⊢ và r nFR p S= ⊢ . Vậy có một phép chuyển ( , , ) ( , , )cv r t v r t′ ′ ′→ nếu và chỉ nếu ( ) ( , ) ( ) ( , , , ) r p v R v v r r p r l t t S l r v v′ ′ ′ ′∧ ∧ = ∧ ∧ = − ∧ 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. 21 • 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 2 2 2 2 2 2 2, , , , ,Ctr Fd Md Rd MSpec Init Inv= là được làm mịn bằng hợp đồng 1 1 1 1 1 1 1, , , , ,Ctr Fd Md Rd MSpec Init Inv= , (được biểu diễn là 1 2Ctr Ctr⊑ ) nếu và chỉ nếu: • 1 2Fd Fd⊆ , 1 2Rd Rd⊆ và 2 1 1 1 2 1 1 1| | , | |Init Fd Init Fd Init Rd Init Rd= ≤ đối với các hàm 1 2, ,f f f và tập A. |f A biểu thị hạn chế của f trên A và 1 2f f≤ biểu thị rằng f1 và f2 có cùng miền và 1 2( ) ( )f x f x≤ với mọi x trong miền của chúng. • 1 2Md Md⊆ . • Với mọi phương thức op được khai báo trong 1Md thì 1 2( ) ( )Mspec op Mspec op⊑ và 2 1Inv Inv⇒ . 22 Ta lý giải định nghĩa này như sau. 2Ctr cung cấp tất cả các dịch vụ mà 1Ctr cung cấp và có thể cung cấp nhiều hơn nữa. 2Ctr phải có ít nhất cùng tài nguyên như là 1Ctr có. Điều kiện 2 1Inv Inv⇒ nói lên rằng thuộc tính của các biến được đảm bảo bởi 1Ctr thì cũng chắc chắn được đảm bảo bởi 2Ctr . Vật có thể thay thế 1Ctr bằng 2Ctr mà không bị mất bất kì một dịch vụ nào. Đặt , , , , , 1,2i i i i i iCtr Fd Md Rd Mspec Init 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à 1 2f Fd Fd∈ ∩ bao hàm cả 1 2( ) ( )Init f Init f= và 1 2op Md Md∈ ∩ bao hàm cả 1 2( ) ( )MSpec op MSpec op⇔ . Kết hợp hợp đồng 1 2Ctr Ctr∪ được định nghĩa như sau: 1 2 1 2 1 2 1 2 1 2 1 2 1 2 ( , ), , , , Fd Fd Md Md Rd Rd Ctr Ctr MSpec MSpec Init Init Inv Inv ∩ ∩ ∪ ∪ = ∪ ∧⊎ với 1 2( )( )Init Init x⊎ được định nghĩa là 1 2 1 2 { ( ), ( )} nê'u ( ) nê'u ( ) nê'u 1 2 1 2 2 1 max Init x Init x x dom(Init ) dom(Init ) Init x x dom(Init )\ dom(Init ) Init x x dom(Init )\ dom(Init ) ∈ ∩  ∈  ∈ Khi 1 2Ctr Ctr∪ được định nghĩa thì ta có thể nói 1Ctr và 2Ctr 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 1 1 1, ( ( [ / ] [ / ]))r r r r FR r RES FR r 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 23 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; 24 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{ 25 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 1( , , )call Comp C op , với 1op 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 1( , )op 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ụ 26 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 C opi , 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 C opi bao hàm đặc tả chức năng của C opi 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. 27 • 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 , , , , , 1,2i i i i i iC Ctr Dep SDep Mcode Inv 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 1 2( ) ( )Mcode op Mcode op≡ đối với tất cả 1 2op Md Md∈ ∩ . Tổ hợp 1 2C C∪ được định nghĩa là: 1 2 1 2 1 2 1 2 1 2, , , ,Ctr Ctr Dep Dep SDep SDep Mcode Mcode SInv SInv∪ ∪ ∪ ∪ ∪ 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 ( ( ( )) ( )) U Dep Inv Ctr U SInv U ∈ ∧∧ . Điều kiện ( ( ))Inv Ctr U trên 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ó 28 ( , ) , , 0Schedule Comp C skip 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 0l 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ó ( ) ( ), , x Schedule Com SDep U FP l n 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 Comp2 được làm mịn bởi Comp1 nếu và chỉ nếu Comp2 tốt hơn Comp1 theo nghĩa Comp2 cung cấp nhiều hơn các dịch vụ của Comp1 nhưng cần ít dịch vụ hơn Comp1 và điều kiện lập lịch trong Comp2 kém hơn trong Comp1 (có nghĩa là Comp2 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 Comp1 thì cũng hoạt động với Comp2). Vậy ta có định nghĩa cho làm mịn thành phần như sau: (định nghĩa 11) Lấy , , , , , 1,2i i i i i iComp Ctr Dep SDep Mcode SInv i= = là các thành phần bị động. Comp1 được gọi là làm mịn bởi Comp2 (được biểu thị là 1 2Comp Comp⊑ ) nếu và chỉ nếu: • 1 2Ctr Ctr⊑ (tức là Comp2 cung cấp nhiều dịch vụ hơn Comp1). • 2 1Dep Dep⊆ , 2 1SDep SDep⊆ và 1 2SInv SInv⇒ (tức là Comp2 không cần nhiều dịch vụ từ hệ thống như Comp1 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 29 trường và đồng hồ bên trong nó. Một luồng T được định nghĩa always follows D 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 “ follows D 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 VU Dep* 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. 1Comp và 2Comp là các thành phần bị động sao cho 1 2Comp Comp⊑ và 1Comp S∈ . S1 có được bằng việc thay thế 1Comp bằng 2Comp và đồng thời thay thế mỗi biến cố của 1Comp trong hệ thống S bằng một biến cố của 2Comp . Do vậy, S1 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 1Comp bằng các biến cố của 2Comp 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 ( ) ( ( ( )) ( )) U Dep C Inv Ctr U SInv U ∈ ∧∧ . Từ định nghĩa 11 ở trên về làm mịn thành phần, nó kéo theo 1 1 2 2( , ) || ( , ) ||Schedule Comp Comp Comp op Schedule Comp Comp Comp opi i⊑ cho bất kì phương thức op nào trong 1Comp . 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à 2 1( ) ( )SInv Comp SInv Comp⇒ , ta có ( ) ( )Mspec op Mcode op⊑ giữ với giả thiết ( ) ( ( ( )) ( )) U Dep C Inv Ctr U SInv U ∈ ∧∧ . 30 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ả f{src}, true src = current_position,0 < l 1′ ≤⊢ . Mặc dù mã chương trình không đượ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à 31 { , , }, _ _ _ ,0 1fsrc dstn map true map map for the area l′ = < ≤⊢ và _ ( : , : , : )find route in src in dstn out route với đặc tả là { , , }, _ _ , 75 es 1 4 src dstn route true route route to the_destination MHz proc or memory 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 75 _MHz processor được khởi tạo là 1. Đoạn mã của phương thức này như sau: : _ ; ( ( , ) || . _ os( )); ( ( , ) || . _ ( , , )); _ ( ); dstn read dstn Schedule Controller GPS GPS get 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 14l< ≤ . 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 32 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 _ _ after _ _ _ find route handle 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. 33 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. 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