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

ĐẠ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 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 - 2010 ĐẠ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 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. Phạm Ngọc Hùng Cán bộ đồng hướng dẫn: Ths. Đặng Việt Dũng HÀ NỘI - 2010 Đặc tả và kiểm chứng các phần mềm tương tranh i LỜI CẢM ƠN Lời đầu tiên em xin bày tỏ lòng biết ơn sâu sắc đến thầy Phạm Ngọc Hùng và thầy Đặng Việt Dũng đã tận tình hướng dẫn, chỉ bảo em trong quá trình thực hiện đề tài. Em xin chân thành cảm ơn các thầy cô giáo trong Khoa Công nghệ Thông tin, trường Đại học Công Nghệ, Đại học Quốc Gia Hà Nội đã tận tình giảng dạy, trang bị cho em những kiến thức quý báu trong suốt thời gian qua. Con xin chân thành cảm ơn ông bà, cha mẹ đã luôn động viên, ủng hộ con trong suốt thời gian học tập và thực hiện khóa luận tốt nghiệp. Tôi xin cảm ơn sự quan tâm, giúp đỡ và ủng hộ của anh chị em, bạn bè trong quá trình thực hiện khóa luận. Mặc dù đã cố gắng hoàn thành khóa luận trong phạm vi và khả năng cho phép 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. 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. Đặc tả và kiểm chứng các phần mềm tương tranh vi 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 ..............................................................................................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 Đặc tả và kiểm chứng các phần mềm tương tranh viii Danh mục các hình vẽ Hình 2.1: Nghiên cứu khí động học trên mô hình ô tô ..................................................4 Hình 2.2.1a: Mô hình hóa hành trình bay của máy bay................................................6 Hình 2.2.2a: Máy trạng thái DRINKS..........................................................................7 Hình 2.2.2b: Máy trạng thái Gate................................................................................8 Hình 2.3.1c: Tiến trình tuần tự BOMP.......................................................................10 Hình 2.3.1d: Sự tổng hợp tuần tự LOOP....................................................................10 Hình 2.3.1e : Sự tổng hợp song song hai tiến trình tuần tự. .......................................11 Hình 2.3.1a: Máy trạng thái PHIN ............................................................................12 Hình 2.3.1b: Máy trạng thái FORK ...........................................................................13 Hình 2.3.2.1a: Bữa tối của triết gia ...........................................................................13 Hình 2.3.2.1b: Deadlock............................................................................................14 Hình 2.4a: Mô hình hành động của chiếc ô tô............................................................16 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 Đặc tả và kiểm chứng các phần mềm tương tranh x Danh mục các bảng biểu Bảng 4.3.2a Những toán tử tương đương giữa FSP và Java ......................................32 Bảng 4.3.2b: Các thành phần cơ bản khi chuyển từ Java sang FSP:..........................32 Đặc tả và kiểm chứng các phần mềm tương tranh vii BẢNG KÝ TỰ VIẾT TẮT Ký tự viết tắt Ý nghĩa FSP (Finite State Process) Máy hữu hạn trạng thái LTS (Labelled Transition System) Máy dịch chuyển trạng thái có gán nhãn LTSA (LTS Analyzer) Công cụ hỗ trợ kiểm chứng với đặc tả là 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 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à: Đặc tả và kiểm chứng các phần mềm tương tranh 2 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. Đặ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 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. Đặc tả và kiểm chứng các phần mềm tương tranh 4 Chương 2: Các khái niệm cơ bản Trong chương này chúng ta sẽ tìm hiểu một số khái niệm 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ụ hỗ trợ kiểm chứng LTSA. 2.1 Phương pháp mô hình hóa Mô hình là một đại diện đơn giản hóa của thế giới thực. Mô hình được sử dụng rộng rãi trong kỹ thuật, để tập trung vào một khía cạnh cụ thể của một hệ thống thế giới thực [1]. Ví dụ, các nhà khoa học muốn nghiên cứu tính động học của một chiếc ô tô. Thay vì sử dụng một chiếc ô tô thật, nhà khoa học chỉ cần sử dụng mô hình của chiếc ô tô đó với điều kiện mô hình phải có hình dáng bên ngoài giống hệt chiếc ô tô thật. Khí động học của ô tô chỉ bị ảnh hưởng do hình dáng bên ngoài của nó nên nghiên cứu trên mô hình hoàn toàn cho kết quả chính xác giống như nghiên cứu trên chiếc ô tô thật. Hình 2.1: Nghiên cứu khí động học trên mô hình ô tô Như vậy phương pháp mô hình hóa có ưu điểm là tạo được môi trường gần giống với thực tế từ đó cho kết quả kiểm tra tương đối chính xác. Thiết kế có vai trò vô cùng quan trọng trong sản xuất phần mềm nói chung và 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 sẽ không thể nào đầy đủ được. Tuy nhiên ta hoàn toàn có thể giải quyết vấn đề đó nếu mô tả các hành động đó bằng FSP: Đặc tả và kiểm chứng các phần mềm tương tranh 6 Maybay = (catcanh -> bay -> hacanh -> Maybay). FSP có tính đệ quy nên ta có thể dễ dàng giải quyết bài toán trên. Ta có mô hình được phân tích từ mẫu FSP này: Hình 2.2.1a: Mô hình hóa hành trình bay của máy bay. Một phần mềm tương tranh bao gồm rất nhiều tiến trình, mỗi tiến trình là sự thực thi của một tiến trình tuần tự. Một tiến trình được chia làm một hoặc nhiều hành động nguyên tử ( hành động nguyên tử không thể chia được thành các hành động nhỏ hơn), các hành động này được thực thi một cách tuần tự. Mỗi hành động gây ra một sự chuyển tiếp từ trạng thái hiện tại sang trạng thái tiếp theo. Trình tự các hành động xảy ra có thể được xác định bằng một đồ thị chuyển tiếp. Nói cách khác, chúng ta có thể mô hình hóa các tiến trình thành các máy hữu hạn trạng thái [1]. Như vậy, chúng ta hoàn toàn có thể mô hình hóa chi tiết một ph