Khóa luận Mô hình hóa các hệ thống dựa trên các thành phần
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Nguyễn Văn Nghiệp
MÔ HÌNH HÓA
CÁC HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
HÀ NỘI - 2009
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Nguyễn Văn Nghiệp
MÔ HÌNH HÓA
CÁC HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
Cán bộ hướng dẫn: TS. Đặng Văn Hưng
HÀ NỘI - 2009
TÓM TẮT NỘI DUNG KHÓA LUẬN
Mục đích của khóa luận là nghiên cứu và tìm hiểu các khái niệm liên quan đến
thành phần phần mềm, hệ thống dựa trên thành phần và hệ thống dựa trên thành phần
thời gian thực. Đầu tiên tôi sẽ trình bày tổng quan về việc xây dựng hệ thống dựa trên
thành phần và các lợi ích của nó trong việc phân tích, thiết kế các hệ thống thông tin.
Tôi sẽ trình bày việc mô hình hóa hình thức hệ thống dựa trên thành phần dựa trên nền
tảng của UTP (Unifying Theory of Programming). Tôi sẽ trình bày về các khái niệm
trong mô hình hệ thống dựa trên thành phần như: giao diện, hợp đồng, thành phần, kết
hợp thành phần. Các định nghĩa này sẽ đóng vai trò nền tảng cho việc phát triển các
khuôn mẫu cho thành phần. Một hợp đồng được định nghĩa sẽ bao hàm đặc tả của các
phương thức, một thành phần được định nghĩa là một cài đặt của một hợp đồng. Cài
đặt này có thể yêu cầu các dịch vụ từ các thành phần khác với một vài giả thiết về lập
lịch cho việc giải quyết xung đột các phương thức dùng chung và sử dụng các tài
nguyên hiện có trong xử lí song song. Trong khóa luận tôi sẽ trình bày sâu hơn về mô
hình thành phần thời gian thực dựa trên các khái niệm, các định nghĩa đã được nêu ra
trước đó. Với phần này, tôi đưa ra một mô hình giao diện thành phần cho hệ thống dựa
trên thành phần thời gian thực. Cùng với đó, đặc tả phương thức sẽ được mở rộng với
một ràng buộc về thời gian là một quan hệ giữa tài nguyên có sẵn và lượng thời gian
tiêu tốn để thực thi phương thức. Với mô hình đó, nó hỗ trợ sự phân tách giữa yêu cầu
chức năng, yêu cầu phi chức năng và kiểm chứng hợp phần hình thức của hệ thống
dựa trên thành phần thời gian thực. Cuối cùng tôi cho một ví dụ minh họa cho mô hình
được nghiên cứu trong luận văn này.
LỜI CẢM ƠN.
Em xin chân thành cảm ơn các thầy giáo, cô giáo trong khoa đã giúp đỡ em trong
thời gian học tập tại khoa để em có những kiến thức nền tảng cho việc nghiên cứu
khoa học để áp dụng vào việc nghiên cứu những lý thuyết, kiến thức liên quan đến đề
tài khóa luận tốt nghiệp. Đặc biệt, em xin gửi lời cảm ơn sâu sắc đến Tiến sĩ Đặng Văn
Hưng, người đã luôn quan tâm, giúp đỡ, hướng dẫn em trong suốt quá trình nghiên
cứu và trình bày khóa. Thầy đã giúp em rất nhiều trong việc tiếp cận các vấn đề mà em
còn chưa hiểu rõ, thầy luôn nhiệt tình chỉ dạy cho em những kinh nghiệm quý báu khi
tiếp cận các vấn đề mới. Em cũng xin cảm ơn tới gia đình. Gia đình là nguồn lực động
viên em khi làm khóa luận này.
Sinh viên
Nguyễn Văn Nghiệp
MỤC LỤC
LỜI MỞ ĐẦU ................................................................................................................1
1. TỔNG QUAN VỀ HỆ THỐNG DỰA TRÊN CÁC THÀNH PHẦN ...................3
1.1. Hệ thống dựa trên thành phần là gì?................................................................3
1.1.1. Thành phần phần mềm..........................................................................................3
1.1.2. Hệ thống dựa trên thành phần..............................................................................4
1.2. Hệ thống thời gian thực là gì? ...........................................................................6
2. KIẾN TRÚC HỆ THỐNG DỰA TRÊN THÀNH PHẦN......................................7
3. TÌM HIỂU MÔ HÌNH THÀNH PHẦN ..................................................................8
3.1 Thiết kế dưới dạng công thức logic....................................................................8
3.2 Giao diện và hợp đồng ........................................................................................9
3.3. Kết hợp hợp đồng.............................................................................................11
4. MÔ HÌNH THÀNH PHẦN THỜI GIAN THỰC.................................................18
4.1. Các thiết kế có nhãn ràng buộc về thời gian sử dụng như dịch vụ..............18
4.2. Sử dụng các ngôn ngữ hình thức có nhãn ràng buộc về thời gian để đặc các
giao thức tương tác thời gian thực và đặc tả tiến trình. ......................................22
4.3. Các hợp đồng thời gian thực. ..........................................................................23
4.4. Thành phần bị động .........................................................................................25
4.5. Thành phần chủ động ......................................................................................28
5. ỨNG DỤNG MÔ HÌNH THÀNH PHẦN TRONG HỆ THỐNG NHÚNG.......30
KẾT LUẬN ..................................................................................................................33
BẢNG KÍ HIỆU, VIẾT TẮT
=
Bằng
P Q
P và Q
P Q
P hoặc Q
¬ P
Phủ định P
Nếu P thì Q
P ⇒ Q
x :T • P
x :T • P
Tồn tại x trong tập T sao cho P
Mọi x trong T sao cho P
Thuộc
Không thuộc
{}
Tập rỗng
{a}
Tập đơn chứa duy nhất phần tử a
{x :T | P(x)}
{ f (x):T | P(x)}
Tập hợp tất cả x trong T sao cho P(x)
Tập hợp giá trị của hàm f(x) sao cho P(x)
S T
S ∩ T
S \ T
S hợp T
S giao T
S trừ T
S T
S T
S chứa trong 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
Chương trình đạt đến trạng thái ổn định
P bao hàm Q mọi nơi
′
ok
P
⇒
Q
′
P Q
Quan hệ ok P
⇒
ok
Q
P ⊒Q
P là một bản làm mịn của Q có nghĩa là
(t,Q) được làm mịn từ (s,P)
P
⇒
Q
(s,P) ⊑ (t,Q)
P || Q
Phân tách hợp phần song song của P và Q
Hợp phần song song với toán tử M
Gán giá trị e cho biến x.
M
x := e
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
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
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
• Giao diện
• Xác định duy nhất
• Khả năng sử dụng lại
• Sẵn sàng để sử dụng
• Client anonymity
Bên cạnh đó, thành phần còn có các đặc tính khác như:
• Độc lập về ngôn ngữ
• Độc lập về nền tảng
• Khả năng cấu hình
3
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
• Không có mã lệnh (hộp đen)
• Được phát triển riêng rẽ
• Trong hầu hết các trường hợp được
thiết kế cho một hệ thống
• Ngữ cảnh phát triển không thay đổi
được sau khi biên dịch
• 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
• 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
• 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
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
đặ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
op(in,out)
in
out
là tập hợp các biến.
dấu hiệu của dạng thức
Định nghĩa 1
với
và
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
′
x
diện bởi những biến đầu tiên trong tập hợp
{
|
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ế
D
=
α
,
FP là được làm mịn từ thiết kế D2
=
α
,
FP (có nghĩa là
1
1
2
D ⊑ D2 ) nếu và chỉ nếu
1
8
′
,
′
v
(
ok
,
ok
v
,
•
FP ⇒ FP
)
2
1
′
v
với
v
,
là các vectơ của các biến chương trình.
Dãy thành phần
Lấy FP và D2
D
=
α
,
=
α
,
FP là các thiết kế sau đó
D
;
D2
≙
α
,
FP
FP
1
1
2
1
Với FP
≙
m
•
FP
(
m
)
FP
(
m
)
với giả sử là FP
=
FP
(
v
)
và FP
=
(
v
)
.
1
2
1
1
2
2
Từ đây về sau, tôi sử dụng
bởi x1 trong biểu thức F.
F
[
x1
\x
]
để biểu diễn biểu thức kết quả từ việc thay thế x
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
Mdr . 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:
,
Ir
)
với Ip = Fdp ,Mdp
và
I
=
Fdr
,
r
Một hợp đồng là một tập hợp hữu hạn I,Init,MSpec,Invp ,Invr ,Pro với
= (Ip Ir là một giao diện. Lấy Md Mdr Mdp Fd Fdr Fdp
•
I
,
)
=
,
=
• 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 Mdp với một thiết kế
α
, FP
với
(α
\ (in out)) Mdp
• 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
9
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
{
m
?,
phép chiếu trên
Pro là được chấp nhận.
m
!| m Fdp}* {
m
?,m!| m Fdr}*. Chỉ có hành vi của các
{
m
?, !| m Fdp}* và {m?,m!| m Fdr}* thuộc về
m
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, http://en.wikipedia.org/wiki/Communicating_sequential_processes
10
Hợp đồng Ctr = (Ip1,Ir1),MSpec1,Init1,Invp1,Invr1,Pro1 được làm mịn của
1
đồng Ctr = (Ip2,Ir2 ),MSpec2,Init2,Invp2,Invr2,Pro2
được biểu diễn là
2
Ctr ⊑ Ctr nếu và chỉ nếu:
1
2
•
Fdp1 Fdp2
,
Fdr1 Fdr2 , và Init2 Fdp1
=
Init1 Fdp1 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 Mdp2 và MDr1 Mdr2
•
.
• Đối với tất cả phương thức op được khai báo trong Mdp1 thì
MSpec1 op ⊑ MSpec2 op và Invp2 ⇒ Invp1
(
)
(
)
.
• Đối với tất cả phương thức op được khai báo trong Mdr2 thì
MSpec2 (op) ⊑ MSpec1(op) và Invr1 ⇒ Invr2
.
•
Pro1 {m?,m!| m Fdp1} Pro2 {m?,m!| m Fdp1} và
Pro2 {m?,m!| m Fdr2} Pro1 {m?,m!| m Fdr2}
.
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 Invr1 ⇒ Invr2 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
11
Lấy Ctr = (Ipi ,Iri ),MSpeci ,Initi ,Invpi ,Invri ,Proi ,i =1,2, là 2 hợp đồng có
i
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
(Ip1 Ip2,Ir1 Ir2 ),MSpec1 MSpec2,Init1 Init2,Invp1
Ctr Ctr =
1
2
Invp2,Invr1 Invr2,Pro1 Pro2 (Pro1 Pro2 )
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 Pro2 đã 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
Ctr = (Ipi ,Iri ),MSpeci ,Initi ,Invpi ,Invri ,Proi ,i =1,2 là các hợp đồng có các tập
i
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 ∩ Fdp2 ) suy ra Init1( f ) = Init2 ( f ) và
op (Mdp1 ∩ Mdp2 ) (Mdr1 ∩ Mdr2 ) suy ra MSpec1(op)
định rằng Ir1 Ip2 Invp2 Invr1 MSpec1(op) ⊑ MSpec2 (op) đối với tất cả
op Mdr1
MSpec2 (op). Giả
,
⇒
,
.
Cắm đầy đủ của Ctr tới Ctr được biểu diễn là Ctr >> Ctr được định nghĩa là:
1
2
1
2
(Ip1 Ip2,Ir2 ),MSpec2,
Ctr >> Ctr =
1
2
Init1 Fdr1 ⊎ Init2 ,Invp1 Invp2,Invr2,Pro
Ở đây, ta nhận thấy tập các yêu cầu không phải là Ir1 Ir2 mà chỉ là Ir2 bởi vì
do Ctr được làm mịn từ Ctr nên Ctr có đầy đủ tập các yêu cầu của Ctr1. Và vì thế,
2
1
2
Ctr cắm đầy đủ vào Ctr
.
1
2
Với (Init1 ⊎ Init2 )(x) được định nghĩa là
12
Init (x) = Init (x) nê'u x dom(Init ) ∩ dom(Init )
1
2
1
2
Init (x) nê'u x dom(Init ) \ dom(Init )
1
1
2
Init2 (x) nê'u x dom(Init2 ) \ dom(Init1)
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 Ctr >> Ctr
.
1
2
• Thứ nhất, hợp đồng ghép Ctr >> Ctr cũng phải cho phép các phương thức
1
2
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 Pro2 phải bao gồm Pro
.
• Các phương thức m từ Ctr2 thì không được yêu cầu bởi Ctr có thể được sử
1
dụng song song với các phương thức trong Ctr1. Vậy Pro phải bao gồm
Pro (Pro2 ∩{!m,?m | m Mdp2 \ Mdr1}*)
.
• Câu hỏi ở đây là làm thế nào mà một phương thức m trong Mdp2 ∩ Mdr1 lại
được sử dụng với một phương thức trong Mdp1 . 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 Pro2 Pro1 (Pro2 ∩{!m,?m | m Mdp2 \ Mdr1}*)
Khi Ctr >> Ctr được định nghĩa, ta nói rằng Ctr có khả năng kết nối với Ctr
.
1
2
1
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ế Ctr1. Lí do là nó có thể yêu cầu cái gì đó từ môi
trường mà Ctr không cung cấp.
1
Định lí 1
Lấy Ctr là khả kết nối với Ctr2 . Nếu Ctr là đóng (có nghĩa là Ir2 = ) thì
1
2
Ctr ⊑ (Ctr >> Ctr2 )
.
1
1
Chứng minh:
13
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
ꢀ
Ip2 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 = (Ip ,Ir ),MSpec,Init,Invp ,Invr ,Pro
•
Mcode gán mỗi phương thức op trong Mdp 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 Mdr được thay thể bởi ?op!op từ bắt đầu và kết thúc
hành động, {?m!m | m Mdr} đượ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à Invp đượ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 ,Mcodei ,i =1,2 là các thành phần, với Ctr >> Ctr được
i
1
2
′
định nghĩa. Lấy được Mcode từ Mcode bằng việc thay thế mỗi lần xuất hiện của
1
op (Mdr1 ∩ Mdp2 ) bằng Mcode2 (op) trong dãy của Mcode1 . Thật dễ dàng để
14
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:
′
Ctr >> Ctr ,Mcode1 Mcode2 Md2 \ Md1 là một thành phần.
1
2
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 x1) mà đưa ra là một đáp án x1 của phương trình
bậc 2 theo x2: ax4 + bx2 + c = 0. Thành phần double_ quadr yêu cầu dịch vụ
dquadr(in:real a,b,c;out :real x1) 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
•
ax14 + bx12 + c = 0}
}
required method{
name{ quadr(in : real a, b, c; out : real x1)},
ax12+bx1+c = 0∧x1 ≥ 0}
specification{ ac ≤ 0
•
}
protocol{ (?dquadr!dquadr)∗ ⊕ (?quadr!quadr)∗}
15
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,SMdp ) với SMdp 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
SysCtr = SI,SMSpec,Inv,Behav
với
•
•
SI = (E,Fd,SMdp ) 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 SMdp với một thiết kế
\ (in out)) Fd
α
,FP
với
(α
.
•
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 SMdp}*. 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
thống cung cấp dãy các sự kiện như là biến cố trong
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ô
α
trong Behav là nếu môi trường hệ
α
do vậy hệ thống cung cấp dãy
α
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
• Một hợp đồng Ctr = (Ip ,Ir ),MSpec,Init,Invp ,Invr ,Pro với giao diện
cung cấp rỗng, Ip = ( , )
.
• Một hợp đồng hệ thống SysCtr = 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 SMdp
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 Mdr
được thay thế bởi ?op!op (tự bắt đầu và kết thúc hành động), trên
{?m,!m | m Mdr} đượ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 SMdp
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
SysCtr . 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
′′
′′
′′
′
′′
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 ,...,resn } 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
α
≙
{x,y},FP
≙
x ≥ 0
•
f y2 = x và FR
≙
P133+ P266 =1•
r
18
((P133 =1⇒ l ≤ 0.001) (P133 = 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
,
FR2 được gọi là làm mịn từ D =
α
,
FP FR
,
2
1
1
1
(biểu diễn là 2 ) nếu và chỉ nếu
D
⊑
D
1
′
,
′
(
ok
,
ok
v
,
v • FP
⇒
FP1) (
r
,
l • FR2
⇒
FR
)
2
1
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 ,...,resn ). 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 D = α1
,
FP
,
FR và D2 = α 2
,
FP FR2 là hai thiết kế có nhãn phụ
,
1
1
1
2
thuộc thời gian. Vậy, D ;D2 ≙
α
,Fp,FR với
1
′
•
•
FP = FP
(
v
)
và FP = FP
(v)
1
1
2
2
FR
≙
l1
,
l2 •
(
FR
[l1 / l
]
FR2
[l2 / l
]
l = l1 + l2
)
1
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 D = α1
,
FP
,
FR và D2 = α 2
,
FP FR2 là các thiết kế có nhãn phụ
,
1
1
1
2
thuộc thời gian. Giả thiết rằng α1
∩
α 2
=
. Vậy D || D2 ≙
α
,FP,FR khi
1
19
•
•
α
≙
α1 α 2 và FP ≙ FP FP
1
2
FR ≙ l1,l2,r ,r • (FR [l1 / l,r / r]
1
2
1
1
với r1 và r2 là các véc tơ
FR2[l2 / l,r .r] l = max{l1,l2} r = r + r )
2
1
2
của biến tài nguyên và r1+r2 đã được định nghĩa.
Điều kiện biểu thị số lượng các biến tài nguyên đủ để thực thi
r
=
r
+
r
D
và
1
2
1
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 f R và FR = pr
S
.
n
c
′ ′ ′
Vậy có một phép chuyển (v,r,t) →(v ,r ,t ) nếu và chỉ nếu
′
′
′
′
p(v) R(v,v ) r = r pr (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.
20
• 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
Ctr = Fd2,Md2 ,Rd2,MSpec2,Init2,Inv2
2
là được làm mịn bằng hợp đồng
Ctr = Fd1,Md1 ,Rd1,MSpec1,Init1,Inv1
,
1
(được biểu diễn là Ctr
⊑
Ctr2 ) nếu và chỉ nếu:
1
•
Fd1 Fd2
đối với các hàm f , f1, f2 và tập A. f | A biểu thị hạn chế của f trên A và
f1 f2 biểu thị rằng f1 và f2 có cùng miền và f1(x) f2 (x) với mọi x
trong miền của chúng.
,
Rd1 Rd2 và Init2 | Fd1 = Init1 | Fd1,Init2 | Rd1 ≤ Init1 | Rd1
≤
≤
•
Md1 Md2
.
• Với mọi phương thức op được khai báo trong Md1 thì
Mspec1(op)
⊑
Mspec2 (op) và Inv2
⇒
Inv1
.
21
Ta lý giải định nghĩa này như sau. Ctr cung cấp tất cả các dịch vụ mà Ctr cung
2
1
cấp và có thể cung cấp nhiều hơn nữa. Ctr phải có ít nhất cùng tài nguyên như là Ctr
2
1
có. Điều kiện Inv2
⇒
Inv1 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 Ctr2 . Vật có thể thay thế Ctr bằng Ctr mà
1
2
không bị mất bất kì một dịch vụ nào.
Đặt Ctr = Fdi ,Mdi ,Rdi ,Mspeci ,Initi ,i =1,2 là các hợp đồng có ràng buộc
i
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 ∩ Fd2 bao hàm cả Init1( f ) = Init2 ( f ) và op Md1 ∩ Md2 bao hàm cả
MSpec1(op)
MSpec2 (op). Kết hợp hợp đồng Ctr Ctr được định nghĩa như
1
2
(Fd1 ∩ Fd2,Md1 ∩ Md2 ),Rd1 Rd2,
sau: Ctr Ctr =
1
2
MSpec1 MSpec2,Init1 ⊎ Init2,Inv1 Inv2
với (Init1
⊎
Init2 )(x) được định nghĩa là
max{Init (x),Init (x)} nê'u x dom(Init1 )∩ dom(Init2 )
1
2
Init (x)
nê'u x dom(Init1 )\ dom(Init2 )
nê'u x dom(Init2 )\ dom(Init1 )
1
Init2 (x)
Khi Ctr Ctr được định nghĩa thì ta có thể nói Ctr và Ctr có thể rút gọn.
1
2
1
2
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,r
•
(r
≥
r
⇒
(FR[r / RES] FR[r / RES]))
⇒
.
1
1
1
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
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
Tải về để xem bản đầy đủ
41 trang
26/05/2025
220
Bạn đang xem 30 trang mẫu của tài liệu "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ải tài liệu gốc về máy hãy click vào nút Download ở trên.
File đính kèm:
- khoa_luan_mo_hinh_hoa_cac_he_thong_dua_tren_cac_thanh_phan.pdf
