- 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. - 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.. - 17Chương 3: Kiểm chứng thiết kế. - 173.1 Đặc tả thiết kế bằng FSP. - Kiểm chứng thiết kế bằng LTSA. - 10Hình 2.3.1c: Tiến trình tuần tự BOMP. - 11Hình 2.3.1e : Sự tổng hợp song song hai tiến trình tuần tự.. - 12Hình 2.3.1a: Máy trạng thái PHIN. - 40Hình 4.5e: Máy trạng thái REDEXIT trong thiết kế.. - Máy hữu hạn trạng thái LTS (Labelled Transition System). - 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. - 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.. - 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?. - 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ế. - 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. - 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. - 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ự. - 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]. - 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]. - Trong đó: Maybay là một tiến trình. - 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. - 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. - 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. - 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].. - 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. - 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]. - 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. - 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:. - Tiến trình tuần tự BOMP. - Nếu chúng ta định nghĩa tiến trình SKIP = END then P. - Ví dụ tiến trình P123 và 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 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ự.:. - Sự tổng hợp song song hai tiến trình tuần tự.. - Hình 2.3.1a: Máy trạng thái PHIN. - 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. - 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. - 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. - Đ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. - 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. - 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. - 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. - 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. - 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. - 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. - Ta có định nghĩa tiến trình RED và thuộc tính ONEWAY:. - Ta có định nghĩa tiến trình cầu: BRIDGE = BRIDGE[0][0. - 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ổ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. - 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.. - 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. - 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.. - 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.. - 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?. - 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ế. - 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?. - 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ế. - 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”. - 4.5 Kiểm chứng cài đặt. - Các bước kiểm tra giống với cách kiểm tra thiết kế ở chương 3. - 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. - Hình 4.5d: Máy trạng thái REDEXIT. - 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ế. - 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ế.. - 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