Luận văn thạc sĩ nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm

Khám phá luận văn thạc sĩ về khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm. Tìm hiểu các phương pháp và kết quả nghiên cứu.

• Tác giả: Đậu Quốc Toản
• Người hướng dẫn: Tiến Sĩ Phạm Ngọc Hùng
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Nghiên Cứu Chuyển Đổi Đặc Tả Hình Thức Trong Kiểm Chứng Phần Mềm
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• TÓM TẮT
• BẢNG TỪ VIẾT TẮT
• 1. CHƯƠNG 1: GIỚI THIỆU
• 2. CHƯƠNG 2: KIẾN THỨC CƠ BẢN
• 2.1. Labeled Transition System (LTS)
• 2.2. Các phương pháp biểu diễn LTS
• 2.2.1. Phương pháp liệt kê
• 2.2.2. FSP
• 2.3. Dẫn xuất
• 2.4. Ghép nối song song
• 2.5. LTS an toàn và thuộc tính an toàn
• 2.6. Tính thỏa mãn
• 2.7. Đặc tả ngôn ngữ FSP
• 3. CHƯƠNG 3: CÔNG CỤ KIỂM CHỨNG PHẦN MỀM DỰA TRÊN THÀNH PHẦN AGTOOL
• 4. CHƯƠNG 4: CHUYỂN ĐỔI GIỮA CÁC DẠNG BIỂU DIỄN CỦA LTS
• 4.1. Chuyển đổi FSP sang LF
• 4.2. Chuyển đổi LF sang FSP
• 4.3. Phân tích đánh giá
• 5. CHƯƠNG 5: KẾT QUẢ THỰC NGHIỆM BẰNG CÔNG CỤ GUI-AGTOOL
• 6. CHƯƠNG 6: KẾT LUẬN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu

Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là một vấn đề quan trọng nhằm đảm bảo tính đúng đắn, giảm tỉ lệ lỗi, tìm khiếm khuyết của phần mềm trước khi đưa vào sử dụng. Vấn đề này không chỉ là yếu tố quyết định thành công của các công ty phần mềm mà còn góp phần quan trọng tới sự thành công của khách hàng. Đặc biệt, trong các phần mềm nhúng/điều khiển, lỗi trong phần mềm có thể gây ra thiệt hại nghiêm trọng. Một trong những phương pháp nhằm chứng minh tính đúng đắn của chương trình là kiểm chứng mô hình. Tuy nhiên, một trong những hạn chế lớn nhất của phương pháp này là vấn đề "bùng nổ không gian trạng thái". Phương pháp kiểm chứng giả định-đảm bảo được xem là giải pháp tiềm năng để giải quyết vấn đề này cho các hệ thống dựa trên thành phần. AGTool là một công cụ hỗ trợ kiểm chứng phần mềm, cho phép người dùng sinh ra một giả thiết kiểm chứng để kiểm tra một thành phần và cả hệ thống có thỏa mãn một thuộc tính hay không.

II. Kiến thức cơ bản

Chương này trình bày các khái niệm cơ bản về Labeled Transition System (LTS) và các phương pháp biểu diễn LTS. LTS được sử dụng để đặc tả hành vi của các thành phần và thuộc tính cần kiểm chứng. Phương pháp liệt kê (LF) và FSP (Finite State Processes) là hai phương pháp chính để biểu diễn LTS. FSP được sử dụng để xây dựng mô hình các tiến trình, có thể được phân tích và kiểm tra bởi công cụ LTSA. Sự tương đương giữa hai phương pháp này cho phép chuyển đổi qua lại giữa các dạng biểu diễn, từ đó tạo điều kiện thuận lợi cho việc kiểm chứng phần mềm.

2.1 Labeled Transition System LTS

LTS là một mô hình toán học dùng để mô tả hành vi của hệ thống. Một LTS được định nghĩa bởi một bộ bốn bao gồm tập trạng thái, bảng chữ cái hành động, trạng thái khởi đầu và hàm chuyển trạng thái. LTS cho phép mô tả các hành động có thể xảy ra trong hệ thống và cách mà hệ thống chuyển từ trạng thái này sang trạng thái khác. Việc sử dụng LTS trong kiểm chứng phần mềm giúp phát hiện lỗi và đảm bảo tính đúng đắn của hệ thống.

