Sinh dữ liệu thử cho ứng dụng Lustre/SCADE sử dụng điều kiện kích hoạt

Kỷ yếu Hội nghị Quốc gia lần thứ VIII về Nghiên cứu cơ bản và ứng dụng Công nghệ thông tin (FAIR); Hà Nội, ngày 9-10/7/2015 
DOI: 10.15625/vap.2015.000202 
SINH DỮ LIỆU THỬ CHO ỨNG DỤNG LUSTRE/SCADE SỬ DỤNG 
ĐIỀU KIỆN KÍCH HOẠT 
Trịnh Công Duy1, Nguyễn Thanh Bình1, Ioannis Parissis2 
1
 Trường Đại học Bách Khoa, Đại học Đà Nẵng, Đà Nẵng, Việt Nam 
2
 Viện Đại học Bách khoa Grenoble, Cộng hòa Pháp. 
tcduy@dut.udn.vn, ntbinh@dut.udn.vn, ioannis.parissis@grenoble-inp.fr 
TÓM TẮT - Kiểm thử là một trong những hoạt động quan trọng trong tiến trình phát triển phần mềm. Phần mềm phát triển 
ngày càng phức tạp, yêu cầu chất lượng ngày càng cao hơn, vai trò kiểm thử càng quan trọng hơn, đặc biệt là trong phát triển phần 
mềm cho các hệ thống phản ứng. Hệ thống phản ứng được phát triển phổ biến trong các lĩnh vực như hàng không, năng lượng, hạt 
nhân Những hệ thống này thường yêu cầu rất cao về chất lượng và đòi hỏi các hoạt động kiểm thử nghiêm ngặt trước khi chúng 
được triển khai sử dụng. Lustre/SCADE là ngôn ngữ được sử dụng rộng rãi để phát triển phần mềm cho các hệ thống phản ứng, một 
lĩnh vực mà chất lượng phần mềm được yêu cầu hết sức nghiêm ngặt, gần như là không được phép xảy ra bất cứ một lỗi nhỏ nào. 
Điều này đòi hỏi việc kiểm thử phải được tiến hành thường xuyên và liên tục khi có bất cứ sự thay đổi nào trên ứng dụng. Bên cạnh 
đó, đối với những ứng dụng trong lĩnh vực này, việc kiểm thử thủ công sẽ rất khó thực hiện và không mang lại hiệu quả, do đó yêu 
cầu cần phải tự động hóa hoạt động kiểm thử cho các ứng dụng Lustre/SCADE. Trong bài báo này, chúng tôi tập trung nghiên cứu 
việc kiểm thử tự động cho các ứng dụng Lustre/SCADE. Chúng tôi đề xuất kỹ thuật sử dụng các điều kiện kích hoạt trên mạng lưới 
toán tử (operator network) để sinh ra các dữ liệu thử một cách tự động. Trong đó, kỹ thuật kiểm chứng mô hình (model checking) 
được sử dụng trong việc sinh tự động các dữ liệu thử này. Cuối cùng, chúng tôi thử nghiệm giải pháp này trên một chương trình 
Lustre/SCADE trong hệ thống điều khiển nhiệt độ môi trường. 
Từ khóa - Hệ thống phản ứng; Kiểm chứng mô hình; Kiểm thử; Thuộc tính bẫy; Lustre/SCADE; Sinh dữ liệu thử. 
I. GIỚI THIỆU 
Việc phát hiện và khắc phục lỗi cho các phần mềm là một công việc đòi hỏi nhiều nỗ lực và chi phí trong phát 
triển phần mềm. Hiện nay, phần mềm đang được ứng dụng ngày càng rộng rãi trong nhiều lĩnh vực, do đó chất lượng 
phần mềm ngày càng được quan tâm. Trong công nghệ phần mềm, kiểm thử là hoạt động cơ bản nhằm phát hiện các 
lỗi của phần mềm. Trong đó, kiểm thử tự động nhằm xử lý một cách tự động quy trình kiểm thử, sinh ca kiểm thử, thực 
thi kiểm thử và đánh giá kết quả kiểm thử. 
Hệ thống phản ứng (reactive system) khi hoạt động đáp ứng (phản ứng) với các sự kiện bên ngoài [3]. Chẳng 
hạn, các hệ thống sinh học là những hệ thống phản ứng, bởi vì nó phản ứng với các sự kiện nhất định. Tuy nhiên, trong 
tin học và điều khiển, thuật ngữ này được sử dụng chủ yếu để mô tả các hệ thống nhân tạo. Hệ thống phản ứng liên tục 
tương tác với môi trường và thực thi theo yếu tố tác động bởi môi trường. Ở một khía cạnh trừu tượng thì nó được xem 
là một hộp đen, ta cung cấp các giá trị đầu vào thì hệ thống sẽ cho ra các giá trị đầu ra thích hợp. Các hệ thống phản 
ứng có thể được xem là đang ở một trạng thái nhất định và đợi thông tin đầu vào (input). Với mỗi đầu vào, chúng thực 
hiện tính toán và sinh đầu ra (output) và chuyển sang một trạng thái mới. Thông thường, các hệ thống nhúng và các hệ 
thống điều khiển cũng là các hệ thống phản ứng [2]. 
Lập trình đồng bộ (synchronous programming) [3] đã được giới thiệu vào cuối những năm 80 như là một 
phương pháp tiếp cận để thiết kế các hệ thống phản ứng. Kể từ đó, nó đã được sử dụng rộng rãi, chủ yếu trong lĩnh vực 
yêu cầu độ an toàn cao như hệ thống điện tử, vận tải, sản xuất năng lượng (các hệ thống phản ứng). Một lợi thế quan 
trọng của cách tiếp cận đồng bộ này là nhằm cung cấp một khuôn khổ chính thức, hiệu quả và đồng nhất cho các hoạt 
động phát triển - thiết kế, cài đặt và xác minh. Một số ngôn ngữ lập trình, đặc biệt đối với các ngôn ngữ sử dụng 
phương pháp tiếp cận đồng bộ như Esterel, Signal hoặc Lustre [4]. SCADE (Safety Critical Application Development 
Environment) là những công cụ thương mại dựa trên các mô hình đồng bộ và ngôn ngữ lập trình Lustre. SCADE đã 
được sử dụng trong các dự án quan trọng tại châu Âu (Airbus A340-600, A380, Eurocopter) và trở thành một tiêu 
chuẩn trong lĩnh vực này. 
Lustre [4] là một ngôn ngữ đồng bộ luồng dữ liệu, được thiết kế năm 1984 bởi Viện IMAG tại Grenoble. 
Chương trình Lustre gồm một chuỗi có thứ tự các phương trình giúp xác định phương thức dòng đầu vào được chuyển 
thành các dòng đầu ra thông qua một tập hợp các toán tử. Do đó, cách biểu diễn phù hợp nhất cho các chương trình 
Lustre là một đồ thị có hướng, gọi là mạng lưới toán tử (trong thực tế, người sử dụng không viết chương trình Lustre 
mà sử dụng trình soạn thảo đồ họa trong công cụ SCADE để xây dựng các mạng lưới toán tử liên quan). Việc kết hợp 
của cả hai mô hình đồng bộ và dòng dữ liệu, cú pháp đồ họa đơn giản, áp dụng khái niệm thời gian rời rạc là một số 
trong những đặc điểm chính làm cho Lustre trở thành ngôn ngữ lý tưởng cho việc xây dựng các mô hình, các thiết kế 
hệ thống điều khiển trong một số lĩnh vực công nghiệp, chẳng hạn như hệ thống điện tử, ô tô và năng lượng, hạt nhân 
nói riêng và hệ thống phản ứng nói chung. Với các hệ thống này, yếu tố an toàn (safety) được quan tâm hàng đầu. Vì 
vậy việc hệ thống bị lỗi khi đang vận hành sẽ gây hậu quả rất nghiêm trọng. Hơn nữa, “lỗi hệ thống” có xu hướng được 
phát hiện muộn trong quá trình phát triển khi mà nó đã gây ra thiệt hại đáng kể, rất khó để gỡ lỗi và tốn nhiều chi phí. 
Trong tiến trình phát triển phần mềm cho các hệ thống phản ứng, giai đoạn kiểm thử đóng vai trò rất quan trọng. Phần 
Tm
t
đ
d
ứ
c
c
R
p
x
th
k
th
tr
T
c
k
d
th
g
p
c
d
h
L
c
c
A
1
v
v
n
p
đ
v
rịnh Công Duy, N
ềm càng lớn
ốt, ngăn ngừa
Bắt đầu
ó đến nay, nh
Nhóm t
ụng trên ngôn
ng trên Lustr
hí bao phủ. N
ông cụ LESA
inus Plasmeij
hản ứng. Tiếp
ây dựng tập c
ử cho các ứn
Nhìn ch
iểm thử, kiểm
ấy chưa có n
ong việc kiểm
Trong b
rong đó, sử d
hứng mô hình
iểm chứng m
ữ liệu thử dựa
Nội dun
ống phản ứn
iới. Mục II tr
háp sử dụng 
ụ kiểm chứng
ụng giải pháp
ướng phát tri
Trong m
ustre và môi 
ác điều kiện 
hứng mô hình
. Tổng quan
. Ngôn ngữ l
Hệ thốn
ới các tác độn
ới các tác độ
ày không thể
hải tôn trọng 
ược xem là m
ào trước đó v
guyễn Thanh B
 và càng phức
 các khiếm kh
 từ đầu những
