Khóa luận Đặc tả và kiểm chứng các phần mềm tương tranh - Lê Hồng Phong

ĐẠ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 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 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 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 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 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 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 28 Hình 4.5a: Mở tệp SafeBridge bằng công cụ LTSA 36 Hình 4.5b: Check safety phương thức redExit 37 Hình 4.5c: Check prgress phương thức redExit 38 Hình 4.5d: Máy trạng thái REDEXIT 39 Hình 4.5e: Máy trạng thái REDEXIT trong thiết kế. 40 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 31 Bảng 4.3.2b: Các thành phần cơ bản khi chuyển từ Java sang FSP: 31 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 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. 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 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: 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ần mềm tương tranh với đặc tả là FSP. 2.2.2 Các thành phần cơ bản trong FSP Action prefix ((x -> P)): Nếu x là một hành động và P là một tiến trình thì một action frefix (x -> P) mô tả một tiến trình trong đó các hành động x hoạt động đúng theo mô tả của tiến trình P [1]. Tiến trình P phải viết hoa chữ cái đầu, hành động x viêt bằng chữ cái thường. Ta lấy lại ví dụ trên phần 2.2.1 : Maybay = (catcanh -> bay -> hacanh -> Maybay). 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é: 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: Hình 2.2.2b: Máy trạng thái Gate Tham số tiến trình (Process parameters): khi tiến trình và hành động có nhiều giá trị thì thay vì đánh chỉ mục thì chúng ta có thể tạo tham số để mô tả tiến trình bằng FSP được gọn hơn. Ta lấy ví dụ Gate ở trên: const N = 3 Gate = ( in[i:1..N] -> out[i] -> Gate). Trong đó i:1..N có nghĩa i có giá trị lần lượt từ 1 đến N. Hành động được đảm bảo (Guarded Action): thường rất hữu dụng để định nghĩa các hành động cụ thể nhưng muốn xảy ra phải thỏa mãn một điều kiện nào đó. Ví dụ mô tả đám đông vào thang máy, thang máy cho phép chở 10 người, nếu số người quá quy định thì phải ra bớt, ngược lại có thể thêm người vào vì còn nhiều người đang chờ được vào: Count(N=10) = Count[1], Count[i:1..N] = (when(i Count[i+1] | when(i>N) out -> Count[i-1]). Hành động được đảm bảo bởi “when” đảm bảo cho thang máy hoạt động đúng công suất. Khi số người quá quy định thì phải ra ngoài bớt, khi số người trong thang chưa tới giới hạn thì có thể tiếp tục vào. Alphabet của tiến trình (Process Alphabet): Alphabet của một tiến trình là một tập hợp tất cả cách hành động mà nó có thể tham gia. Ta lấy một ví dụ định nghĩa WRITE sử dụng write[1] và write[3]: WRITER = (write[1]->write[3]->WRITER) +{write[0..3]}. 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]. 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]. Ví dụ tiến trình P123 và LOOP: Hình 2.3.1d[1]: Sự tổng hợp tuần tự LOOP Sự tổng hợp song song các tiến trình tuần tự: Sự tổng hợp song song SP1 || SP2 của hai tiến trình tuần tự SP1 và SP2 kết thúc khi cả hai tiến trình cùng kết thúc. Nếu kết thúc có thể tới được trong SP1 || SP2 thì nó là tiến trình tuần tự [1]. Hình dưới cho một ví dụ về sự tổng hợp song song của tiến trình tuần tự.: Hình 2.3.1e[1] : Sự tổng hợp song song hai tiến trình tuần tự. 2.3 LTS (Labelled Transition System) 2.3.1 LTS Khái niệm: Về cơ bản LTS[1][2] (Lebelled Transition System) giống FSP, mỗi mô tả FSP có một mô tả máy trạng thái (LTS) tương ứng. Mỗi LTS tương ứng với một quá trình FSP là một đồ thị. Ta lấy ví dụ LTS mô tả bài toán “bữa tối của triết gia” [1]: PHIL = (sitdown->right.get->left.get ->eat->left.put->right.put ->arise->PHIL). FORK = (get -> put -> FORK). ||DINERS(N=5)= forall [i:0..N-1] (phil[i]:PHIL ||{phil[i].left,phil[((i-1)+N)%N].right}::FORK). menu RUN = {phil[0..4].{sitdown,eat}} 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 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. Hình 2.3.2.1b: Deadlock[1] 2.3.2.2 Phân tích Deadlock Trong mô hình trạng thái hữu hạn FSP của một tiến trình, một trạng thái deadlock là một trạng thái không có sự chuyển tiếp đi. Một tiến trình ở trạng thái như vậy có thể không tham gia vào các hành động tiếp theo. Trong FSP trạng thái deadlock này được biểu diễn bằng một biến cục bộ STOP[1]. Nhìn chung, hệ thống tương tranh với rất nhiều tiến trình xảy ra rất có thể sẽ xảy ra bế tắc. Việc kiểm tra, phân tích deadlock trong đồ thị LTS là hết sức quan trọng. Nó đảm bảo cho việc thiết kế chương trình phần mềm đúng đắn và chính xác. Công cụ LTSA có sẵn chức nằng phân tích deadlock, chúng ta sẽ nghiên cứu ở phần sau. 2.3.3 Thuộc tính An toàn (safety property) Khái niệm safety: Thuộc tính an toàn đảm bảo không có lỗi xảy ra trong quá trình thực hiện các tiến trình của một hệ thống tương tranh. Safety property: Về mặt cú pháp, những tiến trình FSP được thêm vào trước từ khóa property để khẳng định nó là một thuộc tính an toàn. Một thuộc tính an toàn khẳng định tất cả các hành động trong Alphabet của nó đều được nó chấp nhận. Điều này đảm bảo cho hệ thống hoạt động đồng bộ bởi tiến trình an toàn này. Ví dụ mô tả trạng thái đèn xanh, đỏ của đèn giao thông: property TRAFICLIGHT = (red -> enter |blue -> exit). 2.3.4 Thuộc tính Liveness (Liveness property) Khái niệm: Thuộc tính Liveness là thuộc tính quan trọng nhất trong chương hệ thống tương tranh, nó khẳng định khi chương trình kết thúc có đạt trạng thái tốt hay không [1]. 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). Hình 2.4a: Mô hình hành động của chiếc ô tô Hình 2.4b: LTSA animator điều khiển các hành động trong mô hình 2.4a Mỗi hành động được chọn trong Animator sẽ điều khiển các hoạt động tương ứng trong mô hình. 2.5 Kết luận Trong chương này, chúng ta đã tìm hiểu một số khái niệm phần mềm tương tranh, phương pháp mô hình hóa, máy hữu hạn trạng thái FSP và công cụ hỗ trợ kiểm chứng LTSA. Đây là những khái niệm cơ bản mà chúng ta sẽ phải trang bị để có thể thực hiện đặc tả và kiểm chứng thiết kế, cài đặt một phần mềm tương tranh mà chúng ta sẽ tìm hiểu ở hai chương sau. Chương 3: Kiểm chứng thiết kế Một bản thiết kế, dù cẩn thận và chi tiết đến đâu cũng có thế tồn tại thiếu sót, chính vì vậy mô hình hóa thiết kế là một cách để kiểm chứng hiệu quả nhất. Phương pháp mô hình hóa được sử dụng rất rộng rãi trong kỹ thuật, ở một phương diện nào đó, mô hình có thể đại diện cho vật chất, mang đầy đủ các tính chất của vật chất. Khi chúng ta kiểm tra trên mô hình sẽ cho kết quả tương đương với ở ngoài thực tế. Trong thiết kế cũng vậy, mô hình hóa thiết kế sẽ cho chúng ta kiểm tra thiết kế một cách toàn diện, xem nó có đúng với yêu cầu bài toán đặt ra không? 3.1 Đặc tả thiết kế bằng FSP Như chúng ta đã biết ở trên, FSP rất phù hợp cho việc thiết kế một phần mềm tương tranh, tuy nhiên, chúng ta vẫn cần kiểm chứng xem thiết kế liệu có đúng như yêu cầu của bài toán không? LTS Analiser ( LTSA) dùng để phân tích FSP thành các mô hình, thuận tiện cho việc kiểm tra thiết kế. Để thuận tiện cho việc hình dung, chúng ta cùng xem một ví dụ đặc tả thiết kế bằng FSP. Bài toán “SingleLandBridge” được phát biểu như sau: Trên một con đường có một chiếc cầu hẹp, chiếc cầu chỉ đủ cho một làn xe chạy. Yêu cầu đặt ra là tạo ra một chương trình điều khiển sự ra, vào của ô tô ở hai đầu cầu. Chương trình sẽ cho các ô tô đi tới cầu được qua cầu nếu trên cầu chỉ có ô tô đi cùng chiều hoặc không có ô tô chạy theo hướng ngược lại. Nếu trên cầu có xe đang qua cầu theo hương ngược lại hoặc có ô tô đã chờ ở đầu cầu bên kia trước thì ô tô này phải chờ cho chiếc xe đó qua trước. Chúng ta hãy cùng nghiên cứu yêu cầu thiết kế cho bài toán. Thiết kế phải thực hiện được nhiệm vụ chỉ cho phép ô tô đó được qua cầu nếu trên cầu có ô tô đi cùng hướng hoặc hướng ngược lại không có ô tô. Thiết kế của bài toán này đã được đặc tả bằng FSP trong các ví dụ có sẵn của công cụ LTSA. Ví dụ này mang tên “SingleLandBridge”. Tuy nhiên, chúng ta sẽ tìm hiểu chi tiết cách đặc tả thiết kế bằng các máy trạng thái FSP. Ta quy định ô tô qua chiếc cầu sẽ phân thành hai loại là ô tô đỏ (red) đi từ phía tây sang và ô tô xanh (blue) đi từ phía đông sang. Hình 3.1: Mô tả các ô tô đi qua một chiếc cầu hẹp[1] Trước khi đặc tả hai yêu cầu của thiết kế, chúng ta hãy định nghĩa hai tiến trình ô tô và cầu trước: Tiến trình ô tô (CAR) có hai hành động là đi vào (enter) và đi ra (exit) khi qua cầu: CAR = (enter -> exit -> CAR). Tuy nhiên nếu ô tô đi theo đoàn thì mỗi lần chiếc ô tô dẫn đầu được qua cầu thì cả đoàn của chiếc ô tô đó đều được qua. Ta có thêm một định nghĩa những chiếc ô tô nữa: CARS = (red:CONVOY || blue:CONVOY). Trong đó red, blue là những chiếc xe đỏ hoặc xanh, CONVOY là tiến trình mô tả tính chất theo đoàn của những chiếc ô tô. CONVOY được định nghĩa như sau: CONVOY = [ID]:CAR ID là số ô tô có trong đoàn ô tô. Nếu một chiếc ô tô đỏ lên cầu, đồng nghĩa với việc trên cầu đó không có chiếc ô tô xanh nào. Nếu trên cầu đã có ô tô đỏ rồi nhưng do các ô tô đỏ đi cùng chiều nên chiếc ô tô đó vẫn được lên cầu, khi đó số ô tô đỏ trên cầu sẽ tăng thêm một. Ngược lại, khi ô tô đỏ đó rời cầu, số ô tô đỏ sẽ giảm đi một. Nếu trên cầu chỉ có một chiếc ô tô đỏ, khi chiếc ô tô đó rời cầu thì trên cầu sẽ không còn chiếc ô tô nào, ta gọi đó là thuộc tính ONEWAY. Khi xảy ra ONEWAY, hai đầu cầu bên nào có ô tô tới trước sẽ được qua trước. Ta có định nghĩa tiến trình RED và thuộc tính ONEWAY: RED[i:ID] = (red[ID].enter -> RED[i+1] |when(i==1)red[ID].exit -> ONEWAY |when( i>1)red[ID].exit -> RED[i-1] ) Thuộc tính an toàn ONEWAY khẳng định chiếc cầu an toàn và cho phép ô tô qua cầu khi trên cầu chỉ có một chiếc ô tô và chiếc ô tô đó đã thoát ra ngoài chiếc cầu: property ONEWAY = (red[ID].enter -> RED[1] |blue[ID].enter -> BLUE[1] ) Tương tự như vậy ta cũng có tiên trình BLUE: BLUE[i:ID] = (blue[ID].enter -> BLUE[i+1] |when(i==1)blue[ID].exit -> ONEWAY |when( i>1)blue[ID].exit -> BLUE[i-1] ) Trên chiếc cầu bao giờ cũng chỉ có một loại ô tô, hoặc là ô tô đỏ, hoặc là ô tô xanh. Nếu có cả ô tô đỏ và ô tô xanh thì chắc chắn sẽ xảy ra tai nạn. Khi trên cầu không có ô tô xanh, tức là ô tô đỏ được qua cầu và ngược lại, trên cầu không có ô tô đỏ thì ô tô xanh được qua cầu. Ta có định nghĩa tiến trình cầu: BRIDGE = BRIDGE[0][0], // cầu trống BRIDGE[nr:T][nb:T] = //nr, nb là số ô tô đỏ, số ô tô xanh có trên cầu (when (nb==0) // T là số loại ô tô có trên cầu red[ID].enter -> BRIDGE[nr+1][nb] |red[ID].exit -> BRIDGE[nr-1][nb] |when (nr==0) blue[ID].enter -> BRIDGE[nr][nb+1] |blue[ID].exit -> BRIDGE[nr][nb-1] ). Bây giờ chúng ra sẽ đặc tả bằng FSP các yêu cầu mà thiết kế phải giải quyết. - Ô tô được lên cầu khi trên cầu không có ô tô đi ngược chiều hoặc có ô tô đi cùng chiều: NOPASS1 = C[1], C[i:ID] = ([i].enter -> C[i%N+1]). - Sau khi tất cả những chiếc xe đi cùng chiều rời cầu, xe ở một trong hai đầu cầu sẽ được phép qua cầu: NOPASS2 = C[1], C[i:ID] = ([i].exit -> C[i%N+1]). ||CONVOY = ([ID]:CAR || NOPASS1 || NOPASS2). ||CARS = (red:CONVOY || blue:CONVOY). ||SingleLaneBridge = (CARS || BRIDGE || ONEWAY ). Tổng hợp tất cả các máy hữu hạn trạng thái FSP ta được một máy dịch chuyển trạng thái có gán nhãn LTS hoàn chỉnh để đặc tả thiết kế bài toán: /** Concurrency: State Models and Java Programs * Jeff Magee and Jeff Kramer */ /* Single Lane bridge Red cars go from west to east Blue cars go from east to west */ const N = 3 // number of each type of car range T = 0..N // type of car count range ID= 1..N // car identities BRIDGE = BRIDGE[0][0], //initially empty BRIDGE[nr:T][nb:T] = //nr is the red count, nb the blue count (when (nb==0) red[ID].enter -> BRIDGE[nr+1][nb] |red[ID].exit -> BRIDGE[nr-1][nb] |when (nr==0) blue[ID].enter -> BRIDGE[nr][nb+1] |blue[ID].exit -> BRIDGE[nr][nb-1] ). CAR = (enter->exit->CAR). /* cars may not overtake each other */ NOPASS1 = C[1], C[i:ID] = ([i].enter -> C[i%N+1]). NOPASS2 = C[1], C[i:ID] = ([i].exit -> C[i%N+1]). ||CONVOY = ([ID]:CAR || NOPASS1 || NOPASS2). ||CARS = (red:CONVOY || blue:CONVOY). ||SingleLaneBridge = (CARS || BRIDGE || ONEWAY ). property ONEWAY = (red[ID].enter -> RED[1] |blue[ID].enter -> BLUE[1] ), RED[i:ID] = (red[ID].enter -> RED[i+1] |when(i==1)red[ID].exit -> ONEWAY |when( i>1)red[ID].exit -> RED[i-1] ), BLUE[i:ID] = (blue[ID].enter -> BLUE[i+1] |when(i==1)blue[ID].exit -> ONEWAY |when( i>1)blue[ID].exit -> BLUE[i-1] ). 3.3. Kiểm chứng thiết kế bằng LTSA Sau khi đã đặc tả xong thiết kế của bài toán bằng FSP chúng ta tiến hành kiểm chứng thiết kế đó bằng cách sử dụng công cụ hỗ trợ kiểm chứng LTSA để phân tích mẫu LTS vừa được tạo ra. 3.3.1 Giao diện của công cụ LTSA LTSA có giao diện trực quan rất dễ sử dụng như ảnh bên dưới: Hình 3.3.1: Giao diện công cụ LTSA Trong cửa sổ giao diện của chương trình có 3 khung nhìn: - Edit: để soạn thảo mã cho chương trình hoặc hiển thị đoạn mã đã có sẵn. - Output: nơi trả về kết quả khi kiểm tra độ an toàn hoặc khi biên dịch đoạn mã. - Draw: Hiển thị kết quả là các mô hình khi biên dịch đoạn mã LTS. Chi tiết về 3 khung nhìn này chúng ta sẽ tìm hiểu ở các phần tương ứng tiếp theo. Nếu muốn viết một đoạn mã mới, chúng ta chỉ cần nhấn vào biểu tượng New File hoặc vào thực đơn File chọn New. Khi muốn lưu đoạn mã lại ta nhấn vào biểu tượng Save File hoặc tại hộp chọn File chọn Save, đặt tên cho đoạn mã và chọn OK. Kiểu file mặc định là lts. Nếu muốn mở một đoạn mã có sẵn, nhấn và biểu tượng Open file hoặc tại thực đơn File chọn Open… . Khi công việc chuẩn bị mã đã xong, ta tiến hành kiểm tra đoạn mã: 3.3.2 Check safety Check safety sẽ kiểm tra xem chương trình của bạn đã được thiết kế có an toàn hay không? Chương trình sẽ phân tích những tiến trình có trong thiết kế của bạn và phân tích xem trong quá trình các tiến trình đó hoạt động có xảy ra deadlock hay không? Tại thực đơn Check chọn Safety Hình 3.3.2: Kết quả hiển thị sau khi check safety Trên hình vẽ, công cụ LTSA đã phân tích tất cả các máy trạng thái được tạo ra để kiểm tra xem thiết kế có an toàn không? Cụ thể trong bài toán này chúng ta có kết quả kiểm tra là “ No deadlock/errors” tức là thiết kế không có lỗi và không có deadlock. 3.3.3 Check Progress Check progess có tác dụng tìm ra những hành động có vi phạm hay không, điển hình là hành động đó không có trạng thái kết thúc và không thể thực hiện được. Tại thực đơn Check chọn Progress Hình 3.3.3: Kết quả hiển thị khi check progress Trong cửa sổ output, tất cả các máy trạng thái được phân tích để tìm các vi phạm có thể có. Cụ thể trong thiết kế này kết quả kiểm tra là “ No progress violations detected” nghĩa là không có progress nào vi phạm. 3.3.4 Compile Chức năng Compile dùng để biên dịch đoạn mã LTS thành các máy trạng thái tương ứng, tại đó, ta có thể kiểm tra xem thiết kế có chính xác thieo yêu cầu không? Muốn biên dịch đoạn mã tại cửa sổ của chương trình nhấn biển tượng chữ C (Compile) hoặc tại thực đơn Build chọn Compile. Hình 3.3.4: Kết quả hiển thị khi biên dịch đoạn mã LTS Sau khi chọn Compile khung nhìn Output sẽ hiện ra thông báo kết quả biện dịch, nếu đoạn mã không có lỗi, chương trình sẽ thông báo biên dịch thành công. Nếu đoạn mã có lỗi, cửa sổ sẽ thông báo có lỗi ở dòng bao nhiêu để sửa. Trên màn hình hiển thị có 3 dòng chữ bắt đầu bằng “Conpiled” điều đó có nghĩa có 3 máy trạng thái được biên dịch và không có lỗi về cú pháp. Ba máy trạng được tạo ra thành công là CAR, NOPASS, và NOPASS2. Nếu cõ lỗi về cú pháp, chương trình sẽ không biên dịch được và sẽ báo lỗi đó là lỗi ở dòng bao nhiêu để ta có thể biết và sửa. Các mô hình được tạo ra sẽ được hiển thị ở khung nhìn Draw mà được mô tả trong phần 3.3.5. 3.3.5 LTS Analiser Kết quả phân tích ví dụ trên bằng LTSA: Hình 3.3.5: LTS Analiser SingleLaneBridge Mỗi mô tả FSP được mô tả bằng một mô hình tương ứng trong LTSA. Phần bên trái là danh sách các mô hình, phần bên phải hiển thị mô hình tương ứng được chọn ở danh sách bên trái. Trên hình ta thấy một máy trạng thái với tên trạng thái ban đầu là red:CONVOY.NOPASS1. Máy trạng thái này tương ứng với đoạn mã sau trong LTS: NOPASS1 = C[1], C[i:ID] = ([i].enter -> C[i%N+1]). NOPASS2 = C[1], C[i:ID] = ([i].exit -> C[i%N+1]). ||CONVOY = ([ID]:CAR || NOPASS1 || NOPASS2). ||CARS = (red:CONVOY || blue:CONVOY). 3.3.6 LTSA Animator LTSA Animator là chức năng để điều khiển cách hành động có thể xảy ra theo như thiết kế. Để sử dụng chức nằng này ta vào thực đơn Check chọn Run và chọn DEFAULT. Cửa sổ Animator sẽ hiện ra: Hình 3.3.6: Animator SingleLandBridge Các hành động trong Animator sẽ tương ứng với các hành động trong mô hình. Hành động được chọn trong Animator sẽ điều khiển hoạt động của mô hình trong LTSA. Khi một hành động được thực thi, mỗi mô hình có hành động được thự hiện sẽ chuyển thành màu đỏ ở phần bên trái của cửa sổ LTSA. Hành động được thực thi cũng được thể hiện bằng màu đỏ trong mô hình ở phần bên phải của cửa sổ LTSA. Toàn bộ các hành động trong thiết kế sẽ được Animator ghi lại, nhờ đó LTSA có thể kiểm tra được toàn bộ các hành động có thể xảy ra trong thiết kế. Với cách kiểm tra bằng mô hình như vậy, chúng ta có thể dễ dàng kiểm tra xem thiết kế có đúng với yêu cầu bài toán đặt ra không? Bằng việc lựa chọn tất cả các hành động có thể xảy ra trong animator chúng ta đã kiểm tra được toàn bộ hoạt động của hệ thống tương tranh trong thiết kế. Qua đó chúng ta kết luận được thiết kế có hoạt động chính xác hay không. Cụ thể trong thiết kế đang được kiểm chứng này, em đã kiểm tra các hoạt động xảy ra trong thiết kế và thấy thiết kế hoạt động đúng theo yêu cầu. 3.4 Kết luận Trong chương này, chúng ta đã tìm hiểu được cách đặc tả một thiết kế bằng FSP và dùng công cụ LTSA để kiểm chứng thiết kế đó. Đối với ví dụ cụ thể mà chúng ta sử dụng để kiểm chứng, thiết kế đã đáp ứng được yêu cầu đặt ra. Chương 4: Kiểm chứng cài đặt Trong chương này chúng ta sẽ tìm hiểu cách chuyển từ mã nguồn Java thành FSP để sử dụng công cụ LTSA kiểm chứng xem chương trình có lỗi và hoạt động đúng theo thiết kế hay không? 4.1 Phương pháp để kiểm chứng cài đặt Từ trước tới nay chúng ta vẫn quen với cách phương pháp kiểm thử quen thuộc như: kiểm thử hộp trắng, kiểm thử hộp đen… Các phương pháp này có thể chỉ ra được chương trình có lỗi hay không. Tuy nhiên chúng không thể chỉ ra được chương trình liệu có còn lỗi hay không. Hệ thống tương tranh có rất nhiều luồng được xử lý cùng một lúc, có những trường hợp xung đột giữa các luồng mà các phương pháp kiểm thử trên không kiểm tra được. Chính vì vậy đòi hỏi phải có một phương pháp kiểm chứng trực quan, một phương pháp hình thức có thể thể hiện được từng hoạt động nhỏ nhất của phần mềm bằng cách đặc tả chi tiết từng câu chữ của mã nguồn, nhờ đó kiểm chứng được phần mềm một cách trọn vẹn. Khi đã có một thiết kế đúng đắn và chính xác thì việc kiểm chứng phần mềm chỉ cần đối chiếu xem chương trình đó có hoạt động chính xác theo thiết kế hay không. Cách đơn giản nhất là biên dịch chương trình đó thành chính ngôn ngữ mà chúng ta đã thiết kế. Cụ thể là chuyển chương trình thành một bộ quy trình FSP và sử dụng công cụ hỗ trợ phân tích LTSA của nó. Bằng việc kiểm tra xem bộ quy trình đó có thỏa mãn thiết kế hay không? Chúng ta có thể biết được phần mềm có thỏa mãn thiết kế? Ở chương 3, chúng ta đã nghiên cứu thiết kế bài toán “SingleLandBridge”. Mã nguồn của chương trình được viết bằng Java. Chúng ta sẽ tìm hiểu phương pháp chuyển mã nguồn Java thành FSP và thực hành chuyển mã nguồn bài toán “SingleLandBridge” thành một bộ FSP. 4.2 Cách chuyển từ mã nguồn Java sang FSP Chúng ta hãy tìm hiểu mối tương quan giữa Java và FSP để có thể chuyển từ mã nguồn Java thành FSP. Bảng 4.3.2a Những toán tử tương đương giữa FSP và Java Java FSP ++ (cộng 1) .inc -- (trừ 1) .dec = (bằng) = | (hoặc) | ! (not) ! == (so sánh bằng) == > (lớn hơn) > < (nhỏ hơn) < & (và) & Tuy nhiên trên FSP chỉ thực hiện được trên các phép toán với số nguyên. Bảng 4.3.2b: Các thành phần cơ bản khi chuyển từ Java sang FSP: ++a a.inc --a a.dec a = true a.write[true] a = false a.write[false] if(a == 0) … a.read[v:Int] -> if v = 0 then … if(a > 0) … a.read[v:Bool] -> if v > 0 then … while (!a) … WHILE = (a.read[v:Bool] -> if(!v) then… Bây giờ, chúng ta sẽ lấy một ví dụ để nghiên cứu cách chuyển từ Java sang FSP: Đây là một hàm trong mã nguồn Java của bài toán “SingleLandBridge” được lấy từ trang web[3] chính thức của cuốn sách Concurrency: State models and Java programes second edition[1]: synchronized void redExit(){ --nred; if (nred==0) notifyAll(); } Phương pháp chuyển mã nguồn Java sang FSP là chuyển lần lượt từng câu, chữ trong mã Java thành FSP. Tên hàm Java sẽ được gán nhãn trạng thái bắt đầu trong FSP. - Các phương thức trong Java sẽ là các trạng thái được gán nhãn tương ứng với tên phương thức trong Java. - Vòng lặp trong Java cũng là các trạng thái được gán nhãn tương ứng với tên vòng lặp trong Java. - Các biến trong Java thành các hành động trong FSP. Đây là FSP đặc tả mã nguồn Java trên: const N = 3 range Int = 0..N set VarAlpha = {read[Int],dec} REDEXIT = (acquire -> redExit -> nred.dec // nred-- -> nred.read[v:Int] // if (nred==0) notifyAll() -> if (v == 0) then (notifyAll -> CONTINUE) else CONTINUE ), CONTINUE = (release -> REDEXIT). 4.3 Ứng dụng để chuyển mã nguồn bài toán “SingleLandBridge” Chúng ta chuyển các hàm trong lớp SafeBridge của lớp SingleLandBridge được lấy từ trang web[3] chính thức của cuốn sách “Concurrency: State Models & Java Programs second edition[1]”, đây là mã nguồn giải quyết bài toán “SingleLandBridge” Đây là mã nguồn Java của lớp SafeBridge: class SafeBridge extends Bridge { private int nred = 0; private int nblue = 0; synchronized void redEnter() throws InterruptedException { while (nblue>0) wait(); ++nred; } synchronized void redExit(){ --nred; if (nred==0) notifyAll(); } synchronized void blueEnter() throws InterruptedException { while (nred>0) wait(); ++nblue; } synchronized void blueExit(){ --nblue; if (nblue==0) notifyAll(); } Ví dụ đặc tả phương thức redExit bằng LTS const N = 3 range Int = 0..N set VarAlpha = {read[Int],dec} REDEXIT = (acquire -> redExit -> nred.dec -> nred.read[v:Int] -> if (v == 0) then (notifyAll -> CONTINUE) else CONTINUE ), CONTINUE = (release -> REDEXIT). 4.5 Kiểm chứng cài đặt Sau khi đã chuyển xong mã nguồn thành bộ FSP, chúng ta tiến hành kiểm tra bộ FSP này. Các bước kiểm tra giống với cách kiểm tra thiết kế ở chương 3. Chúng ta tiến hành kiểm chứng mẫu phương thức redExit: Hình 4.5a: Mở tệp SafeBridge bằng công cụ LTSA Chúng ta tiến hành kiểm chứng phương thức redExit: Check safety: Hình 4.5b: Check safety phương thức redExit Phương thức không hề có lỗi và không có deadlock. Check progress: Hình 4.5c: Check prgress phương thức redExit Phương thức không hề có progess nào vi phạm. Như vậy phương thức hoàn toàn không chứa lỗi, bây giờ chúng ta sẽ tiến hành kiểm tra xem phương thức có đúng với thiết kế không. Compile: Hình 4.5d: Máy trạng thái REDEXIT Mô tả ngắn gọn ý nghĩa của mô hình: - Một xe đỏ rời cầu (redExit) thì số xe đỏ trên cầu sẽ giảm đi một (nred.dec). - Nếu không còn xe đỏ trên cầu (nred.read[0]) thì thông báo cho các xe khác biết (notifyAll). - Nếu vẫn còn xe đỏ trên cầu (nred.read[1..3]) thì xe sau lại tiếp tục rời cầu. Ta tiến hành kiểm tra máy trạng thái REDEXIT này với máy trạng thái tương ứng trong thiết kế: Hình 4.5e: Máy trạng thái REDEXIT trong thiết kế. Qua so sánh hai mô hình ta thấy mô hình trong phương thức redExit hoàn toàn thỏa mãn thiết kế. Đối với các phương thức còn lại ta tiến hành đặc tả và kiểm chứng tương tự như phương thức redExit. Sau khi kiểm chứng toàn bộ các phương thức ta sẽ có một kết quả kiểm chứng đầy đủ về cài đặt của applet này. 4.6 Kết luận Với việc biên dịch tỷ mỉ mã nguồn Java thành FSP như trên, chúng ta đã kiểm tra được một cách toàn diện chương trình cài đặt. Từng hàm trong Java được kiểm tra một cách trực quan, nhờ đó có thể tìm ra được những lỗi tiềm ẩn rất khó phát hiện cũng như những sai sót so với thiết kế. Chương 5: Kết luận Trong khóa luận, em đã tìm hiểu được những khái niệm 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ách sử dụng công cụ LTSA. Từ những kiến thức đã thu được, chúng ta có thể thực hiện kiểm chứng một phần mềm tương tranh bằng cách đặc tả thiết kế và mã nguồn của phần mềm bằng FSP rồi sử đụng công cụ LTSA để kiểm chứng. Phương pháp này cho kết quả kiểm chứng cũng như độ an toàn của phần mềm rất cao. Hiện tại, em mới chỉ ứng dụng để kiếm chứng một applet vì khi chuyển mã nguồn của phần mềm thành FSP thì phải chuyển chính xác từng câu chữ một. Tuy nhiên, với một đội ngũ kiểm thử viên đông đảo và chuyên nghiệp chúng ta hoàn toàn có thể ứng dụng kiểm chứng những phần mềm lớn hơn và có độ phức tạp cao hơn. Tài liệu tham khảo Tài liệu tiếng Anh [1] Jeff Magee and Jeff Kramer: Concurrency: State Models & Java Programs second edition, sách điện tử, 2006 [2] Dr. Richard S. Hall, concurrent programing, slide, 2001 Websites: [3] [4]