2.2 Các phương pháp biểu diễn LTS

Có hai phương pháp chính để biểu diễn LTS: phương pháp liệt kê (LF) và FSP. Phương pháp liệt kê mô tả LTS bằng cách liệt kê tất cả các hàm chuyển trạng thái cùng với trạng thái khởi tạo. Trong khi đó, FSP cung cấp một cách tiếp cận tổng quát hơn để mô hình hóa các tiến trình. Mặc dù FSP có thể khó hiểu hơn, nhưng nó cho phép xây dựng các mô hình phức tạp hơn và có thể được phân tích bằng các công cụ kiểm chứng phần mềm như LTSA.

III. Chuyển đổi giữa các dạng biểu diễn của LTS

Chương này trình bày các phương pháp chuyển đổi giữa hai dạng biểu diễn của LTS là LF và FSP. Việc chuyển đổi này không chỉ giúp cải thiện khả năng tương tác giữa các công cụ kiểm chứng mà còn tối ưu hóa quy trình kiểm chứng phần mềm. Luận văn đề xuất một thuật toán để chuyển từ LF sang FSP và ngược lại, nhằm nâng cao hiệu quả của AGTool trong việc kiểm chứng phần mềm. Những cải tiến này sẽ giúp AGTool trở thành một công cụ hiệu quả hơn trong thực tế.

3.1 Chuyển đổi FSP sang LF

Chuyển đổi từ FSP sang LF yêu cầu một quy trình phân tích và chuyển đổi các hành động và trạng thái trong mô hình FSP thành dạng biểu diễn liệt kê. Quá trình này cần đảm bảo rằng tất cả các hành động và trạng thái đều được mô tả chính xác trong LF, từ đó tạo ra một mô hình có thể được kiểm chứng bằng AGTool. Việc thực hiện chuyển đổi này giúp tăng cường khả năng tương tác giữa AGTool và các công cụ kiểm chứng khác.

3.2 Chuyển đổi LF sang FSP

Chuyển đổi từ LF sang FSP cũng cần một quy trình tương tự, trong đó các hàm chuyển trạng thái trong LF sẽ được chuyển đổi thành các tiến trình trong FSP. Điều này không chỉ giúp tối ưu hóa quy trình kiểm chứng mà còn mở rộng khả năng sử dụng của AGTool trong các ứng dụng thực tế. Việc chuyển đổi này cũng giúp giảm thiểu lỗi trong quá trình kiểm chứng và nâng cao chất lượng phần mềm.

IV. Đánh giá thực nghiệm

Chương này trình bày kết quả thực nghiệm từ việc áp dụng các phương pháp chuyển đổi giữa LF và FSP trong AGTool. Các kết quả cho thấy rằng việc chuyển đổi này không chỉ cải thiện khả năng tương tác của AGTool mà còn nâng cao hiệu quả kiểm chứng phần mềm. Thực nghiệm cho thấy rằng AGTool có thể xử lý các mô hình phức tạp hơn và giảm thiểu thời gian kiểm chứng. Những cải tiến này mở ra hướng đi mới cho việc phát triển các công cụ kiểm chứng phần mềm trong tương lai.

V. Kết luận

Luận văn đã trình bày một cách chi tiết về khả năng chuyển đổi giữa các đặc tả hình thức trong kiểm chứng phần mềm. Các phương pháp chuyển đổi giữa LF và FSP đã được đề xuất và thực nghiệm cho thấy tính khả thi và hiệu quả của chúng. Những cải tiến này không chỉ giúp AGTool trở thành một công cụ mạnh mẽ hơn mà còn góp phần nâng cao chất lượng phần mềm trong ngành công nghiệp. Hướng phát triển trong tương lai sẽ tập trung vào việc tối ưu hóa các thuật toán chuyển đổi và mở rộng khả năng tương tác của AGTool với các công cụ kiểm chứng khác.

Nội dung chính