iều công trình
ác giả Laya M
 ngữ Lustre [
e, tuy nhiên n
ăm 1999, nh
R để kiểm ch
er đến từ Đạ
 đến, nhóm t
a kiểm thử c
g dụng dựa tr
ung các nghi
 thử tự động
hiều nghiên 
 thử các chư
ài báo này, c
ụng các điều
 để sinh tự đ
ô hình LESA
 trên các kết 
g của bài bá
g, ngôn ngữ l
ình bày các cơ
điều kiện kích
 mô hình LE
 này cho một
ển tiếp theo. 
ục này chún
trường SCAD
kích hoạt cho
 trong sinh dữ
 về Lustre/SC
ập trình Lustr
g phản ứng l
g từ bên ngo
ng bên ngoài.
 đồng bộ hóa
nghiêm ngặt 
ột chuỗi vô h
à hiện tại. 
ình, Ioannis Paris
 tạp, thủ tục k
uyết trước kh
 năm 90, lĩnh
 nghiên cứu đ
adani ở Đại
10]. Nhóm ng
ghiên cứu này
óm tác giả N
ứng mô hình 
i học Nijmege
ác giả Elizabe
ần thực hiện 
ên mô hình U
ên cứu đến th
 các hệ thống
cứu thực hiện
ơng trình Lus
húng tôi đề x
 kiện kích ho
