ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Lê Hồng Phong
ĐẶC TẢ VÀ KIỂM CHỨNG CÁC PHẦN MỀM
TƯƠNG TRANH
KHÓA LUẬN TỐT NGHIỆP HỆ ĐẠI HỌC CHÍNH QUY
Ngành: công nghệ phần
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Lê Hồng Phong
ĐẶC TẢ VÀ KIỂM CHỨNG CÁC PHẦN MỀM
TƯƠNG TRANH
nhưng chắc chắn sẽ không tránh khỏi những thiếu sót. Em rất mong nhận được sự
thông cảm, góp ý và tận tình chỉ bảo của quý thầy cô và các bạn.
Hà Nội, ngày 15 tháng 5 năm 2010
Sinh viên thực hiện
Lê Hồng Phong Đặc tả và kiểm chứng các phần mềm tương tranh
ii
TÓM TẮT
Phần mềm tương tranh, một phần mềm được ứng dụng rộng rãi trong các hệ
thống nhúng và các hệ thống điều khiển. Chúng có vai trò vô cùng quan trọng trong
việc điều khiển các hệ thống đó. Chỉ cần một lỗi nhỏ của phần mềm có thể gây ra hậu
quả vô cùng nghiêm trọng vì những hệ thống này có thể trực tiếp và gián tiếp ảnh
hưởng đến cuộc sống của con người. Chính vì vậy phần mềm tương tranh phải được
kiểm chứng để giảm thiểu tối đa lỗi của chương trình. Vì những lý do đó, đề tài “Đặc
tả và kiểm chứng các phần mềm tương tranh” đề cập tới phương pháp hình thức, các lý
thuyết về máy hữu hạn trạng thái (Finite State Process, FSP) và sử dụng máy hữu hạn
trạng thái để đặc tả thiết kế và mã nguồn của phần mềm tương tranh. Từ đó sử dụng
công cụ phân tích máy hữu hạn trạng thái để kiểm chứng xem thiết kế và mã nguồn
của phần mềm có lỗi và chạy đúng theo yêu cầu không.
2.3.2.2 Phân tích Deadlock 14
2.3.3 Thuộc tính An toàn 14
2.3.4 Thuộc tính Liveness 15
2.4 Công cụ LTSA 15
2.5 Kết luận 16
Chương 3: Kiểm chứng thiết kế 17
3.1 Đặc tả thiết kế bằng FSP 17
3.3. Kiểm chứng thiết kế bằng LTSA 23
3.3.1 Giao diện của công cụ LTSA 23
3.3.2 Check safety 24
3.3.3 Check Progress 25
3.3.4 Compile 25
3.3.5 LTS Analiser 27
3.3.6 LTSA Animator 28
3.4 Kết luận 30
Chương 4: Kiểm chứng cài đặt 31
Đặc tả và kiểm chứng các phần mềm tương tranh
vii
4.1 Phương pháp để kiểm chứng cài đặt 31
4.2 Cách chuyển từ mã nguồn Java sang FSP 31
4.3 Ứng dụng để chuyển mã nguồn bài toán “SingleLandBridge” 34
4.5 Kiểm chứng cài đặt 36
4.6 Kết luận 41
Chương 5: Kết luận 42
Tài liệu tham khảo 43
Hình 2.4b: LTSA animator điều khiển các hành động trong mô hình 2.4a 16
Hình 3.1: Mô tả các ô tô đi qua một chiếc cầu hẹp 18
Hình 3.3.1: Giao diện công cụ LTSA 23
Hình 3.3.2: Kết quả hiển thị sau khi check safety 24
Hình 3.3.3: Kết quả hiển thị khi check progress 25
Hình 3.3.4: Kết quả hiển thị khi biên dịch đoạn mã LTS 26
Hình 3.3.5: LTS Analiser SingleLaneBridge 27
Hình 3.3.6: Animator SingleLandBridge 29
Hình 4.5a: Mở tệp SafeBridge bằng công cụ LTSA 37
Đặc tả và kiểm chứng các phần mềm tương tranh
ix
Hình 4.5b: Check safety phương thức redExit 38
Hình 4.5c: Check prgress phương thức redExit 39
Hình 4.5d: Máy trạng thái REDEXIT 40
Hình 4.5e: Máy trạng thái REDEXIT trong thiết kế. 41
LTS
Đặc tả và kiểm chứng các phần mềm tương tranh
1
Chương 1: Giới thiệu
1.1 Nhu cầu thực tế và lý do thực hiện đề tài
Ngày nay, cùng với sự phát triển mạnh mẽ của máy móc phục vụ đời sống con
người là sự phát triển âm thầm của các hệ thống tương tranh. Chúng được tạo ra để
điều khiển hoạt động của những máy móc đó. Một hệ thống tương tranh có thể bao
gồm cả phần mềm và phần cứng nhưng cũng có thể chỉ có phần mềm. Phần mềm
tương tranh chính là linh hồn của hệ thống, giúp chúng hoạt động chính xác theo
những gì mà con người yêu cầu. Hiện nay, phần mềm tương tranh được ứng dụng rất
nhiều trong các hệ thống nhúng và điều khiển. Từ những vật dụng rất đơn giản trong
đời sống hàng ngày như nồi cơm điện, ti vi, đến những hệ thống điều khiển phức tạp
mô hình được đặc tả bằng FSP và sử dụng công cụ LTSA để kiểm chứng.
Với cách tiếp cận này, ta có được một quy trình kiểm chứng đầy đủ hai chiều, có
tính hệ thống từ pha kiểm thử đến pha cài đặt.
1.2 Mục tiêu của đề tài
Phương pháp hình thức là các kỹ thuật toán học được sử dụng để đặc tả, phát
triển và kiểm chứng các hệ thống phần mềm và phần cứng. Phương pháp tiếp cận này
đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao như hệ thống điều
khiển lò phản ứng hạt nhân, điều khiển tên lửa, khi vấn để an toàn hay an ninh có vai
trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển của hệ thống sẽ không
có lỗi. Khi kiểm chứng bằng phương pháp hình thức, điều đặc biệt là chúng ta không
cần dữ liệu đầu vào mà chỉ cần kiểm tra các mô hình mô tả các hành động, trạng thái
của hệ thống khi hoạt động.
Như vậy, đề tài cần giải quyết các công việc chính sau:
Tìm hiểu về phương pháp mô hình hóa, máy hữu hạn trạng thái, máy
dịch chuyển trạng thái có gán nhãn (Labelled Transition System, LTS)
và công cụ hỗ trợ kiểm chứng LTSA (Labelled Transition System
Analyzer).
Sử dụng công cụ hỗ trợ kiểm chứng LTSA để kiểm chứng thiết kế của
một hệ thống điều khiển được đặc tả bằng FSP.
Đặc tả mã nguồn Java của hệ thống điều khiển trên bằng FSP, sử dụng
công cụ hỗ trợ kiểm chứng LTSA để kiểm tra xem chương trình có lỗi và
đúng với thiết kế không.
Đặc tả và kiểm chứng các phần mềm tương tranh
3
1.3 Nội dung của khóa luận
Nội dung của khóa luận gồm 5 chương:
Chương 1 trình bày nhu cầu thực tế, lý do thực hiện đề tài và mục tiêu cần đạt
được.
Chương 2 giới thiệu những lý thuyết cơ bản về phương pháp mô hình hóa, máy
phần mềm tương tranh nói riêng. Phần mềm được lập trình ra có đạt yêu cầu hay
Đặc tả và kiểm chứng các phần mềm tương tranh
5
không là phụ thuộc vào thiết kế có chính xác hay không? Chính vì vậy, lựa chọn
phương pháp thiết kế phù hợp với đặc tính của phần mềm là hết sức quan trọng.
Khi thiết kế một phần mềm tương tranh, chúng ta phải mô tả chi tiết được các
hoạt động của phần mềm. Thiết kế càng chi tiết thì phần mềm hoạt động càng chính
xác. Tuy nhiên, để có được một thiết kế chính xác như vậy rất khó. Các phương pháp
thiết kế hiện tại chỉ đáp ứng được yêu cầu tạo ra thiết kế theo yêu cầu của sản phẩm.
Tuy nhiên chúng lại không giải quyết được vấn đề kiểm chứng các thiết kế đó. Như
vậy, chúng ta sẽ không thể tìm ra những hạn chế của thiết kế. Bài toán đó sẽ được giải
quyết bằng việc khai thác ưu điểm nổi bật của phương pháp mô hình hóa:
- Phương pháp mô hình hóa có thể tạo ra một thiết kế mô tả được chi tiết hoạt
động của hệ thống. Ở đây chúng ta sẽ sử dụng mẫu FSP để đặc tả thiết kế đó.
- Phân tích mẫu thiết kế thông qua việc sử dụng công cụ LTSA, chúng ta có thể
kiểm tra được mẫu thiết kế được đặc tả bằng FSP có chạy đúng, chính xác hay không.
Khi phần mềm đã được viết xong, với phương pháp hình thức, chúng ta có thể
mô hình hóa mã nguồn của phần mềm để kiểm chứng xem phần mềm có chạy đúng
theo thiết kế hay không. Đây chính là ứng dụng ngược rất hay của phương pháp hình
thức.
2.2 FSP (Finite State Process)
2.2.1 Khái niệm FSP
Máy hữu hạn trạng thái (FSP) được tạo ra để mô tả các mô hình tiến trình. FSP
có thể mô tả được những hành động, trạng thái của tiến trình. Ta lấy một ví dụ đơn
giản mô tả các hành động cất cánh, bay, hạ cánh của một chiếc máy bay:
cất cánh -> bay -> hạ cánh -> cất cánh -> bay -> hạ cánh -> ……
Ta có thể thấy nếu máy bay còn hoạt động được thì các hành động này sẽ liên
tục xảy ra đến khi nào mà máy bay không được sử dụng nữa. Chính vì vậy mô tả trên
Trong đó: Maybay là một tiến trình
catcanh, bay, hacanh là các hành động.
Lựa chọn (| Choice): Nếu x, y là các hành động thì (x -> Q | y -> P) mô tả một
tiến trình trong đó các hành động đầu tiên tham gia là x hoặc y. Các hành động tiếp
theo hoạt động theo mô tả của Q nếu hành động đầu tiên xảy ra là x, các hành động
tiếp theo hoạt động theo mô tả của P nếu hành động đầu tiên xảy ra là y.
Ví dụ mô tả việc lấy nước uống ở máy đun nước [1], nếu ấn nút đỏ thì được cà
phê, nếu ấn nút xanh thì được trà:
DRINKS = (red -> coffee -> DRINKS
| blue -> tea -> DRINKS).
Khi phân tích mẫu FSP trên ta đuợc mô hình:
Hình 2.2.2a: Máy trạng thái DRINKS
Lập chỉ mục cho các quy trình và hành động (indexed process and actions)
Khi mô hình các tiến trình và hành động có có những trường hợp những tiến trình và
hành động đó có rất nhiều giá trị. Ta có thể gán nhãn cho các quy trình và hành động
đó và lập chỉ mục cho chúng. Ví dụ FSP mô tả hành động vào, ra của 3 chiếc ô tô khi
qua 3 cổng của một trạm soát vé:
Đặc tả và kiểm chứng các phần mềm tương tranh
8
Gate = (in[1] -> out[1] -> Gate
| in[2] -> out[2] -> Gate
| in[3] -> out[3] -> Gate).
Trong đó [1], [2], [3] là chỉ mục của các hành động in và out.
Kết quả khi phân tích bằng công cụ LTSA:
Trong ví dụ này thì Alphabet của WRITE là write[0 3].
2.2.3 Quy trình tuần tự
Các tiến trình trong FSP được chia làm 3 loại:
- Các tiến trình cục bộ (local process) được định nghĩa là một trạng thái trong
một tiến trình cơ bản [1].
- Tiến trình cơ bản (primitive process) được xác định bởi tập hợp các tiến trình
cục bộ. Một tiến trình cục bộ được xác định bằng cách sử dụng STOP, ERROR, tiền
hành động (Action prefix) và lựa chọn (|, choice) [1].
- Tiến trình tuần tự ( sequential process) là một tiến trình có thể kết thúc. Một
tiến trình có thể kết thúc nếu một tiến trình cục bộ END có thể được với tới từ trạng
thái bắt đầu của nó [1].
Đặc tả và kiểm chứng các phần mềm tương tranh
10
Tiến trình cục bộ END: Tiến trình cục bộ END biểu thị trạng thái mà tiến trình
kết thúc thành công. Một tiến trình đúng đắn khi không có hành động nào tiếp theo xảy
ra sau END. Về mặt ngữ nghĩa nó tương tự như STOP. Tuy nhiên, STOP là một trạng
thái mà tiến trình tạm ngưng quá sớm, thường là do deadlock. STOP được sử dụng khi
ta muốn kết thúc một tiến trình [1]. Ví dụ sau mô tả tiến trình hẹn giờ một quả bom nổ
trong đó trạng thái E là trạng thái kết thúc:
Hình 2.3.1c [1] : Tiến trình tuần tự BOMP
Sự tổng hợp các tiến trình tuần tự: Nếu Q là một tiến trình tuần tự, P là một
tiến trình cục bộ, sau đó P;Q biểu diễn cho sự tổng hợp tuần tự như vậy khi P kết thúc,
P;Q sẽ trở thành tiến trình Q [1].
Nếu chúng ta định nghĩa tiến trình SKIP = END then P; SKIP ≡ P and SKIP; P ≡
P. Một sự tổng hợp tuần tự trong FSP luôn luôn có dạng: SP1;SP2;….;SPn;LP [1]
Nơi SP1;…;SPn là sự tổng hợp tuần tự và LP là tiến trình cục bộ. Một sự tổng
hợp tuần tự có thể xuất hiện ở bất cứ chỗ nào trong định nghĩa của một tiến trình cơ
bản mà một tiến trình cục bộ tham chiếu đến có thể xuất hiện [1].
Phân tích mẫu LTS này ta được 2 mô hình tương ứng: Hình 2.3.1a: Máy trạng thái PHIN
Đặc tả và kiểm chứng các phần mềm tương tranh
13 Hình 2.3.1b: Máy trạng thái FORK
2.3.2 Deadlock
2.3.2.1 Khái niệm
Deadlock xảy ra trong hệ thống khi tất cả các tiến trình của hệ thống đều bị
chặn hoặc không đủ điều kiện để tiến trình đó hoạt động.
Một ví dụ về deadlock điển hình là: “bữa tối của triết gia”. Một bàn ăn có 5 cái
ghế, 5 vị triết gia cùng ngồi vào chiếc bàn. Khi bày đũa, người phục vụ chỉ để vào giữa
mỗi người 1 chiếc đũa. Như vậy 2 bên mỗi vị triết gia đều có 2 chiếc đũa nhưng nếu
người này cầm đũa thì người kia sẽ không có:
Hình 2.3.2.1a: Bữa tối của triết gia[1]
Nếu số đũa được chia đều ra cho năm người, như vậy mỗi người sẽ có một
chiếc đũa. Cả năm người sẽ không thể thực hiện bữa ăn của mình với một chiếc đũa
được, khi đó deadlock xảy ra.
Đặc tả và kiểm chứng các phần mềm tương tranh
14
Thuộc tính tiến trình (progress): Một đặc tính progress khẳng định tại bất kỳ
trạng thái nào của một trong các hoạt động của một thực thi phải xảy ra. Tức là các
hoạt động thành công và phải được kết thúc .
Phân tích tiến trình: phân tích tiến trình để tìm ra tập kết thúc của các trạng
thái. Tập kết thúc của trạng thái là một tập hợp trong đó một trạng thái có thể truy cập
từ mọi trạng thái khác trong tập hợp thông qua một hoặc nhiều chuyển tiếp và không
có chuyển tiếp nào từ bên trong tập hợp ra trạng thái bên ngoài tập hợp.
2.4 Công cụ LTSA
LTSA (Labelled Transition System Analiser) là một công cụ hỗ trợ kiểm chứng
với đặc tả là LTS. LTSA sử dụng để kiểm tra tính mong muốn và không mong muốn
cho tất cả các trình tự có thể có của các sự kiện và hành động [1]. LTSA được tải miễn
phí từ trang web [4] chính thức của cuốn sách “Concurrency: State Models and Java
Programs second edition [1]”. Ta lấy ví dụ LTSA phân tích một đặc tả LTS cho trạng
thái vào, ra của một chiếc ô tô khi qua cầu:
CAR = (enter -> exit -> CAR).
Copyright: Tài liệu đại học ©