Tổng quan nghiên cứu

Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là một thách thức lớn, đặc biệt khi các hệ thống ngày càng phức tạp và yêu cầu tính đúng đắn cao. Theo ước tính, lỗi phần mềm có thể gây ra thiệt hại nghiêm trọng về kinh tế, chính trị và an ninh quốc gia, điển hình như sự cố Therac-25 từ năm 1985 đến 1987, được xem là tai nạn bức xạ nghiêm trọng nhất trong lịch sử y học hiện đại. Mục tiêu của luận văn là nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức trong kiểm chứng phần mềm, nhằm nâng cao hiệu quả và tính ứng dụng của công cụ kiểm chứng AGTool trong thực tế. Phạm vi nghiên cứu tập trung vào việc phát triển thuật toán chuyển đổi qua lại giữa hai kiểu biểu diễn LTS phổ biến là Listing Form (LF) và Finite State Process (FSP), đồng thời tích hợp với công cụ LTSA để tăng khả năng tương tác. Nghiên cứu được thực hiện trong bối cảnh phát triển phần mềm tại Việt Nam, với dữ liệu và công cụ được thử nghiệm trên môi trường Ubuntu. Ý nghĩa của nghiên cứu được thể hiện qua việc giảm thiểu thời gian chuẩn bị đặc tả đầu vào, tăng tính chính xác và khả năng tái sử dụng đặc tả trong kiểm chứng phần mềm hướng thành phần, góp phần nâng cao chất lượng phần mềm trong các hệ thống nhúng và điều khiển.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Luận văn dựa trên lý thuyết về Labeled Transition System (LTS), một mô hình toán học dùng để mô tả hành vi của hệ thống phần mềm dưới dạng các trạng thái và chuyển đổi giữa các trạng thái đó. Hai phương pháp biểu diễn LTS chính được nghiên cứu là:

• Listing Form (LF): Biểu diễn LTS bằng cách liệt kê tất cả các hàm chuyển trạng thái, yêu cầu chuẩn bị chi tiết và dễ gây lỗi.
• Finite State Process (FSP): Ngôn ngữ mô hình hóa tiến trình hữu hạn trạng thái, được phân tích và kiểm tra bởi công cụ LTSA, có tính tổng quát và khả năng mô tả phức tạp hơn.

Ngoài ra, luận văn áp dụng mô hình kiểm chứng giả định-đảm bảo (Assume-Guarantee Verification) nhằm giải quyết vấn đề "bùng nổ không gian trạng thái" trong kiểm chứng mô hình. Công cụ AGTool được sử dụng để sinh giả định kiểm chứng, hỗ trợ kiểm chứng từng thành phần phần mềm riêng biệt.

Các khái niệm chuyên ngành quan trọng bao gồm: ghép nối song song (parallel composition), thuộc tính an toàn (safety property), phép gán lại nhãn (relabeling) và phép ẩn (hiding) trong FSP, cùng với ngôn ngữ lập trình hàm OCaml dùng để cài đặt công cụ.

Phương pháp nghiên cứu

Nguồn dữ liệu chính là các đặc tả phần mềm dưới dạng LTS, được biểu diễn bằng LF và FSP. Phương pháp nghiên cứu bao gồm:

• Phân tích từ vựng và cú pháp của ngôn ngữ FSP sử dụng công cụ Ocamllex và Ocamlyacc để xây dựng bộ chuyển đổi.
• Thiết kế và cài đặt thuật toán chuyển đổi giữa LF và FSP, bao gồm:
  • Thuật toán chuyển đổi FSP sang LF dựa trên việc phân tích danh sách các trạng thái và hàm chuyển trạng thái.
  • Thuật toán chuyển đổi LF sang FSP bằng cách xây dựng chuỗi ký tự biểu diễn tiến trình FSP từ danh sách hàm chuyển trạng thái.
• Tích hợp các thành phần chuyển đổi vào công cụ AGTool, tạo thành GUI-AGTool với giao diện người dùng trực quan trên hệ điều hành Ubuntu.
• Thử nghiệm và đánh giá hiệu quả chuyển đổi, so sánh kết quả với công cụ LTSA để đảm bảo tính chính xác.

Quá trình nghiên cứu kéo dài trong khoảng thời gian từ năm 2014 đến 2015, với các bước phát triển, kiểm thử và hoàn thiện công cụ.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

1. Thuật toán chuyển đổi FSP sang LF được phát triển hoàn chỉnh, cho phép chuyển đổi các đặc tả FSP phức tạp thành dạng liệt kê LF. Thuật toán xử lý danh sách trạng thái và hàm chuyển trạng thái một cách hiệu quả, đảm bảo tính đầy đủ của dữ liệu đầu ra. Kết quả thử nghiệm cho thấy thuật toán có thể xử lý các mô hình với khoảng vài chục trạng thái và hàm chuyển trạng thái, phù hợp với các hệ thống phần mềm hướng thành phần.