ộng các dữ l
R để tiến hàn
quả sinh ra từ
o được tổ chứ
ập trình Lustr
 sở lý thuyết 
 hoạt trên mạ
SAR để tạo d
 hệ thống cụ t
g tôi trình bày
E. Đồng thời
 một chương 
 liệu thử. 
ADE 
e trong các h
à một hệ thốn
ài nó. Hệ thốn
 Hệ thống ph
 một cách hợp
ràng buộc về 
ạn các véc tơ
sis 
iểm thử đòi h
i thực hiện ki
 vực nghiên c
ã và đang đư
 học Grenobl
hiên cứu này
 sử dụng phư
icolas Halbw
các hệ thống 
n mở rộng cô
ta Fourneret 
ở phiên bản m
ML. 
ời điểm hiện
 phản ứng v
 hướng tiếp c
tre/SCADE. 
uất kỹ thuật 
ạt trên mạng
iệu thử dựa t
h kiểm chứng
 quá trình kiể
c như sau: M
e và các nghiê
nền tảng sử d
ng lưới toán 
ữ liệu thử ch
hể và các kết
II. CƠ
 cơ sở lý thuy
 chúng tôi cũn
trình Lustre/S
ệ thống phản 
g thay đổi hàn
g này có thể 
ản ứng liên tụ
 lý với hệ th
thời gian thực
 đầu vào và đ
Hình 1. Mô 
ỏi tốn nhiều 
ểm thử ở mức
ứu về kiểm th
ợc thực hiện.
e thực hiện ki
 đã xây dựng 
ơng thức xác
achs và Pasc
phản ứng [9]
ng cụ kiểm th
[13] ở đại họ
ới, trong ngh
tại tập trung 
à chương trìn
ận sử dụng c
sinh dữ liệu t
 lưới toán tử 
rên các điều k
 mô hình cho
m chứng này.
ục I giới thi
n cứu về kiểm
ụng trong ngh
tử của một ch
o các chương
quả của việc 
 SỞ LÝ TH
ết của nghiên
g trình bày k
CADE. Và c
ứng 
h động của n
tự định hướng
c phản ứng l
ống. Nói cách
 cần đáp ứng
ầu ra. Ở mỗi b
hình hệ thống p
thời gian và c
 chi tiết hơn, 
ử cho các hệ
ểm thử tự độn
công cụ Lute
 định ngẫu nh
al Raymond đ
[12]. Năm 20
ử tự động GA
c Franche-Co
iên cứu này 
vào nghiên cứ
h Lustre/SCA
ác điều kiện 
hử tự động c
của chương t
iện kích hoạ
 một chương 
ệu chung về b
 thử cho các
iên cứu này. 
ương trình L
 trình Lustre/
thử nghiệm. C
UYẾT 
 cứu, bao gồm
ỹ thuật xây dự
uối cùng sẽ l
ó với đầu ra, 
 hoặc được đ
ại với các tác
 khác, môi tr
kịp thời [12].
ước thì giá tr
hản ứng 
ông sức. Việ
phức tạp hơn 
 thống phản ứ
g cho các ứn
s[11] để kiểm
iên các ca kiể
ến từ Đại họ
04, nhóm tác
ST để có th
mté đã thực h
tác giả đề xuấ
u các kỹ thu
DE. Tuy nhi
kích hoạt trên
ho các chươn
rình Lustre, đ
t này. Chúng 
trình Lustre c
ài báo và trì
 chương trình
Trong mục II
ustre, kết hợp
SACDE. Phầ
uối cùng là p
 các nội dun
ng mạng lướ
à những nội d
điều kiện và t
iều khiển định
 động từ môi
ường không 
 Việc thực th
ị đầu ra được
c tìm lỗi càng
và chi phí cao
ng được hình
g dụng phản 
 thử các ứng 
m thử dựa tr
c Grenoble đ
 giả Pieter Ko
ể kiểm thử cá
iện sinh ca k
t kỹ thuật sin
ật kiểm chứng
ên, theo chún
 mạng lưới c
g trình Lustr
ồng thời sử 
tôi sẽ sử dụn
ụ thể, từ đó 
nh bày tổng q
 Lustre/SACD
I, chúng tôi đ
 với việc sử 
n IV trình bà
hần kết luận 
g về ngôn ng
i toán tử, các 
ung về ứng 
rạng thái nhằ
 hướng để ph
 trường, khi m
thể chờ đợi v
i của hệ thống
 xác định bởi 
629 
 sớm càng 
 hơn [1]. 
 thành. Từ 
ứng và áp 
dụng phản 
ên các tiêu 
ã sử dụng 
opman và 
c hệ thống 
iểm thử và 
h ca kiểm 
 mô hình, 
g tôi nhận 
ác toán tử 
e/SCADE. 
dụng kiểm 
g công cụ 
sinh ra các 
uan về hệ 
E trên thế 
ề xuất giải 
dụng công 
y việc ứng 
và đề xuất 
ữ lập trình 
lộ trình và 
dụng kiểm 
m đáp ứng 
ản ứng lại 
ôi trường 
à hệ thống 
 phản ứng 
