ðẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ðẠI HỌC CÔNG NGHỆ

LƯƠNG THANH HOÀI

THẨM ðỊNH CÁC THÀNH PHẦN
CỦA HỆ THỐNG LAI THỜI GIAN THỰC
KẾT NỐI ðỒNG BỘ
DỰA TRÊN LOGIC TÍNH TOÁN KHOẢNG DC
(DURATION CALCULUS)
Ngành: Công nghệ thông tin
Chuyên ngành: Công nghệ phần mềm
Mã số: 60 48 10

LUẬN VĂN THẠC SĨ
NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ðặng Văn Hưng

Hà Nội - 2010


LỜI CAM ðOAN
Tôi xin cam ñoan các thông tin, số liệu, kiến thức trích dẫn trong luận văn là thu thập
từ các nguồn chính thống, ñăng tải trên các tạp chí chuyên ngành, sách, báo…

Các giải pháp ñưa ra là của bản thân rút ra từ quá trình nghiên cứu tổng hợp.

Tác giả ký tên

Lương Thanh Hoài




MỞ ðẦU
Tóm tắt – ðể xác ñịnh và kiểm chứng hệ thống lai phân tán thời gian thực kết nối
ñồng bộ (distributed synchronously communication real-time hybrid system), bộ ba
Hoare cổ ñiển (classical Hoare triples) ñược mở rộng với việc nhúng hành vi
(behavior) thời gian thực của chương trình. Nhờ vào việc mở rộng này một Hệ Thống
Chứng Minh Có Tính Kết Hợp (Compositional Proof System) dựa trên Sự Mở Rộng
về Thời Gian ðơn ðiệu Yếu (Weakly Monotonic Time Extention) của DC* (WDC*)
ñã ñược hình thành. Lợi thế của luật chứng minh kết hợp (compositional) là nó thực
hiện việc chia một hệ thống lớn thành các phần nhỏ có thể quản lý ñược sau ñó chứng
minh tính ñúng của toàn bộ hệ thống từ việc chứng minh tính ñúng của các thành phần
hợp thành. WDC* cung cấp bản chất ñơn giản trong việc lý luận về thiết kế của những
chương trình thời gian thực bằng những phương tiện của giả thuyết ñồng bộ lý tưởng
(true synchrony) và tính toán siêu trù mật (super-dense computation). ðiều này ñược
mô phỏng bằng quá trình kiểm chứng những thuộc tính an toàn của việc tránh xung
ñột trong Hệ Thống ðiều Khiển Tàu ðiện Châu Âu (European Train Control System –
ETCS), phiên bản ñầy ñủ các tham số.
Giới thiệu - Với sự tăng trưởng nhanh chóng của mạng cùng sự phát triển mạnh về
khả năng tính toán, nhu cầu cho các hệ thống quy mô lớn và phức tạp ñã tăng lên ñáng
kể. Nhiều hệ thống hỗ trợ hoặc thay thế kiểm soát của con người trong các hệ thống
ñòi hỏi an toàn cao như: Hệ thống ñiều khiển ñiện tử trên máy bay, hệ thống ñiều
khiển tàu, hệ thống ñiều khiển nhà máy năng lượng hạt nhân v…v. Lỗi trong các hệ
thống ñòi hỏi an toàn cao này có thể dẫn ñến những thảm họa lớn và lấy ñi mạng sống
của con người. Vì vậy, hệ thống an toàn cao cần duy trì những thuộc tính ñảm bảo cao.
ðể phù hợp với những thuộc tính ñảm bảo cao, những hệ thống này thường chia sẻ tài
nguyên giữa nhiều tác tử tính toán chủ ñộng ñồng thời và phải tuân thủ chặt chẽ những
ràng buộc thời gian thực. Hệ thống lai thời gian thực phân tán dựa trên kết nối ñồng bộ
là một trong những hệ thống an toàn cao, nó ñóng một vai trò rất quan trọng trong
những hệ thống có qui mô lớn.
Tuy nhiên, tính ñồng thời, sự ràng buộc thời gian, giao diện liên tục và rời rạc làm cho