2. Thuật toán chuyển đổi LF sang FSP cũng được xây dựng thành công, tạo ra chuỗi ký tự FSP từ danh sách hàm chuyển trạng thái và trạng thái. Tuy nhiên, kết quả FSP sinh ra ở dạng đơn giản nhất, chưa được tối ưu hóa về mặt cú pháp và cấu trúc. Việc này ảnh hưởng đến khả năng đọc hiểu và tái sử dụng đặc tả trong các công cụ khác.

3. Tích hợp thành công các thành phần chuyển đổi vào GUI-AGTool, tạo ra một công cụ có giao diện đồ họa thân thiện, hỗ trợ nhập/xuất dữ liệu FSP và LF, đồng thời hiển thị biểu đồ trực quan các thành phần phần mềm. Công cụ này đã được thử nghiệm trên môi trường Ubuntu với các mô hình kiểm chứng điển hình, cho thấy khả năng tương tác tốt với công cụ LTSA.

4. So sánh kết quả với LTSA cho thấy các đặc tả FSP được sinh ra từ LF có tính tương đương về mặt mô hình, đảm bảo tính chính xác của thuật toán chuyển đổi. Điều này khẳng định tính khả thi của phương pháp chuyển đổi trong việc hỗ trợ kiểm chứng phần mềm hướng thành phần.

Thảo luận kết quả

Nguyên nhân thành công của nghiên cứu là do việc áp dụng chặt chẽ các lý thuyết về LTS, FSP và kiểm chứng giả định-đảm bảo, kết hợp với việc sử dụng ngôn ngữ OCaml có khả năng xử lý cú pháp và từ vựng hiệu quả. So với các nghiên cứu trước đây, công trình đã mở rộng khả năng tương tác giữa AGTool và LTSA, giải quyết hạn chế về kiểu dữ liệu đầu vào và đầu ra.

Tuy nhiên, kết quả chuyển đổi LF sang FSP chưa tối ưu về mặt cú pháp, điều này có thể làm giảm tính dễ hiểu và khả năng mở rộng của đặc tả. Đây là điểm cần cải tiến trong các nghiên cứu tiếp theo. Ngoài ra, việc thử nghiệm chủ yếu trên các mô hình có kích thước vừa phải, nên cần đánh giá thêm trên các hệ thống lớn hơn để kiểm chứng khả năng mở rộng.

Dữ liệu có thể được trình bày qua các biểu đồ thể hiện số lượng trạng thái và hàm chuyển trạng thái trước và sau khi chuyển đổi, cũng như bảng so sánh thời gian xử lý và độ chính xác giữa GUI-AGTool và LTSA.

Đề xuất và khuyến nghị

1. Cải tiến thuật toán chuyển đổi LF sang FSP nhằm tối ưu hóa cú pháp và cấu trúc đặc tả FSP, giúp tăng tính dễ đọc và khả năng tái sử dụng trong các công cụ kiểm chứng khác. Thời gian thực hiện dự kiến trong 6-12 tháng, do nhóm phát triển GUI-AGTool đảm nhận.

2. Mở rộng thử nghiệm trên các hệ thống phần mềm lớn và phức tạp hơn, nhằm đánh giá khả năng mở rộng và hiệu suất của công cụ. Khuyến nghị thực hiện trong vòng 12 tháng, phối hợp với các doanh nghiệp phát triển phần mềm nhúng.

3. Phát triển thêm các tính năng hỗ trợ tự động hóa trong GUI-AGTool, như tự động phát hiện lỗi cú pháp, hỗ trợ gợi ý đặc tả và tích hợp sâu hơn với các công cụ kiểm chứng khác. Thời gian thực hiện 6 tháng, do nhóm nghiên cứu và phát triển phần mềm đảm nhiệm.

4. Đào tạo và phổ biến công cụ GUI-AGTool trong cộng đồng nghiên cứu và phát triển phần mềm, nhằm tăng cường ứng dụng thực tế và nhận phản hồi để hoàn thiện công cụ. Khuyến nghị tổ chức các hội thảo, khóa học trong vòng 1 năm tới, do các trường đại học và viện nghiên cứu phối hợp thực hiện.