giá trị đầu 
6đ
h
tr
tr
lĩ
h
tr
v
tr
n
p
n
ứ
x
c
k
đ
đ
d
d
s
d
tr
g
k
n
30 
Hình 1 
ầu ra và chuy
ệ thống phản 
ong các lĩnh 
Lustre 
ình điều khiể
nh vực năng 
ệ thống thời g
ình, ngôn ngữ
Một chư
à cũng chính 
ong chương t
ode khác. Mộ
hương trình, 
ever, đoạn ch
Lustre 
ng với một ch
- Toán 
- Toán 
- Toán 
Các kiể
- Kiểu 
or, =>, kiểu n
- Kiểu 
ác phép so sá
Bên cạn
hởi tạo và toá
ược sử dụng đ
- Toán 
ồng hồ trước 
ụng như là th
- Toán 
òng dữ liệu m
ử dụng để tạo
ụng cùng với
ước các biểu 
- Toán 
ọi là bộ lọc. 
hi F là đúng. 
 Đặc bi
hững ngôn ng
minh họa mô
ển sang một 
ứng. Các hệ t
vực như hàng
[4] là một ngô
n trong các h
lượng, hạt nh
ian thực. Kh
 Lustre mô tả
ơng trình Lu
là hàm đầu và
rình là không
t node xác đị
trong node có
ương trình nà
được dựa trên
uỗi các tuần 
tử logic: and,
tử số học: +, 
tử so sánh: 
u dữ liệu cơ b
luận lý (boole
ày thường đư
số nguyên, số
nh: , <, <=,
h các toán tử
n tử điều kiệ
ể tạo ra các t
tử ưu tiên (pr
đó. Các toán 
am số của toá
tử khởi tạo (i
ột giá trị khở
 ra một chuỗ
 các toán tử p
hiện Z = X →
tử điều kiện w
Ví dụ ta có ch
Khi F là sai th
ệt, ngôn ngữ 
ữ lập trình kh
SIN
 hình của mộ
trạng thái mớ
hống phản ứn
 không, năng 
n ngữ hướng 
ệ thống phản
ân... Ngôn ng
ác với ngôn n
 cách mà các
stre gồm các 
o của nó. Mỗ
 quan trọng [4
nh luồng đầu
 thể chứa các
y khai báo mộ
 khái niệm v
tự các đồng h
 or, not, xor, 
-, *, /, div, mo
, , >=
ản của ngôn n
an): Gồm 2 g
ợc dùng trong
 thực (int, rea
 >, >=. 
 trên, ngôn ng
n. Các toán t
oán tử mới v
ecedence) đư
tử sẽ nhận giá
n tử pre(), pr
nitialization) 
i tạo ban đầu
i mới Z = X →
re() vì giá trị
 pre(Y) sẽ có
hen: Toán tử
uỗi E và F và
ì chuỗi G sẽ 
Lustre không 
ác [4]. 
H DỮ LIỆU THỬ
t hệ thống ph
i. Thông thườ
g thường đượ
lượng, hạt nh
dữ liệu đồng 
 ứng như: cá
ữ Lustre rất t
gữ mệnh lệnh
 đầu vào được
nốt (node). M
i biến có thể
]. Một khi m
 ra như các ch
 biến cục bộ. 
t node never
Hình 2. Ví d
ề các luồng (f
ồ. Ngôn ngữ 
=> 
d 
gữ Lustre: 
iá trị true, fa
 lập trình các
l): Các kiểu n
ữ Lustre có c
ử thời gian nà
à phức tạp hơ
ợc ký hiệu là 
 trị nil ở chu k
e(X) cho kết q
được ký hiệu
. Ví dụ, các c
Y, chuỗi kết
 chuỗi đầu tiê
 chuỗi giá trị 
 when được
 G = E when
không có giá 
cung cấp các
 CHO ỨNG DỤ
ản ứng. Với 
ng, các hệ th
c áp dụng chủ
ân, hệ thống l
bộ, được xây 
c hệ thống điề
hích hợp tron
 (imperative l
 chuyển thàn
ột node là mộ
được định ngh
ột node được
ức năng của l
Hình 2 là ví d
với đầu vào l
ụ một đoạn chư
lows) và đồng
Lustre gồm c
lse. Kiểu này
 cấu trúc điều
ày được sử dụ
ác toán tử thờ
y có hoạt độ
n. 
pre(): Các toá
ỳ đồng hồ đầ
uả chuỗi tuần
 là → hoặc f
huỗi X(x1, x2
 quả sẽ là Z(x
n trong pre()
 Z= ( x1, y2, y
sử dụng để th
 F, sẽ tạo ra c
trị gì cả. 
 toán tử lặp (w
NG LUSTRE/SC
mỗi đầu vào, 
ống nhúng và
 yếu để xây d
iên quan đến 
dựng dành riê
u khiển tự độ
g việc lập trìn
anguages), m
h kết quả đầu 
t tập hợp các
ĩa chỉ một lần
 định nghĩa, n
uồng đầu vào
ụ một chươn
à E và đầu ra
ơng trình Lustr
 hồ (clocks).
ác toán tử cơ b
 được sử dụn
 khiển. 
ng cùng với 
i gian (tempo
ng đặc biệt tr
n tử pre() gh
u tiên. Nếu ch
 tử sẽ là (nil, 
by: Các toán 
, x3,x4,x5,x6
1, x2, x3,x4,x
 là không xác
3,y4,y5,y6 ...)
ay đổi tần su
huỗi mới G s
hile, do whi
ADE SỬ DỤNG
hệ thống thự
 các hệ thống
ựng các hệ th
giao diện ngư
ng cho việc l
ng, các hệ th
h các thành p
ô tả dòng điều
ra. 
 phương trình
 trong một n
ó có thể đượ
, thông qua m
g trình Lustre
là S. 
e 
 Luồng là mộ
ản sau: 
g với các toá
các phép toán
ral operator): 
ên luồng dữ l
i nhớ giá trị c
uỗi X(x1, x2,
x1, x2, x3, x4
tử → được sử
 ...) và Y(y1, y
5,x6 ...). Toá
 định. Sử dụn
. 
ất đồng hồ. T
ẽ có giá trị tư
le, for) hay th
 ĐIỀU KIỆN K
c hiện tính to
 điều khiển c
ống điều khi
ời – máy 
ập trình nên c
ống giám sát
hần quan trọ
 khiển của m
 xác định kết 
ode và thứ tự 
c sử dụng bên
ột tập hợp có
 để thực hiện
t chuỗi các gi
 ... định tự động các điều kiện kích hoạt tương ứng. 
- Tiến hành kiểm chứng mô hình chương trình Lustre ban đầu với các thuộc tính đầu vào là các thuộc tính bẫy 
được tạo ra trên cơ sở phủ định các điều kiện kích hoạt được sinh ra từ bước 2. 
Việc xác định các lộ trình và các điều kiện kích hoạt tương ứng đóng vai trò quan trọng trong việc định nghĩa ra 
các thuộc tính bẫy cho quá trình kiểm chứng mô hình. Mục tiêu của quá trình kiểm chứng mô hình không phải để kiểm 
tra mô hình của hệ thống được thiết kế đúng hay không, mà ở đây mục đích chính của chúng ta là sinh ra các phản ví 
dụ, các phản ví dụ này chính là dữ liệu thử cần được tạo ra. 
B. Sinh dữ liệu thử tự động với công cụ kiểm chứng mô hình LESAR 
Để thực hiện việc sinh ra dữ liệu thử sau khi có điều kiện kích hoạt và các phản ví dụ tương ứng, chúng tôi sử 
dụng công cụ kiểm chứng mô hình LESAR cho các chương trình Lustre. Tuy nhiên, mục đích của chúng ta là cần sinh 
ra các phản ví dụ, do đó các thuộc tính đầu vào phải là các thuộc tính bẫy dựa trên các điều kiện kích hoạt, thuộc tính 
bẫy nAC được xác định theo công thức: 
 nAC=not (AC) 
Hình 9 minh họa quy trình sử dụng công cụ LESAR để sinh ra dữ liệu thử dựa trên mã nguồn chương trình 
Lustre và các điều kiện kích hoạt. 
Hình 9. Sử dụng LESAR tạo các dữ liệu thử 
Việc sinh dữ liệu thử sử dụng kỹ thuật kiểm chứng mô hình bằng công cụ LESAR dựa trên các điều kiện kích 
hoạt được thực hiện trình tự qua các bước chi tiết như sau: 
Bước 1 - Xác định các điều kiện kích hoạt: Từ chương trình Lustre chúng ta xác định các điều kiện kích hoạt 
tương ứng với các lộ trình trên mạng lưới toán tử; 
Bước 2 – Định nghĩa các thuộc tính bẫy: Tương ứng với từng điều kiện kích hoạt bước 1, ta xác định được các 
thuộc tính AC của chương trình cần kiểm chứng. Sau đó định nghĩa các thuộc tính bẫy nAC dựa trên các thuộc tính 
AC: 
nAC=not AC; 
Bước 3 – Định nghĩa dữ liệu đầu vào cho việc kiểm chứng mô hình: Điểm đặc biệt của công cụ LESAR là mô 
hình đầu vào và các thuộc tính cần kiểm chứng đều được định nghĩa bằng ngôn ngữ Lustre chứa trong một tệp duy 
nhất. Do đó, dựa trên mã nguồn Lustre ban đầu và các thuộc tính bẫy nAC ở bước 2, chúng ta tạo ra được tệp đầu vào 
cho việc thực thi kiểm chứng mô hình. 
Bước 4 – Thực thi công cụ LESAR: Quá trình kiểm chứng mô hình cho chương trình Lustre được công cụ 
LESAR đảm nhận. Tương ứng với mỗi đầu vào, quá trình thực thi công cụ LESAR sẽ tạo ra các phản ví dụ tương ứng. 
Bước 5 – Xác định dữ liệu thử: Lần thực thi kiểm chứng mô hình với từng điều kiện kích hoạt các lộ trình trên 
mạng lưới toán tử, chúng ta sẽ nhận được kết quả là các phản ví dụ. Tương ứng với từng phản ví dụ được sinh sau khi 
thực thi kiểm chứng mô hình bằng công cụ LESAR ta có được dữ liệu thử. Chính những phản ví dụ này chính là các dữ 
liệu thử cho chương trình Lustre. 
Ví dụ: Đối với chương trình never trong Hình 4, dữ liệu thử được sinh ra dựa trên điều kiện kích hoạt lộ trình (E 
,L0 ,S ,L2 ,L3 ,S), được trình bày trong Bảng 2. 
Mã nguồn 
Lustre 
Thuộc tính bẫy 
 nAC=not(AC) 
LESAR 
Các phản ví dụ 
(Các dữ liệu thử 
cho chương 
trình Lustre) 
6đ
đ
h
k
đ
v
đ
n
c
k
36 
Trong p
ộng cho hệ th
Trước t
iều khiển nhi
iệu kiểu bool
hiển dùng cô
ến quạt gió: 
iệc), Hot và C
Hệ thốn
− Nút S
iều khiển khá
− Nếu h
hiệt độ của m
− Tươn
ho nhiệt độ củ
− Nếu h
hông thay đổ
Chương t
Lộ trì
Điều 
Thuộ
Phản 
Dữ liệ
hần này, chú
ống điều khiể
iên, chúng ta 
ệt độ này đượ
ean: Tlow, T
ng tắc và tín 
STOP nghĩa l
old tương ứn
g này hoạt độ
witch sử dụng
c không có tá
ệ thống đang 
ôi trường sẽ c
g tự, nếu hệ th
a môi trường
ệ thống đang 
i và không ản
rình Lustre củ
SIN
Bảng 
nh 
kiện kích hoạ
c tính bẫy 
ví dụ được tạ
u thử 
ng tôi ứng dụ
n nhiệt độ dự
hãy xem xét 
c cấu tạo bởi 
ok , Thigh, tư
hiệu cảm biến
à quạt đang n
g với không k
Hì
ng như sau: 
 để điều khiể
c dụng. 
ở trạng thái O
huyển sang tr
ống đang ở tr
 sẽ chuyển sa
ở trạng thái O
h hưởng đến n
a hệ thống đi
Hình 11
node headCo
return(STOP
let 
STOP= false
Deactivated=
Hot=On and
Cold=On an
tel 
H DỮ LIỆU THỬ
2. Sinh dữ liệu 
(E ,L0 
t AC=(fa
(not(L2
nAC=n
o ra --- TRA
true 
{1} 
Tương 
IV. 
ng kỹ thuật đ
a trên điều ki
một thiết bị đ
3 phần: công 
ơng ứng 3 m
 để có được 
gừng hoạt độn
hí nóng hay k
nh 10. Cấu trú
n bật và tắt hệ
n (mở) và ng
ạng thái Cold
ạng thái On v
ng trạng thái 
n (mở) và nh
hiệt độ hiện t
ều khiển nhiệ
. Chương trình
ntrol_v1(On, T
, Deactivated, H
 Æ if On then n
On and Tok; 
 Tlow 
d Thight 
 CHO ỨNG DỤ
thử dựa trên đi
,S ,L2 ,L3 ,S)
lse->pre( tru
) or L1) and f
ot(AC) 
NSITION 1 
ứng với vecto
ỨNG DỤNG
ược trình bày
ện kích hoạt c
iều khiển của
tắc, cảm biến 
ức: nhiệt độ 
4 chế độ điều
g, Deactivate
hông khí lạnh
c của bộ điều k
 thống. Nếu h
ười dùng chọ
 (lạnh). 
à người dùng
Hot (nóng). 
ưng người dù
ại. 
t độ trên được
 LUSTRE hệ th
low, Tok,Thigh
ot, Cold: Boo
ot pre STOP el
NG LUSTRE/SC
ều kiện kích ho
e and true
alse->true) 
--- 
r (E) 
 ở phần trước
ác lộ trình trê
 máy điều kh
nhiệt độ và q
thấp, bình th
 khiển tín hiệ
d tức là quạt 
 được đưa ra
hiển nhiệt độ 
ệ thống đang
n Thight thì q
 chọn Tlow th
ng không tác 
 trình bày tro
ống điều khiển
t:bool)
l); 
se pre STOP;
ADE SỬ DỤNG
ạt 
->false)) an
 để thực hiện 
n mạng lưới t
iển nhiệt độ tr
uạt gió. Thiết
ường, và nhiệ
u (STOP, De
gió ở chế độ c
. 
 ở trạng thái S
uạt gió sẽ hoạ
ì quạt gió sẽ 
động, thì hoạt
ng Hình 11. 
 nhiệt độ 
 ĐIỀU KIỆN K
d 
việc sinh dữ 
oán tử. 
ong Hình 10
 bị cảm biến c
t độ cao. Th
activated, Ho
hờ (quạt gió 
TOP (bị tắt) 
t động mạnh 
hoạt động chậ
 động của qu
ÍCH HOẠT 
liệu thử tự 
, hệ thống 
ho ta 3 tín 
iết bị điều 
t và Cold) 
không làm 
thì các 
làm cho 
m lại làm 
ạt gió sẽ 
Td
b
đ
th
c
s
rịnh Công Duy, N
Trong H
ữ liệu. 
Trong m
oolean (STOP
Dựa trê
iều khiển nhi
# 
1 
2 
3 
4 
5 
6 
7 
8 
9 
Tiếp th
ực hiện lần l
hính là các dữ
Ví dụ v
au: 
Thực th
guyễn Thanh B
ình 12, chươ
H
ạng lưới toá
, Deactivated
n mạng lưới t
ệt độ, chi tiết 
Bả
Lộ trình 
(On, Cold) 
(On, Deactiv
(On, Hot) 
(Tlow,Hot) 
(Thight, Cold)
(Tok, Deactiv
(On, _L4, ST
(On, _L4, ST
(On, _L4, ST
eo, chúng ta á
ượt cho từng 
 liệu thử. 
ới điều kiện 
Hìn
i LESAR chú
ình, Ioannis Paris
ng trình Lustr
ình 12. Mạng
n tử này, có 
, Hot và Cold
oán tử này, ta
trong Bảng 3.
ng 3. Các lộ trì
ated) 
ated) 
OP) 
OP, _L3, _L4
OP, _L1, _L2
p dụng công c
điều kiện kích
kích hoạt AC
h 13. Mã nguồn
ng ta có kết q
node he
r
var AC
let 
STO
STOP; 
Dea
Hot=
Cold
AC1
nAC
l
sis 
e trên được b
 lưới toán tử tư
4 cạnh đầu v
) và những c
 xác định đượ
nh và điều kiện
no
no
no
no
no
no
tru
, STOP) fa
, STOP) fa
ụ kiểm chứn
 hoạt, mỗi lầ
1= not(On) o
 Lustre của mô
uả như Hình 
atControl_v1(
eturns (nAC, S
1: bool; 
P=false -> if
ctivated=On an
On and TLow
=On and THig
= not(On) or 
=not AC1; 
iểu diễn bằng
ơng ứng của hệ
ào kiểu boole
ạnh nội bộ kh
c các lộ trình
 kích hoạt của 
Điều kiện k
t(On) or THig
t(On) or TOk
t(On) or Tlow
t(Tlow) or On
t(Thight) or On
t(Tok) or On
e and false Æ
lse Æ pre(fals
lse Æ pre(fals
g LESAR để s
n thực hiện ch
r THigh, ta x
 hình tương ứn
14. 
On,TLow,TOk,T
TOP,Deactivat
On then not 
d TOk; 
; 
h; 
THigh; 
 một mạng lư
 thống điều khi
an (On, Tlow
ác. 
và các điều k
hệ thống điều k
ích hoạt 
h 
 true 
eÆtrue) and
eÆtrue) and
inh ra dữ liệu
úng ta nhận k
ây dựng mô 
g vớ AC1= not
High: bool) 
ed,Hot, Cold: b
pre STOP el
ới toán tử dướ
ển nhiệt độ 
, Tok và Thi
iện kích hoạt 
hiển nhiệt độ 
 not(On) and
 On and false
 thử. Việc kiể
ết quả trả về
hình cần kiểm
(On) or THigh
ool); 
se pre 
i dạng một s
gh), 4 cạnh đ
tương ứng củ
 false Æ true 
 Æ true 
m chứng mô
 là các phản v
 chứng tươn
637 
ơ đồ luồng 
ầu ra kiểu 
a hệ thống 
hình được 
í dụ, cũng 
g ứng như 
6tư
L
tử
t
n
tr
c
c
L
G
c
c
k
38 
Quá trìn
Ngh
Khi đó 
Lần lượ
ơng ứng, ta c
# Đ
1 not(O
2 not(O
3 not(O
4 not(T
5 not(T
6 not(T
7 false
8 false
9 false
Hệ thố
ustre/SCADE
, dựa vào các
ạp hơn, việc s
Các hệ 
ăng lượng, h
ình phát triển
ác hệ thống p
Trong b
hương trình L
ustre/SCADE
iải pháp này
hương trình L
Chúng 
ác ứng dụng 
iểm thử hồi q
h kiểm chứn
TRA
not
ĩa là: 
On
dữ liệu thử tư
t thực hiện ki
ó thể sinh ra 
iều kiện kích
n) or Thight 
n) or TOk 
n) or Tlow 
low) or On 
hight) or On 
ok) or On 
 Æ true 
 Æ pre(falseÆ
 Æ pre(falseÆ
ng điều khiể
. Sau khi ứng
 phản ví dụ đ
inh dữ liệu th
thống phản ứ
àng không. Đ
, việc kiểm th
hản ứng, nên 
ài báo này, c
ustre, kết hợ
. Chúng tôi đ
 hoàn toàn có
ustre/SCADE
tôi sẽ tiếp tục
Lustre/SCAD
uy tự động ch
SIN
g sẽ tạo ra phả
NSITION 1 
 On or THigh
=0 hoặc THig
ơng ứng là (O
ểm chứng chư
tất cả các dữ l
Bảng 4. 
 hoạt 
true) and no
true) and On
n nhiệt độ là
 dụng kỹ thu
ược sinh ra, c
ử tự động sẽ g
ng ngày càng
ặc điểm chun
ử luôn được 
việc kiểm thử
húng tôi đã đ
p với công c
ã định nghĩa 
 thể được tự
. 
 áp dụng phư
E. Chúng tôi
o các hệ thốn
H DỮ LIỆU THỬ
Hình 14. K
n ví dụ là mộ
h=1 
n, Thight,T o
ơng trình Lu
iệu thử cho c
Các dữ liệu thử
t(On) and fal
 and false Æ
 một ví dụ 
ật kiểm chứng
húng ta sẽ có
iúp tiết kiệm 
V.
 được sử dụn
g quan trọng
quan tâm hàn
 các chương t
ề xuất giải ph
ụ kiểm chứn
được quy trìn
 động hóa nh
ơng pháp này
 cũng hướng 
g phản ứng n
 CHO ỨNG DỤ
ết quả thực thi L
t trường hợp 
k, Tlow)={0,1
stre của hệ th
hương trình n
 của hệ thống đ
se Æ true 
 true 
điển hình ch
 mô hình trên
 được các dữ 
được rất nhiề
KẾT LUẬN
g phổ biến tr
 nhất của nhữ
g đầu. Chươn
rình Lustre/SC
áp sử dụng đ
g mô hình L
h xây dựng t
ằm giảm chi 
 cho việc sin
đến khả năng
ói chung và cá
NG LUSTRE/SC
ESAR 
lỗi: 
,0,0} 
ống điều khiể
hư Bảng 4. 
iều khiển nhiệ
Dữ liệu thử
{0,1,0,0} 
{0,0,1,0} 
{0,0,0,1} 
{1,0,0,0} 
{1,0,0,0} 
{1,0,0,0} 
Giá trị bất k
Giá trị bất k
Giá trị bất k
o các hệ thố
 cơ sở các đi
liệu thử cần th
u chi phí cho 
ong ngành cô
ng hệ thống 
g trình Lustre
ADE càng tr
iều kiện kích
ESAR để sin
ập dữ liệu thử
phí và tăng h
h dữ liệu thử
 tự động hóa
c ứng dụng L
ADE SỬ DỤNG
n nhiệt độ với
t độ 
 (Dạng vector 
ỳ 
ỳ 
ỳ 
ng phản ứng
ều kiện kích h
iết. Với nhữn
quá trình kiểm
ng nghiệp qu
này là tính an
/SCADE đượ
ở nên quan tr
 hoạt trên mạ
h dữ liệu thử
 cho kiểm th
iệu quả của 
 tự động tron
 quá trình sin
ustre/SCADE
 ĐIỀU KIỆN K
 các điều kiện
(On, T
hight
,Tok, 
 được xây d
oạt trên mạng
g hệ thống lớ
 thử. 
an trọng như
 toàn, do đó
c sử dụng để
ọng. 
ng lưới toán 
 cho các chư
ử các chương
quy trình kiể
g kiểm thử h
h dữ liệu thử
 nói riêng. 
ÍCH HOẠT 
 kích hoạt 
T
low
))
ựng bằng 
 lưới toán 
n và phức 
 hạt nhân, 
 trong quá 
 phát triển 
tử của các 
ơng trình 
 trình này. 
m thử các 
ồi quy cho 
 cũng như 
Trịnh Công Duy, Nguyễn Thanh Bình, Ioannis Parissis 639 
VI. TÀI LIỆU THAM KHẢO 
[1] Trinh Cong Duy, Nguyen Thanh Binh, Ioannis Parissis, “Automatic Generation of Test Cases in Regression 
Testing for Lustre/SCADE”, Journal of Software Engineering and Applications, Vol. 6, 2013. 
[2] Trinh Cong Duy, Nguyen Thanh Binh, Ioannis Parissis, “Automatic generation of test cases in regression testing 
for Reactive Systems”, FAIR 2013, Hue, Vietnam, 2013. 
[3] Albert Benveniste, Gerard Berry, “The Synchronous Approach to Reactive and Real-Time Systems”, Proceedings 
of the IEEE, 1991. 
[4] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice, “LUSTRE: A Declarative Language for Programming 
Synchronous Systems”, ACM Symposium on Principles of Programming Languages, Munich, Germany, 1987. 
[5] Esterel Technologies website:  
[6] A. Lakehal and I. Parissis, “Lustructu: A Tool for the Automatic Coverage Assessment of Lustre Programs”, IEEE 
International Symposium on Software Reliability Engineering, Chicago, Illinois, USA, 2005. 
[7] Gordon Fraser, FranzWotawa, Paul E. Ammann, “Testing with model checkers: A survey”, Competence Network 
Softnet Austria, Austria, 2007. 
[8] Karolina Zurowska and Juergen Di, “Model-based generation of test cases for reactive systems”, Applied Formal 
Methods Group School of Computing Queen’s University Kingston, Ontario, Canada, 2010. 
[9] Nicolas Halbwachs, "Lustre program verification: the tool Lesar", Synchronous Programming of Reactive Systems 
Volume 215 of the series The Springer International Series in Engineering and Computer Science pp 139-147, 
1993. 
[10] Laya Madani, Virginia Papailiopoulou, Ioannis Parissis, “Towards a testing methodology for reactive system: a 
case study of a landing gear controller”, Laboratoire d’Informatique de Grenoble, 2006. 
[11] L. duBousquet, F. Ouabdesselam, J.- L.Richier, and N. Zuanon, “Lutess: testing environment for synchronous 
software”, Advances in Computing Science, Springer, 1998. 
[12] Nicolas Halbwachs, Pascal Raymond, “Validation of Synchronous Reactive Systems: from Formal Verication to 
Automatic Testing”, Grenoble, France, 1999. 
[13] Elizabeta Fourneret, Fabrice Bouquet, Frédéric Dadeau and Stéphane Debricon, “Selective Test Generation 
Method for Evolving Critical Systems”, Université de Franche-Comté, LIFC - INRIA CASSIS Project, 2010. 
TEST DATA GENERATION FOR LUSTRE/SCADE PROGRAMS USING 
THE ACTIVATION CONDITIONS 
Trinh Cong Duy, Nguyen Thanh Binh, Ioannis Parissis 
ABSTRACT-Testing is important activities in the software development process. Software development increasingly complex, 
requiring increasingly higher quality, it is even more important in developing software for reactive systems. Reactive systems are 
popularly developed in many indutrial fields such as aviation, energy, nuclear ... These systems usually require very high quality 
and rigorous testing activities before they are deployed for use. Lustre/SCADE is a formal synchronous declarative language widely 
used for modeling and specifying safety critical applications in the fields of avionics, transportation, and energy production. In such 
applications, the testing activity to ensure correctness of the system plays a crucial role. So, testing work need to be conducted 
regularly and continuously when there are any changes in the application. Besides, for those applications in this field, the test 
manually would be very difficult to implement and not effective, so the need to automate testing activities for Lustre/SCADE 
applications. In this paper, we focus on the test automation for applications Lustre / SCADE. We propose to use activation 
condition of operator network and usenmodel checking techniques to automatically generated test data. Finally, we apply this 
approach on one program Lustre for Heater Controller System.