tiến trình thiết kế dựa trên mô hình của hệ thống ñiều khiển tàu ñiện ñể chia việc kiểm
chứng toàn bộ vấn ñề của hệ thống thành các phần nhỏ hơn có thể kiểm chứng ñược
bằng các công cụ kiểm chứng tự ñộng ñối với các lớp con của những hệ thống thời
gian thực [6], [7].
Tuy nhiên trong những trường hợp trên một số hệ thống chứng minh có tính kết hợp
ñược ñề xuất dựa trên ECTL (Existential Computation Tree Logic) thay vì sự trừu
tượng hóa ñồng bộ lí tưởng, ñã dẫn ñến việc hiểu và lí giải hành vi của hệ thống lai
thời gian thực rất phức tạp. Một số khác ñược ñề xuất cho những biến chia sẻ dựa trên
lược ñồ kết nối ñồng bộ thay vì truyền thông ñiệp dựa trên lược ñồ kết nối ñồng bộ.
Một số kết quả khác ñưa ra những luật phân chia chỉ tương thích tốt trong một số
trường hợp ñặc biệt (như là kiểm chứng tự ñộng của các tác tử giao thông (traffic)). Và
một số kết quả không thể giải quyết ñược vấn ñề không nhất quán giữa mô hình liên
tục sử dụng trong ñặc tả và mô hình rời rạc sử dụng trong cài ñặt.
Thay vào ñó, chúng ta biểu diễn một hệ thống những luật kiểm chứng có tính kết hợp
dựa trên WDC* cho hệ thống lai thời gian thực kết nối ñồng bộ. Sự ñóng góp của bài
luận này là:
1) Sử dụng logic khoảng dựa trên WDC* ñể thích ứng với sự trừu tượng của
ñồng bộ lí tưởng, ñây là yếu tố cơ bản trong việc ñơn giản hóa về mặt bản chất cho
việc hiểu và lí giải về hành vi của hệ thống thời gian thực.


3
2) Làm cho việc sử dụng những luật ñối với giao diện rời rạc tương thích
tốt trong quá trình phân tích và kiểm chứng hệ thống lai từ ñó giải quyết sự không nhất
quán giữa những mô hình liên tục sử dụng trong ñặc tả và mô hình rời rạc sử dụng
trong cài ñặt.
3) Theo cú pháp và những ngữ nghĩa của những ngôn ngữ kết nối ñồng bộ,
chúng ta mô tả hệ thống chứng minh có tính kết hợp cho những hệ thống lai thời gian
thực, nó giúp giải quyết một cách hiệu quả tiến trình phân tích và kiểm chứng những
hệ thống qui mô lớn.

giả sử rằng một trạng thái có hữu hạn biến ñổi trong một khoảng thời gian giới hạn.
Một biểu thức trạng thái ñược thông dịch như là một hàm với các biến trạng thái và
các phép toán logic.
Với một biểu thức trạng thái bất kỳ S, duration của nó ñược ký hiệu bởi
thông dịch I của các biến trạng thái và một khoảng, duration

∫S

∫ S . Cho một

ñược thông dịch như