Đối tượng nên tham khảo luận văn

1. Nhà nghiên cứu và sinh viên ngành Công nghệ Thông tin, đặc biệt chuyên ngành Kỹ thuật Phần mềm: Luận văn cung cấp kiến thức sâu về kiểm chứng mô hình, ngôn ngữ FSP, LTS và công cụ AGTool, hỗ trợ nghiên cứu và phát triển các phương pháp kiểm chứng phần mềm.

2. Kỹ sư phát triển phần mềm nhúng và hệ thống điều khiển: Các kỹ thuật và công cụ trong luận văn giúp đảm bảo tính đúng đắn và an toàn của phần mềm trong các hệ thống quan trọng như điều khiển máy bay, giám sát hạt nhân.

3. Nhà phát triển công cụ kiểm chứng phần mềm: Luận văn trình bày chi tiết về thuật toán chuyển đổi giữa các dạng biểu diễn LTS, giúp phát triển hoặc cải tiến các công cụ kiểm chứng hiện có, tăng khả năng tương tác và tái sử dụng đặc tả.

4. Doanh nghiệp phần mềm và tổ chức kiểm thử chất lượng phần mềm: Công cụ GUI-AGTool và phương pháp kiểm chứng giả định-đảm bảo có thể được ứng dụng để nâng cao hiệu quả kiểm thử, giảm thiểu lỗi và chi phí bảo trì phần mềm.

Câu hỏi thường gặp

1. AGTool là gì và vai trò của nó trong kiểm chứng phần mềm?
   AGTool là công cụ hỗ trợ kiểm chứng đảm bảo giả định (Assume-Guarantee Verification), giúp sinh giả định kiểm chứng cho từng thành phần phần mềm riêng biệt, giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình.

2. Tại sao cần chuyển đổi giữa LF và FSP?
   LF là dạng biểu diễn liệt kê chi tiết, dễ gây lỗi và tốn thời gian chuẩn bị, trong khi FSP là ngôn ngữ mô hình hóa phổ biến, được hỗ trợ bởi công cụ LTSA. Chuyển đổi giúp tăng khả năng tương tác và tái sử dụng đặc tả giữa các công cụ kiểm chứng.

3. Ngôn ngữ OCaml được sử dụng như thế nào trong nghiên cứu này?
   OCaml được dùng để cài đặt các thành phần chuyển đổi và GUI-AGTool nhờ tính năng lập trình hàm, khả năng xử lý cú pháp và từ vựng hiệu quả, cũng như tốc độ thực thi nhanh.

4. GUI-AGTool có những tính năng gì nổi bật?
   GUI-AGTool cung cấp giao diện đồ họa thân thiện, hỗ trợ nhập/xuất dữ liệu FSP và LF, hiển thị biểu đồ trực quan các thành phần phần mềm, đồng thời tích hợp với công cụ LTSA để kiểm chứng mô hình.

5. Những hạn chế hiện tại của công cụ và hướng phát triển tương lai?
   Hiện tại, thuật toán chuyển đổi LF sang FSP chưa tối ưu cú pháp, công cụ cần mở rộng thử nghiệm trên hệ thống lớn hơn và phát triển thêm tính năng tự động hóa. Hướng phát triển tập trung vào cải tiến thuật toán, mở rộng ứng dụng và đào tạo người dùng.

Kết luận

• Luận văn đã phát triển thành công thuật toán chuyển đổi qua lại giữa hai dạng biểu diễn LTS là LF và FSP, giải quyết hạn chế của công cụ AGTool trong việc tương tác với LTSA.
• Công cụ GUI-AGTool được cài đặt với giao diện người dùng trực quan, hỗ trợ nhập/xuất dữ liệu và hiển thị biểu đồ, tăng tính ứng dụng thực tế.
• Kết quả thử nghiệm cho thấy tính chính xác và hiệu quả của các thuật toán chuyển đổi, đồng thời mở rộng khả năng kiểm chứng phần mềm hướng thành phần.
• Các hạn chế về tối ưu hóa cú pháp và khả năng mở rộng được xác định, làm cơ sở cho các nghiên cứu tiếp theo.
• Đề xuất các giải pháp cải tiến, mở rộng thử nghiệm và đào tạo nhằm nâng cao chất lượng và ứng dụng của công cụ trong tương lai.

