Đồ Án đặc tả và kiểm chứng các phần mềm tương tranh

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.

Do thời gian có hạn nên phần thực nghiệm trong khóa luận này em chỉ thực hiện kiểm chứng một applet được viết bằng Java. Thiết kế của bài toàn đã được đặc tả sẵn bằng FSP. Nhiệm vụ của em là kiểm chứng xem thiết kế đó có lỗi xác hay không và chuyển mã nguồn Java của applet thành FSP để kiểm chứng xem mã nguồn có chạy đúng theo thiết kế hay không.









MỤC LỤC


Chương 1: Giới thiệu 1

1.1 Nhu cầu thực tế và lý do thực hiện đề tài 1

1.2 Mục tiêu của đề tài 2

1.3 Nội dung của khóa luận 3

Chương 2: Các khái niệm cơ bản 4

2.1 Phương pháp mô hình hóa 4

2.2 FSP 5

2.2.1 Khái niệm FSP 5

2.2.2 Các thành phần cơ bản trong FSP 6

2.2.3 Quy trình tuần tự 9

2.3 LTS 11

2.3.1 LTS 11

2.3.2 Deadlock 13

2.3.2.1 Khái niệm 13

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 26

3.3.6 LTSA Animator 28

3.4 Kết luận 29

Chương 4: Kiểm chứng cài đặt 30

4.1 Phương pháp để kiểm chứng cài đặt 30

4.2 Cách chuyển từ mã nguồn Java sang FSP 30

4.3 Ứng dụng để chuyển mã nguồn bài toán “SingleLandBridge” 33

4.5 Kiểm chứng cài đặt 35

4.6 Kết luận 40

Chương 5: Kết luận 41

Tài liệu tham khảo 42


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 như hệ thống điều khiển tên lửa đều có một hoặc nhiều phần mềm tương tranh điều khiển.

Những vật dụng, hệ thống điều khiển này gắn bó chặt chẽ với chúng ta, chỉ cần một lỗi nhỏ của phần mềm tương tranh cũng có thể gây ra hậu quả nghiêm trọng. Đã có những con tàu vũ trụ vừa mới rời khỏi mặt đất thì đã rơi, tiêu tốn hàng tỷ đô la để nghiên cứu, chế tạo nó. Nguyên nhân gây ra tai nạn đó chính là do lỗi của hệ thống điều khiển con tàu.

Chính vì vậy, yêu cầu kiểm chứng an toàn cho các hệ thống tương tranh là hoàn toàn tất yếu. Hiện nay, song song với quá trình sản xuất phần mềm luôn có một quá trình kiểm thử (testing) phần mềm. Tuy nhiên, kiểm thử là chưa đủ vì các phương pháp kiểm thử hiện tại chỉ là kiểm tra dữ liệu đầu ra của phần mềm rồi so sánh với dữ liệu đầu vào để kiểm tra xem chương trình chạy có lỗi hay không. Chúng không hề kiểm tra được chi tiết hoạt động của chương trình và không kiểm soát được những lỗi tiềm ẩn ngay cả khi chương trình vẫn chạy đúng. Nếu phần mềm phát hành ra mà vẫn còn chứa lỗi thì nhà sản xuất phải thu hồi sản phẩm để sửa chữa. Điều này làm giảm uy tín và tiêu tốn nhiều tiền của nhà sản xuất.

Chúng ta hoàn toàn có thể khắc phục được những vấn đề trên bằng cách sử dụng phương pháp hình thức để đặc tả và kiểm chứng những phần mềm đòi hỏi tính an toàn cao, nhất là các phần mềm tương tranh.

Cách tiếp cận của khóa luận là:

Trước hết, phải đảm bảo có một thiết kế đúng, chính xác bằng cách đặc tả thiết kế bằng FSP[1] và sử dụng công cụ LTSA[1][4] để kiểm chứng thiết kế đó. Sau khi thiết kế đã được kiểm tra và thẩm định tính đúng đắn, chúng ta tiến hành cài đặt chương trình.

Sau khi đã xây dựng xong phần mềm, có một câu hỏi đặt ra là liệu cài đặt có đúng với thiết kế không? Chúng ta đã có công cụ để kiểm tra tính đúng đắn của thiết kế vì vậy giải pháp cho bài toán này chính là chuyển mã nguồn của cài đặt thành chính 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.

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 hữu hạn trạng thái, máy dịch chuyển trạng thái có gán nhãn và công cụ phân tích LTSA của nó để ứng dụng trong kiểm chứng.

Chương 3 trình bày ứng dụng FSP và LTSA để kiểm chứng một thiết kế xem có chính xác với yêu cầu bài toán đặt ra không?

Chương 4 trình bày cách chuyển từ Java sang FSP để ứng dụng kiểm chứng một chương trình có thỏa mãn thiết kế hay không?

Chương 5 khái quát những kết quả đạt được và hướng phát triển trong tương lai.