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

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