Để tiếp tục phát triển công cụ và ứng dụng phương pháp kiểm chứng giả định-đảm bảo, các nhà nghiên cứu và kỹ sư phần mềm được khuyến khích tham khảo và áp dụng kết quả nghiên cứu này trong các dự án thực tế.

Trích đoạn nội dung tài liệu

Chương 1. Giới thiệu cứu đặc tả hoàn chỉnh của FSP và tích hợp GUI-AGTool với công cụ LTSA. Những cải tiến này sẽ biến GUI-AGTool trở thành một công cụ hiệu quả và có tính tương tác rộng rãi hơn trong thực tế. Cấu trúc của luận văn được chia thành sáu phần.

Chương đầu tiên giới thiệu về vai trò của kiểm chứng phần mềm, công cụ hỗ trợ và bài toán cần giải quyết trong luận văn này. Tiếp theo, chương 2 trình bày các khái niệm cơ bản nhằm phục vụ luận văn. Chương này bao gồm các khái niệm về máy hữu hạn trạng thái, dẫn xuất, ghép nối song song, thuộc tính an toàn, đặc tả của ngôn ngữ FSP, ngôn ngữ lập trình hàm OCaml, Ocamllex và Ocamlyacc. Công cụ kiểm chứng phần mềm dựa thành phần AGTool được mô tả ở chương 3.

Những vấn đề còn tồn tại của công cụ kiểm chứng AGTool được nêu ra trong chương này. Các phương pháp chuyển đổi giữa các dạng biểu diễn của LTS được trình bày trong chương 4. Trong chương này đưa ra hai phương pháp chuyển đổi qua lại giữa hai cách biểu diễn của LTS là FSP và LF. Kết quả sau khi làm thực nghiệm bằng công cụ GUI-AGTool được trình bày ở chương 5.

Cuối cùng, chương 6 tóm tắt kết quả đạt được sau khi hoàn thành luận văn, những vấn đề cần khắc phục và hướng phát triển trong tương lai. 3 z Chương 2 Kiến thức cơ bản 2.1 Labeled Transition System (LTS) Trong luận văn này sử dụng LTS [11] để đặc tả hành vi của các thành phần và thuộc tính cần kiểm chứng. Giả sử Act là tập các hành động có thể quan sát được và τ là hành động đại diện cho tất cả các hành động bên trong của hệ thống, một LTS M là một bộ bốn h Q, αM, σ, q0 i. Trong đó : • Q là một tập hữu hạn các trạng thái không rỗng, • αM ⊆ Act là tập các hành động của thành phần (gọi là bảng chữ cái của M), • q0 ∈ Q là trạng thái ban đầu, và • σ ⊆ Q × (αM ∪ τ ) × Q là hàm chuyển trạng thái.

Với π là một trạng thái lỗi của hệ thống. Chúng ta ký hiệu LTS M= h{π }, Act, σ, π i. Một LTS M = h Q, αM, δ, q0 i được gọi là LTS không đơn định nếu nó có phép biến đổi τ hoặc tồn tại (q, a, q0 ), (q, a, q00 ), trong đó q0 6= q00. Ngược lại, LTS M được gọi là LTS đơn định.

LTS Input = h Q1 , αM1 , δ1 , q10 i, trong đó : • Q1 = {0, 1, 2}, • αM1 = {in, send, ack}, • σ1 = {(0, in, 1), (1, send, 2), (2, ack, 0)}, và • q10 = {0}. Kiến thức cơ bản (a) LTS Input.1: Ví dụ của LTS. LTS Input được mô tả trực quan bởi Hình 2. Khi hệ thống ở trạng thái 0 và thực hiện hành động in thì sẽ chuyển sang trạng thái 1, còn nếu hệ thống ở trạng thái 1 thực hiện hành động send thì sẽ chuyển sang trạng thái 2.