là tổng ñộ dài thời gian trong một khoảng mà tại ñó S hiện hữu. Vì vậy bất kỳ ñoạn
[t,t’], trình dịch I ( ∫ S )([t , t ']) ñược ñịnh nghĩa là

∫

t

t'

I ( S )(t ) dt .

Một công thức ϕ ñược thỏa mãn bởi một trình thông dịch trong một khoảng thời gian
[t,t’] khi nó ñược ñánh giá là ñúng với trình thông dịch ñó trên khoảng thời gian ñã
cho. Ta kí hiệu ñiều này bởi: I ,[t , t '] |= ϕ .
Cho một máy thông dịch I, một biểu thức ϕ ψ là ñúng trên [t,t’’] nếu tồn tại t’ sao
cho t≤t’≤t’’ và ϕ và ψ là ñúng lần lượt trên [t,t’] và [t’,t’’].
Chúng ta cần chú ý các ký hiệu viết tắt sau:


2

1

1

2

1

2

2

[l = 0 / A]ϕ ϕ⇒[ A S / A]ϕ
ϕ⇒[ A ¬S / A]ϕ
( IR1 )
[true / A]ϕ
[l = 0 / A]ϕ ϕ⇒[ S A / A]ϕ
A / A]ϕ
ϕ ⇒ [ ¬S
( IR2 )
[true / A]ϕ
( IR3 )

∀k < ω  ( S ∨ ¬S ) k / A ϕ
[true / A]ϕ

( DC1* ) l = 0⇒ϕ*
( DC2* ) (ϕ* ϕ)⇒ϕ*

nghĩa là với mọi i ∈ π2 (WT ) , chúng ta có θ ( p )(b) = θ ( p )(e) cho tất cả b, e ∈ Per (WT , i ) .
(Trong ñó Per (WT , i ) ≙ {t | (t , i) ∈ WT } ám chỉ khoảng thời gian của pha thứ i)
Hành vi θ cũng gán một số thực với mỗi biến toàn cục x ∈ Gvar . Vì vậy,
θ ∈ ( Pvar → WT → {0,1}) × (Gvar → ℝ )

Một hành vi θ’ ñược gọi là x-variant của θ nếu chúng gán cũng giá trị cho tất cả các
biến ngoại trừ x.
Với mỗi mệnh ñề P, xác ñịnh nghĩa một hàm bộ phận (ánh xạ bộ phận)
θc ( P ) ∈ T → Bool của macro-time như sau:
θc ( P )(t ) = θ ( P )(t , i ) nếu {i | (t , i) ∈ WT } chỉ gồm 1 giá trị

=–

trong các trường hợp khác


7

Chú ý rằng θc ( P) là không xác ñịnh tại tập rời rạc các ñiểm. Tuy nhiên, với
TM = ( ℝ 0 ,
V ( ∫ P )(θ ,[b, e]) =

π1 ( e )

∫

π1 ( b )

V ( x)(θ ,[b, e]) = θ ( x)

θc ( P ) dt


8
Các trường hợp khác có thể tham khảo trong [2], [5], và ñược bỏ qua.
(θ ,[b, e]) |= ⌈ P ⌉0 iff b = e ∧ θ ( P )(b) = 1
(θ ,[b, e]) |= t1 = t2 iff V (t1 )(θ ,[b, e]) = V (t2 )(θ ,[b, e])
(θ ,[b, e]) |= t1 < t2 iff V (t1 )(θ ,[b, e]) < V (t2 )(θ ,[b, e])
(θ ,[b, e]) |= X iff θ ( X )[b, e] = 1
(θ ,[b, e]) |= D1 D2 iff ∃m ∈ WT : b ≤ m ≤ e.
(θ ,[b, m]) |= D1 ∧ (θ ,[m, e]) |= D2
(θ ,[b, e]) |= D* iff b = e | ∃m1 ,....mn ∈ WT : b = m1 < ... < mn = e.
(θ ,[mi , mi+1 ]) |= D ∀i = 1, 2...n −1

ðặc biệt, ta có :
Pti = ⌈1⌉0 , Exti ≙ ¬Pti , Ptl ≙ l = 0, Extm ≙ ¬Ptl
Unit ≙ Exti ∧ ¬( Exti
1

0

minh của DC (xem [2] ñể có chi tiết). Tất cả các tiên ñề cho Durations (nghĩa là DCA1 tới DC-A6 trong [2]) là ñúng và ñược bao gồm trong WDC. Luật qui nạp
(induction rule) sẽ ñược thảo luận riêng bên dưới.
Một formula D ñược gọi là rigid nếu nó không chứa biến khoảng hoặc hạng tử
l , η hoặc là công thức con ⌈ P ⌉0 , Ptl .


9
A0
A1
A2
R
B

0≤l∧0≤η
⌢
⌢
⌢
(( D1 D2 ) ∧ ¬( D1 D3 )) ⇒ ( D1 ( D2 ∧ ¬D3 ))
⌢
⌢
⌢
⌢
D1 ( D2 D3 ) ⇔ ( D1 D2 ) D3
⌢
D1 D2 ⇒ D1 if rigid D1
⌢
⌢
(∃x.D1 ) D2 ⇒ ∃x.( D1 D2 )

Các luật suy diễn của IL (nghĩa là MP,G,N1, N2, M1, M2 trong [2]) ñược bao gồm

⌢
(0 ≤ x ∧ 0 ≤ y ) ⇒ ((l = x + y )⇔ (l = x l = y ))
⌢
(0 ≤ x ∧ 0 ≤ y ) ⇒ ((η = x + y )⇔ (η = x η = y ))

Chúng ta còn có tiền ñề sau, nó khẳng ñịnh rằng micro-steps là rời rạc.
AXM
L 22

⌢
⌢
l = 0 ⇒□( Pti ∨ (Unit true) ∧ (true Unit ))
⌢
(0 ≤ x ∧ 0 ≤ y )⇒((η = x + y )⇔ (η = x η = y ))

Cuối cùng, những luật qui nạp của DC là có cơ sở (ñúng):
H (⌈⌉)

⌢
⌢
H ( X ) ⊢ H ( X ∨ X ⌈ P ⌉∨ X ⌈¬P ⌉)
H (true)

Chúng ta cũng có pha (phase) sau dựa trên luật qui nạp.


10
H (η = 0)

⌢

P ≙ ⌈P⌉0 ⌈P⌉ ⌈P⌉0
P⌉+ ≙

P⌉∨⌈P⌉0

P⌉− ≙

P⌉∨⌈⌉

P
P

+

≙

P ∨⌈P⌉0

+

≙

P ∨⌈⌉

Phép chiếu (projection) Những ngữ nghĩa hình thức của một chương trình là một
công thức WDC*. Tuy nhiên công thức khoảng trong một bộ ba (Hoare) là một công
thức DC*. Vì vậy chúng ta liên hệ hai loại logic này với nhau. Ta ñịnh nghĩa một hàm
*
*
Π : WDC * → DC * , gọi là phép chiếu, cho tương ứng mỗi WDC formula D với một DC

Cho P là một tiến trình, pre và post là vị từ (khẳng ñịnh) trên các biến chương trình.
Một công thức trong Hoare logic có dạng { pre}P{ post} , ñược gọi là bộ ba Hoare, với ý
nghĩa rằng nếu ñiều kiện trước pre ñược giữ trong trọng thái ban ñầu và P kết thúc, thì
ñiều kiện sau post ñược giữ trong trạng thái kết thúc. Bộ ba này ñược gọi là công thức
tính ñúng bộ phận (partial correctness formula) khi mà nó không ñảm bảo việc kết
thúc của chương trình P. Hoare logic với tính ñúng tổng thể (total correctness) ñảm
bảo tính dừng của chương trình. Logic này cung cấp một hệ thống chứng minh ñầy ñủ
cho việc lí giải về hành vi chức năng của những chương trình tuần tự [16, 15]. Rất
nhiều lí thuyết liên quan tới tính dừng của chương trình ñã ñược nghiên cứu. Những
chương trình không dừng không thể lí giải ñược, và thông thường ñược coi là không
xác ñịnh (undefined). Một số mở rộng của logic Hoare tới những ngôn ngữ lập trình
song song chia sẻ biến ñã ñược ñề xuất [18,17]. Tuy nhiên ta sẽ xem xét giới hạn sau
trên việc truy cập vào những biến chia sẻ. Bất kỳ biến chia sẻ nào cũng có thể ñược
ñọc bởi bất kỳ tiến trình. Một số biến chia sẻ có thể ñược ghi bởi bất kỳ tiến trình nào.
Một số khác có thể chỉ ñược ghi bởi một tiến trình và chỉ ñọc bởi một tiến trình khác.
Ta mở rộng logic Hoare ra lập trình song song thời gian thực với biến chia sẻ ñể lí giải
về tính dừng cũng như không dừng của những chương trình thời gian thực. Không
giống với những chương trình máy tính thông thường, những chương trình ñiều khiển
thời gian thực nói chung sẽ thực thi mãi mãi. Vì vậy không dừng là thuộc tính quan
trọng ñể lí giải cho những loại chương trình như vậy. Sự mở rộng bộ ba Hoare của
chúng ta có hai dạng. Dạng thứ nhất là { pre}[ P, ϕ]{ post} tức là nếu tiền ñiều kiện pre
ñúng trong trạng thái ban ñầu và P kết thúc, thì hậu ñiều kiện post ñúng trong trạng
thái cuối và trong khoảng thời gian thực thi chương trình công thức Duration ϕ luôn
ñược thỏa mãn. Dạng thứ hai là { pre}[ P, ϕ ]{} , tức là nếu tiền ñiều kiện pre ñúng trong
trạng thái ban ñầu và P không dừng, thì bất kỳ khoảng thời gian trước của một khoảng
thời gian không giới hạn của chương trình ñều thỏa mãn công thức duration ϕ. Cặp bộ
ba này ñược sử dụng ñể lí giải về các thuộc tính của những chương trình thời gian
thực. Vì vậy, {true}[ P, true]{ false} diễn tả rằng P không kết thúc, và {true}[ P, false]{}
nói lên rằng P không có hành vi không kết thúc. Chú ý rằng có thể nhận dạng theo cú
pháp rằng một bộ ba ñang diễn tả những thuộc tính của những hành vi giới hạn hay


delay e → S 0 | while g do P od

S ::= P1 || P2 || ... || Pn , ( n ≥ 1)

Ta giả sử giả thuyết về ñồng bộ lí tưởng là ñúng, nghĩa là, tính toán và kết nối không
mất thời gian, chỉ sự việc chờ ñồng bộ bên ngoài hoặc những câu lệnh trễ là tốn thời
gian. Ý nghĩ không hình thức của ngôn ngữ lập trình ñược mô tả như sau:
• Skip: một tiến trình trong ñó không hành ñộng nào ñược thực thi và kết thúc
ngay lập tức, vì vậy giá trị của tất cả các biến ñược giữ nguyên.
•

x := e : câu lệnh gán thay ñổi giá trị của biến x tới giá tương ứng của biểu

thức e.
• delay d: ñưa tiến trình vào trạng thái ngủ trong d ñơn vị thời gian. Trong
khoảng thời gian này, tiến trình không thể làm gì.
•

c ? x, c !e : tiến trình vào dữ liệu c ? x gán dữ liệu vào từ kênh c cho biến x,

tương tự như vậy, tiến trình xuất dữ liệu c !e tính toán giá trị biểu thức e và
gửi thông qua kênh c. Nhưng trước khi kết nối có thể xẩy ra thì cả kênh
nhập và xuất phải sẵn sàng ñể kết nối, do ñó trong trường hợp cần thiết các


14
kênh nhập hoặc xuất phải chờ
ñích ñã sẵn sàng.
•

gian thực, ẩn ñi bớt chi tiết về ngữ nghĩa.

2.3 Ng nghĩa hình th c c a ngôn ng l p trình
Ở ñây ta ñưa ra những ngữ nghĩa hình thức ñể lập trình những bước xây dựng công
thức trong WDC*. ðể ñơn giản, ta sử dụng x\ch cho dãy thu ñược từ việc gỡ bỏ tất cả
các kết nối trên kênh ch từ dãy x, x↓CH ≙ x\CHAN\CH phép chiếu vết (trace) trên kênh
CH, và x≤y dãy x là tiền tố của dãy y.
Cho một hệ thống thời gian thực, giờ ta ñã sẵn sàng ñể diễn tả việc giám sát theo thời
gian bằng bộ:
(s,v,v’,tr)

(1)

trong ñó
• s : Time → Rn là một hàm số thực của thời gian, ñược sử dụng ñể mô tả trạng
.

thái vật lý của hệ thống. Ta sử dụng s ñể kí hiệu cho ñạo hàm của s.


15
• tr : Time → chan*, kí hiệu cho việc

ghi vết (trace), xác ñịnh những sự

kiện kết nối một hệ thống gặp phải trên khoảng thời gian dọc theo kênh trong
chan(P). Ở ñây, chan(P) ñược ñịnh nghĩa là tên của các kênh trong tiến trình P.
Nó phải thỏa mãn những luật sau:
1.


Những ngữ nghĩa của ngôn ngữ ñược ñưa ra bởi những ñịnh nghĩa tiếp theo. Ta ñịnh
nghĩa thêm Idle, ñể biểu thị một khoảng không phải ñiểm nơi mà không có sự kiện nào
ñang xẩy ra hoặc ñược mong ñợi xẩy ra theo tiến trình thời gian, nghĩa là tất cả các
kênh và trạng thái/giá trị của các biến ñược giữ nguyên
Idle p ≙ v ' = v ∧ tr = tr ∧ η = 0

(4)

ðể ñơn giản ta viết Idle ñối với Idlep, nhưng nó sẽ ñược ghi thêm p bên dưới khi cần
làm rõ. Ngữ nghĩa của chương trình thời gian thực trong WDC* ñược liệt kê bên dưới:


16

( D1)

M( x := e) ≙ Unit ⌈ x ' = e⌉0 ∧ v ' = x v ∧ l = 0 ∧ tr = tr
M '( x := e) ≙ false

( D 2)

M(skip ) ≙ Pti ∧ tr = tr ∧ v ' = v
M '(skip) ≙ false

( D3)

M(delay d ) ≙ Idle

+


M(

b ; ci ? xi → Si

n
i =1 i

≙ (⌈∨in=1 bi ⌉0

M '(

b ; ci ? xi → Si

n
i =1 i

≙ (⌈∨in=1 bi ⌉0

( D8)

( D9)

delay d → S0 )

M(ci ? xi ) ∧ l ≤ d ) M( Si ) ∨ l = d

M( S0 )

delay d → S0 )


mi ≤ b < m



17
nghĩa là nếu chúng ta chiếu trM( P ||P ||...|| P )
1

2

n

trong khoảng [0,b], lưu vết của những tiến

trình tổ hợp, lên các kênh của chan(Pi) (1 ≤ i ≤ n) thì ta thu ñược vết của Pi khi b nhỏ
hơn thời gian kết thúc của Pi, ngược lại thu ñược tập rỗng.

2.4 Các lu t ki m ch ng
Những luật cho các câu lệnh nguyên tử và các câu lệnh kết hợp ñược liệt kê dưới ñây.
Luật 1 nói rằng việc thực thi của câu lệnh skip không thay ñổi trạng thái cũng như
không tốn thời gian.
Luật 1 (Skip)
{ post}[skip, ]{ post}

Luật 2 nói rằng việc thực thi của câu lệnh gán có thể thay ñổi trạng thái nhưng không
tốn thời gian. Một công thức duration không thể thể hiện sự thay ñổi ngay lập tức của
biến chương trình.
Luật 2 (Assignment)
{ post[ x / e]}[ x := e, ]{ post}


{ post[ x / e]}[c ? x, await (c !) ∧ post[ x / e] * ]{ post}

(b)

{ pre}[c ? x, ¬c !∧ pre * ]{}

giả sử COND1, COND2 ñúng

Luật 6 cho phép làm mạnh hơn tiền ñiều kiện, và làm yếu ñi hậu ñiều kiện hoặc yếu ñi
biểu thức duration trong một bộ ba.
Luật 6 (Consequence)
(a)
(b)

pre '⇒ pre
post ⇒ post ' ϕ⇒φ
{ pre '}[ P, φ]{ post '}
{ pre}[ P, ϕ ]{} pre '⇒ pre
ϕ⇒φ
{ pre '}[ P, φ ]{}

{ pre}[ P, ϕ ]{ post}

Luật 7 diễn tả kết hợp tuần tự của những chương trình. Nó nhấn mạnh tính tương tự
giữa kết hợp tuần tự của chương trình và toán tử chop của công thức duration. Tiếp
theo ñó hệ thống chứng minh cũng có thể ñược sử dụng ñể lí giải về hành vi của những
chương trình không xác ñịnh thời gian.Vì vậy mở rộng bộ ba Hoare của chúng ta là
ñược bảo tồn (conservative). Luật 7-a nói rằng một dãy P; Q kết thúc nếu cả P và Q
kết thúc. Luật 7-b, 7-c, và 7-d nói rằng một dãy P; Q không kết thúc thành công khi P
hoặc Q không kết thúc thành công.


{ pre ∧ ∨in=1 bi }[delay e; S0 , l = d ϕ]{q}
{ pre ∧ ∨in=1 bi }[CondE , l ≤ e α ∨ l = e ϕ]{∨in=1 qi ∨ q}
{ pre ∧ bi }[c ? x, await (c !) ∧l ≤ e]{ pi [v / x]}, i = 1...n
{ pi }[ Si , α ]{}, i = 1...n

(b)

{ pre ∧ ∨in=1 bi }[delay e; S0 , l = d ϕ]{}
{ pre ∧ ∨in=1 bi }[CondE , l ≤ e α ∨ l = e ϕ]{}

trong ñó CondE = in=1 bi ; ci ? xi → Si delay d → S0

Trong luật 9, inv biệu thị cho sự bất biến của vòng lặp, nghĩa là một vị từ ñúng vào
thời ñiểm ñầu và cuối của mỗi vòng lặp. Luật 9-a thể hiện những vòng lặp có kết thúc,
các trường hợp khác là không kết thúc. Với những vòng lặp không dừng chúng yêu
cầu rằng việc thực thi phần thân của vòng lặp chiến khoảng thời gian không ñổi c ñể
tránh hiện tượng divergence và Zeno.
Luật 9 (Iteration) trong tiến trình Pi
( a)

{inv ∧ g}[ P, ϕ]{inv}
{inv}[while g do P od,ϕ* ]{inv ∧ ¬g}

(c )

{inv ∧ g}[ P, α ]{}
{inv}[while g do P od,α ]{}

( a)

Luật 10 (Parallel)
{ prei }[ Pi , ϕi ]{ posti },1 ≤ i ≤ n
(a)

Idle ) ∧ l = m) → ϕ
∧1≤i≤n ((ϕi
{∧1≤i≤n prei }[ P1 || P2 || ... || Pn , ϕ]{∧1≤i≤n posti }

với giả sử COND0 thỏa mãn.
{ prei }[ Pi , ϕi ]{},

1≤ i ≤ n

{ prei }[ Pi , ϕi ]{ posti }, k + 1 ≤ i ≤ n
(b)

∧1≤i≤n ((ϕi
Idle ) ∧ l = m) → ϕ
{∧1≤i≤n prei }[ P1 || P2 || ... || Pn , ϕ ]{}

với giả sử COND1, COND2 thỏa mãn.
Ví dụ Ta xét chương trình sau
P ≙ x := z + 1; x := x − 3; delay 2 || y := y * z; delay 1; y := y + 2; delay 1

Thì bộ ba sau là ñúng:
⌢
{z ≥ 0 ∧ y = 0}[ P, x ≥ −2 ∧(l = 1 ∧ y = 0 ) (l = 1 ∧ y = 2 )]{x ≥ −2 ∧ y = 2}

Vì vậy sẽ có những khả năng giao nhau của P là:



Việc chứng minh các luật này ñược trình bày, về cơ bản là dựa trên ñịnh nghĩa:
ðịnh nghĩa: cho P là chương trình, pre,post là các vị từ, ϕ là công thức duration
(1) Bộ ba { pre}[ P, ϕ]{ post} là ñúng khi và chỉ khi
- ⌈ pre ⌉0

M( P) ⇒WDC* M( P) ⌈ post ⌉0

- ∏ (⌈ pre⌉0 M( P )) ⇒ DC ϕ
*

(2) Bộ ba { pre}[ P, ϕ ]{} là ñúng khi và chỉ khi
∏ (⌈ pre⌉0

M '( P)) ⇒ DC* ϕ


22

Chương 3 - Kỹ thuật thiết kế hệ thống ñiều khiển thời gian
thực
Trong phần trước, chúng ta vừa trình bày một kỹ thuật ñể thu ñược một chương trình
thời gian thực từ một yêu cầu thời gian thực viết trong DC*. Giờ, chúng ta sẽ kết hợp
kỹ thuật này với những kỹ thuật ñược trình bày trong [13] ñể phát triển một phương
pháp ñầy ñủ các bước xây dựng hệ thống thời gian thực.
Một hệ thống ñiều khiển thời gian thực là một hệ thống lai phân tán bao gồm thành
phần liên tục và thành phần rời rạc trong sự tương tác. Một mô hình của những hệ
thống ñiều khiển thời gian thực ñược mô tả trên hình 1.
Sensors