LTS Output = h Q2 , αM2 , σ2 , q20 i, trong đó : • Q2 = {0, 1, 2}, • αM2 = {send, ack, out}, • σ2 = {(0, send, 1), (1, send, 1), (1, out, 2), (2, ack, 0)}, • q20 = {0}. LTS Output được mô tả trực quan bởi Hình 2. Nếu hệ thống đang ở trạng thái 1 mà thực hiện hành động send thì vẫn giữ nguyên trạng thái 1.2 Các phương pháp biểu diễn LTS Để chuẩn bị đầu vào cho các công cụ kiểm chứng mà các thành phần được đặc tả bằng LTS, chúng ta biểu diễn LTS bằng một trong hai phương pháp sau. Kiến thức cơ bản 2.1 Phương pháp liệt kê Phương pháp liệt kê được viết tắt là LF (Listing Form) [7].

Trong phương pháp này, một LTS được biểu diễn bằng cách liệt kê tất cả các hàm chuyển trạng thái cùng với trạng thái khởi tạo.2 định nghĩa đệ quy phương pháp biểu diễn này với State đại diện cho một trạng thái của hệ thống, Action đại diện cho một hành động thuộc tập ký tự, Transition là một phép chuyển trạng thái, Transitions là một dãy tuần tự các phép chuyển trạng thái và LTS được biểu diễn bằng Transitions và kết thúc bằng trạng thái khởi tạo. State = Id Action = Id Transition = (State, Action, State) Transitions = Transition | Transition, Transitions LTS = Transitions, State.2: Phương pháp biểu diễn liệt kê của LTS.3a biểu diễn tiến trình INPUT. Tiến trình này bao gồm các trạng thái 0, 1, 2 và các hành động in, send, ack. Tiến trình INPUT được biểu diễn một cách trực trực quan bởi Hình 2.3b biểu diễn tiến trình OUTPUT.

Tiến trình này bao gồm các trạng thái 0, 1, 2 và các hành động send, out, ack. Tiến trình OUTPUT được biểu diễn một cách trực quan bởi Hình 2. (0,in,1),(1,send,2),(2,ack,0),0 (0,send,1),(1,out,2),(2,ack,0),0 (a) LF của tiến trình INPUT. (b) LF của tiến trình OUTPUT.3: Ví dụ của LF.2 FSP FSP là viết tắt của Finite State Processes (Các tiến trình hữu hạn trạng thái), là một ngôn ngữ mô hình hóa biểu diễn tương ứng với LTS.

FSP dùng để xây dựng mô hình các tiến trình, nó có thể được phân tích và kiểm tra bởi công cụ LTSA [3]. Nếu x là một hành động và P là một tiến trình thì kí hiệu ( x → P) thể hiện cho một tiến trình thực hiện hành động x và sau đó chuyển sang trạng thái P.4a biểu diễn tiến trình INPUT. Tiến trình này bao gồm các trạng thái S0, S1, S2 và các hành động in, send, ack. Tiến trình INPUT được biểu diễn một cách trực trực quan bởi Hình 2.4b biểu diễn tiến trình OUTPUT.

Tiến 6 z Chương 2. Kiến thức cơ bản trình này bao gồm các trạng thái S0, S1, S2 và các hành động send, out, ack. Tiến trình OUTPUT được biểu diễn một cách trực quan bởi Hình 2. (a) FSP của tiến trình INPUT.

(b) FSP của tiến trình OUTPUT.4: Ví dụ của FSP. Biểu diễn LTS trực quan và dễ hiểu trong khi FSP mang tính tổng quát và khó hiểu. Tuy nhiên hai biểu diễn là tương đương nhau. Tương ứng với mỗi FSP thì có một biểu diễn LTS và ngược lại.

Để biểu diễn được hết các hệ thống LTS/FSP còn có thêm nhiều từ khóa và cấu trúc khác, có thể tham khảo trong [3].3 Dẫn xuất Một dẫn xuất [12, 13] của một LTS M = h Q, αM, σ, q0 i là một chuỗi hữu hạn các hành động a1 , a2 ,. , an sao cho tồn tại một chuỗi các trạng thái q1 , q2 ,. , qn thỏa mãn điều kiện (qi−1 , ai , qi ) ∈ σ với i=1. Giả sử Σ ⊆ Act , ký hiệu σ ↑ Σ ký hiệu một dẫn xuất thu được bằng cách loại bỏ khỏi σ tất cả các hành động a mà a ∈/ Σ.

Tập tất cả các dẫn xuất của M được gọi là ngôn ngữ đoán nhận M, ký hiệu L( M ). Với LTS Input được mô tả trong Hình 2.4a thì in, in send, in send ack là các dẫn xuất. Còn in in, in send send không phải là các dẫn xuất.4 Ghép nối song song Ghép nối song song (được ký hiệu là k) là phép toán ghép nối hai thành phần phần mềm bằng cách đội bộ các hành động chung và gối đầu các hành động còn lại [11]. Giả sử M1 = h Q1 , αM1 , σ1 , q1 0 i và M2 = h Q2 , αM2 , σ2 , q2 0 i , ghép nối song song giữa M1 và M2 , ký hiệu M1 k M2 được định nghĩa như sau.

Nếu M1 = Π hoặc M2 = Π thì M1 k M2 = Π. Ngược lại, M1 k M2 = h Q, αM, σ, q0 i, trong đó : Q = Q1 × Q2 , αM = αM1 ∪ αM2 , q0 = (q1 0 , q2 0 ) và hàm σ được xác định như sau : α ∈ αM1 ∩ αM2 , ( p, α, p0 ) ∈ δ1 , (q, α, q0 ) ∈ δ2 (i ) (2. Kiến thức cơ bản kINPUT_OUPUT = (INPUTkOUTPUT). (a) FSP của INPUT||OUTPUT.

(b) LTS của INPUT||OUTPUT.5: Ghép nối song song giữa INPUT và OUTPUT.3) (( p, q), α, ( p0 , q0 )) ∈ δ Kết quả ghép nối song song của hai tiến trình INPUT trong Hình 2.4a và OUPUT trong Hình 2. Kết quả ghép nối song song được biểu diễn trực quan bởi LTS trong Hình 2. Các trạng thái send, ack được đồng bộ hóa, còn các trạng thái còn lại xen kẽ nhau. Các trạng thái mà không dẫn tới khi xuất phát từ trạng thái khởi tạo (0, 0) sẽ bị loại bỏ.5 LTS an toàn và thuộc tính an toàn LTS an toàn là một LTS hữu hạn không chứa bất kỳ một trạng thái lỗi π nào.

Thuộc tính an toàn là thuộc tính đảm bảo không lỗi xảy ra trong quá trình thực hiện của hệ thống. Một thuộc tính an toàn được biểu diễn như là một LTS an toàn p [3]. Thuộc tính an toàn Sa f etyProperty của một hệ thống được minh họa ở Hình 2. Thuộc tính này đảm bảo rằng khi hệ thống thực thi phải luôn đảm bảo các hành động in và out phải được thực hiện đúng thứ tự in→out→in→out.

Khi hệ thống đang ở trạng thái 0 và thực hiện hành động out thì hệ thống sẽ dẫn tới trạng thái -1. Trạng thái -1 được kí hiệu là trạng thái lỗi của hệ thống. Kiến thức cơ bản Hình 2.6: Biểu diễn LTS của thuộc tính an toàn Safety Property.6 Tính thỏa mãn Cho một LTS M, ta nói M thoả mãn thuộc tính p, ký hiệu M |= p, nếu và chỉ nếu : ∀σ ∈ L( M) : (σ ↑ αp) ∈ L( p). Để kiểm chứng một thành phần M thoả mãn một thuộc tính p, khi đó cả M và perr phải được biểu diễn dưới dạng của LTS an toàn (Safety LTS), sau đó thực hiện phép toán ghép nối song song M k perr.

Nếu LTS thu được sau phép ghép nối tồn tại một dẫn xuất có thể tới trạng thái π, khi đó ta nói thành phần M vi phạm thuộc tính p. Ngược lại, M thoả mãn thuộc tính p [3].7 Đặc tả ngôn ngữ FSP Cú pháp của ngôn ngữ FSP được đặc tả bằng văn phạm phi ngữ cảnh, gồm có một tập các luật sinh [3]. Mỗi luật sinh được định nghĩa bằng một kí hiệu không kết thúc ở phía bên trái và một hoặc nhiều các kí hiệu kết thúc hoặc không kết thúc ở phía bên phải. Các kí hiệu không kết thúc được thể hiện bằng kiểu in nghiêng, các kí hiệu kết thúc được thể hiện bằng kiểu in đậm.

Các định nghĩa của một kí hiệu không kết thúc được theo sau bởi dấu hai chấm.