Luận Văn Thạc Sĩ Về Phân Tích, Thiết Kế và Cài Đặt Hệ Thời Gian Thực Kiểm Chứng

Luận văn thạc sĩ phân tích thiết kế và cài đặt kiểm chứng hệ thời gian thực, cung cấp kiến thức chuyên sâu và ứng dụng thực tiễn trong lĩnh vực công nghệ.

• Tác giả: Phạm Văn Tuấn
• Người hướng dẫn: TS. Phạm Hồng Thái
• 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: Phân Tích, Thiết Kế Và Cài Đặt Kiểm Chứng Một Hệ Thời Gian Thực
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2014
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• MỤC LỤC
• DANH MỤC CÁC HÌNH
• DANH MỤC CÁC BẢNG
• DANH MỤC TỪ VIẾT TẮT
• 1. MỞ ĐẦU
• 2. CHƯƠNG 1: HỆ THỜI GIAN THỰC VÀ BÀI TOÁN KIỂM TRA TÍNH ĐÚNG ĐẮN CỦA HỆ THỜI GIAN THỰC
• 1.1. Hệ thời gian thực
• 1.2. Phân loại hệ thời gian thực
• 1.3. Đặc điểm của hệ thời gian thực
• 1.4. Đặc tả thiết kế và yêu cầu của hệ thống
• 1.5. Kiểm tra tính đúng đắn của hệ thống
• 3. CHƯƠNG 2: CÁC CÔNG CỤ ĐẶC TẢ
• 2.1. Ôtômat thời gian
• 4. CHƯƠNG 3: PHÂN TÍCH, THIẾT KẾ BỘ CÔNG CỤ KIỂM CHỨNG MÔ HÌNH
• 5. CHƯƠNG 4: KẾT QUẢ THỰC HIỆN CHƯƠNG TRÌNH
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu về hệ thời gian thực

Hệ thời gian thực là một khái niệm quan trọng trong lĩnh vực công nghệ thông tin, đặc biệt là trong thiết kế và phát triển phần mềm. Hệ thời gian thực được định nghĩa là những hệ thống mà tính đúng đắn của chúng không chỉ phụ thuộc vào kết quả lôgic mà còn vào thời điểm mà các kết quả đó được đưa ra. Điều này có nghĩa là, trong một số ứng dụng, việc phản ứng kịp thời với các sự kiện là rất quan trọng. Các hệ thống này thường được phân loại thành hai loại chính: hệ thời gian thực cứng và hệ thời gian thực mềm. Hệ thời gian thực cứng yêu cầu phản ứng chính xác trong một khoảng thời gian nhất định, trong khi hệ thời gian thực mềm cho phép một mức độ sai lệch nhất định mà không gây ra hậu quả nghiêm trọng. Việc hiểu rõ về hệ thời gian thực là cần thiết để phát triển các ứng dụng an toàn và hiệu quả.

1.1. Khái niệm và phân loại hệ thời gian thực

Khái niệm về hệ thời gian thực bao gồm các hệ thống mà trong đó thời gian phản ứng là yếu tố quyết định đến sự thành công hay thất bại của hệ thống. Hệ thời gian thực cứng yêu cầu các phản ứng phải diễn ra trong thời gian quy định, ví dụ như trong các hệ thống điều khiển máy bay, nơi mà sự chậm trễ có thể dẫn đến thảm họa. Ngược lại, hệ thời gian thực mềm có thể chấp nhận một số sai lệch về thời gian, như trong các ứng dụng giải trí hoặc truyền thông. Việc phân loại này giúp xác định các yêu cầu thiết kế và kiểm tra cho từng loại hệ thống, từ đó đảm bảo tính chính xác và độ tin cậy của chúng.

II. Kiểm tra tính đúng đắn của hệ thống

Kiểm tra tính đúng đắn của hệ thống là một bước quan trọng trong quá trình phát triển hệ thời gian thực. Có nhiều phương pháp để thực hiện việc này, trong đó nổi bật là kiểm chứng mô hình. Phương pháp này cho phép kiểm tra một mô hình trạng thái hữu hạn và xác định xem nó có thỏa mãn các tính chất lôgic đã định nghĩa hay không. Kiểm chứng mô hình giúp phát hiện lỗi trong thiết kế và đảm bảo rằng hệ thống hoạt động đúng như mong đợi. Một trong những ưu điểm của phương pháp này là khả năng tự động hóa, giúp tiết kiệm thời gian và công sức trong quá trình kiểm tra. Tuy nhiên, phương pháp này cũng gặp phải vấn đề bùng nổ không gian trạng thái, đặc biệt là trong các hệ thống lớn, điều này đòi hỏi các kỹ thuật tối ưu hóa để giảm thiểu số lượng trạng thái cần kiểm tra.

2.1. Phương pháp kiểm chứng mô hình

Phương pháp kiểm chứng mô hình được phát triển từ những năm 1980 và đã trở thành một công cụ quan trọng trong việc đảm bảo tính đúng đắn của hệ thời gian thực. Kỹ thuật này cho phép kiểm tra tất cả các trạng thái của hệ thống để xác định xem chúng có thỏa mãn các yêu cầu đã được định nghĩa hay không. Một trong những công cụ nổi bật trong lĩnh vực này là HyTech, cho phép kiểm tra các hệ thống thời gian thực một cách hiệu quả. Tuy nhiên, việc áp dụng phương pháp này cho các hệ thống lớn vẫn là một thách thức lớn do sự bùng nổ không gian trạng thái. Do đó, việc phát triển các kỹ thuật mới để tối ưu hóa quá trình kiểm chứng là rất cần thiết.

III. Thiết kế công cụ kiểm chứng

Thiết kế một công cụ kiểm chứng cho hệ thời gian thực là một nhiệm vụ phức tạp, đòi hỏi sự kết hợp giữa lý thuyết và thực tiễn. Công cụ này cần phải có khả năng mô hình hóa các đặc điểm của hệ thống và thực hiện kiểm chứng một cách hiệu quả. Việc sử dụng ô tômat thời gian và các công thức lôgic như bất biến khoảng tuyến tính (LDI) là những phương pháp phổ biến trong thiết kế công cụ kiểm chứng. Công cụ này không chỉ giúp phát hiện lỗi mà còn cung cấp thông tin chi tiết về cách thức hoạt động của hệ thống, từ đó hỗ trợ các nhà phát triển trong việc tối ưu hóa thiết kế và cải thiện hiệu suất của hệ thống.

3.1. Các thành phần của công cụ kiểm chứng

Công cụ kiểm chứng cho hệ thời gian thực thường bao gồm nhiều thành phần khác nhau, từ mô hình hóa đến kiểm tra. Các thành phần chính bao gồm ô tômat thời gian, các ràng buộc thời gian và các thuật toán kiểm chứng. Ô tômat thời gian cho phép mô hình hóa các trạng thái và chuyển tiếp của hệ thống, trong khi các ràng buộc thời gian xác định các điều kiện cần thiết để chuyển đổi giữa các trạng thái. Các thuật toán kiểm chứng sẽ duyệt qua không gian trạng thái để xác định xem các yêu cầu đã được thỏa mãn hay chưa. Việc thiết kế một công cụ kiểm chứng hiệu quả đòi hỏi sự hiểu biết sâu sắc về cả lý thuyết và thực tiễn trong lĩnh vực này.

IV. Kết quả thực hiện chương trình

Kết quả thực hiện chương trình kiểm chứng cho hệ thời gian thực cho thấy tính khả thi và hiệu quả của công cụ đã được thiết kế. Các bài kiểm tra được thực hiện trên nhiều mô hình khác nhau, bao gồm cả bài toán bếp ga, cho thấy rằng công cụ có khả năng phát hiện lỗi và đảm bảo tính đúng đắn của hệ thống. Đánh giá về bộ công cụ kiểm chứng cho thấy rằng nó không chỉ giúp phát hiện lỗi mà còn cung cấp thông tin hữu ích cho việc tối ưu hóa thiết kế. Hướng cải tiến chương trình cũng được đề xuất, nhằm nâng cao hiệu suất và khả năng mở rộng của công cụ trong tương lai.

4.1. Đánh giá và cải tiến

Đánh giá về bộ công cụ kiểm chứng cho thấy rằng nó đã đáp ứng được các yêu cầu đặt ra trong quá trình phát triển hệ thời gian thực. Tuy nhiên, vẫn còn nhiều điểm cần cải tiến, đặc biệt là trong việc xử lý các hệ thống lớn. Việc tối ưu hóa thuật toán kiểm chứng và cải thiện giao diện người dùng là những hướng đi quan trọng để nâng cao hiệu quả của công cụ. Ngoài ra, việc tích hợp thêm các tính năng mới như hỗ trợ cho các loại mô hình khác cũng sẽ giúp công cụ trở nên linh hoạt và hữu ích hơn trong thực tiễn.

Nội dung chính

Tổng quan nghiên cứu

Hệ thống thời gian thực ngày càng trở nên phổ biến và quan trọng trong nhiều lĩnh vực, từ các thiết bị điện tử gia dụng như tivi, máy giặt đến các hệ thống phức tạp như máy bay, vệ tinh nhân tạo. Theo ước tính, chi phí phát triển phần mềm và phần cứng cho hệ thống thời gian thực thường cao hơn nhiều so với các hệ thống ứng dụng thông thường do yêu cầu tính chính xác và độ tin cậy cực kỳ nghiêm ngặt. Một lỗi nhỏ trong hệ thống thời gian thực có thể gây ra hậu quả nghiêm trọng, ảnh hưởng đến an toàn và hiệu quả vận hành. Do đó, việc phân tích, thiết kế và kiểm chứng tính đúng đắn của hệ thống trước khi triển khai là rất cần thiết.

Mục tiêu nghiên cứu của luận văn là phân tích, thiết kế và cài đặt một công cụ kiểm chứng mô hình cho hệ thống thời gian thực, đặc biệt tập trung vào các hệ thống được đặc tả bằng ôtômat thời gian và các tính chất thời gian được biểu diễn bằng công thức bất biến khoảng tuyến tính (LDI). Phạm vi nghiên cứu tập trung vào các hệ thống thời gian thực được mô hình hóa trong khoảng thời gian thực R+ với các ràng buộc đồng hồ hữu hạn, áp dụng cho các bài toán thực tế như hệ thống bếp ga tự động.

Ý nghĩa của nghiên cứu được thể hiện qua việc cung cấp một công cụ kiểm chứng tự động, giúp phát hiện lỗi thiết kế và đảm bảo tính đúng đắn của hệ thống thời gian thực, từ đó giảm thiểu rủi ro và chi phí phát triển. Các chỉ số hiệu quả bao gồm độ chính xác kiểm chứng, khả năng xử lý các mô hình phức tạp và thời gian thực thi kiểm chứng.

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 hai lý thuyết chính:

1. Ôtômat thời gian (Timed Automaton - TA): Là mô hình toán học dùng để đặc tả các hệ thống thời gian thực, bao gồm tập vị trí, tập đồng hồ, các ràng buộc đồng hồ và các phép chuyển trạng thái có điều kiện về thời gian. Ôtômat thời gian cho phép mô hình hóa chính xác các hành vi đồng thời và các giới hạn thời gian trong hệ thống.

2. Công thức bất biến khoảng tuyến tính (Linear Duration Invariant - LDI): Là một lớp tính chất trong lôgic khoảng (Duration Calculus), biểu diễn các tính chất thời gian liên quan đến tổng thời gian xuất hiện của các trạng thái trong một khoảng thời gian quan sát. LDI cho phép mô tả các yêu cầu an toàn và hiệu năng của hệ thống thời gian thực một cách chính xác.

Các khái niệm chính bao gồm: đồng hồ (clocks), ràng buộc đồng hồ, ôtômat hợp song song, đồ thị vùng (region graph), đồ thị miền (zone graph), và thuật toán kiểm chứng mô hình dựa trên duyệt đồ thị trọng số.

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

Nguồn dữ liệu nghiên cứu bao gồm các mô hình ôtômat thời gian được xây dựng từ các bài toán thực tế như bài toán bếp ga và các ví dụ minh họa. Phương pháp phân tích sử dụng kỹ thuật kiểm chứng mô hình (Model Checking) để tự động kiểm tra tính đúng đắn của hệ thống so với các tính chất LDI.

Quy trình nghiên cứu gồm các bước:

• Xây dựng ôtômat hợp song song từ các ôtômat thành phần bằng thuật toán duyệt đồ thị theo chiều sâu.
• Chuyển đổi ôtômat hợp song song thành đồ thị vùng đạt được nguyên (integral reachability graph) sử dụng kỹ thuật ε-nguyên hóa.
• Rời rạc hóa đồ thị vùng thành đồ thị trọng số phục vụ kiểm chứng LDI.
• Áp dụng thuật toán vét cạn duyệt đồ thị trọng số để kiểm chứng tính thỏa mãn công thức LDI.
• Cài đặt bộ công cụ kiểm chứng trên nền web sử dụng ngôn ngữ PHP, áp dụng mô hình MVC để quản lý mã nguồn và giao diện.

Cỡ mẫu nghiên cứu bao gồm các mô hình ôtômat thời gian với số lượng đỉnh và cạnh khác nhau, trong đó bài toán bếp ga có 2 đỉnh và 2 phép chuyển trạng thái. Phương pháp chọn mẫu dựa trên các bài toán điển hình trong lĩnh vực hệ thống thời gian thực. Timeline nghiên cứu kéo dài trong năm 2014, bao gồm giai đoạn phân tích, thiết kế, cài đặt và đánh giá công cụ.

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

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

1. Hiệu quả xây dựng ôtômat hợp song song: Thuật toán xây dựng ôtômat hợp song song từ các ôtômat thành phần hoạt động hiệu quả, cho phép mô hình hóa các hệ thống phức tạp với nhiều thành phần đồng thời. Ví dụ, với hai ôtômat thành phần, thuật toán duyệt đồ thị theo chiều sâu đã tạo ra ôtômat hợp song song đầy đủ các trạng thái và phép chuyển.

2. Kiểm chứng công thức LDI trên mô hình ví dụ: Với bài toán minh họa, công cụ kiểm chứng đã xác nhận ôtômat thỏa mãn công thức LDI với các hệ số A=0, B=∞, M=5, trong đó hệ số LDI tại các đỉnh lần lượt là 1 và -1. Thời gian thực thi kiểm chứng nằm trong khoảng vài giây, phù hợp với yêu cầu thực tế.

3. Kiểm chứng hệ thống bếp ga: Công cụ đã kiểm chứng thành công tính an toàn của hệ thống bếp ga với công thức LDI đặc tả yêu cầu tỉ lệ thời gian rò gas không vượt quá 1/20 trong khoảng thời gian quan sát không ngắn hơn 60 giây. Kết quả cho thấy hệ thống thỏa mãn yêu cầu với thời gian kiểm chứng hiệu quả.

4. Độ phức tạp thuật toán: Thuật toán kiểm chứng LDI có độ phức tạp hàm mũ trong trường hợp xấu nhất do phải duyệt tất cả các chu trình trong đồ thị trọng số. Tuy nhiên, việc sử dụng kỹ thuật duyệt đồ thị vùng đạt được nguyên và rời rạc hóa giúp giảm thiểu đáng kể không gian trạng thái so với phương pháp truyền thống.

Thảo luận kết quả

Nguyên nhân chính của hiệu quả kiểm chứng là do việc áp dụng mô hình ôtômat thời gian kết hợp với công thức LDI cho phép mô tả chính xác và kiểm tra tự động các tính chất thời gian phức tạp. So với các công cụ kiểm chứng mô hình thời gian thực hiện có như UPPAAL, bộ công cụ này có ưu thế trong việc xử lý các tính chất thời khoảng thay vì chỉ tính chất thời điểm.

Kết quả kiểm chứng trên bài toán bếp ga minh chứng cho tính ứng dụng thực tiễn của công cụ, giúp phát hiện và ngăn ngừa các lỗi tiềm ẩn trong thiết kế hệ thống. Việc trình bày dữ liệu qua các biểu đồ ôtômat, đồ thị vùng và đồ thị trọng số giúp người dùng dễ dàng theo dõi quá trình kiểm chứng và xác định vị trí lỗi nếu có.

Tuy nhiên, độ phức tạp thuật toán vẫn là thách thức lớn, đặc biệt với các hệ thống có số lượng trạng thái và đồng hồ lớn. Việc đề xuất các giải pháp xử lý song song và tối ưu thuật toán là cần thiết để nâng cao hiệu suất kiểm chứng.

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

1. Triển khai xử lý song song: Áp dụng kỹ thuật xử lý song song cho thuật toán duyệt đồ thị trọng số LDI nhằm giảm thời gian kiểm chứng. Cụ thể, thực hiện duyệt đồng thời từ nhiều đỉnh xuất phát, tổng hợp kết quả để rút ngắn thời gian xử lý trung bình khoảng n lần với n là số đỉnh.

2. Sử dụng kỹ thuật gửi yêu cầu không đồng bộ (Ajax): Phân chia công việc kiểm chứng thành các yêu cầu nhỏ gửi không đồng bộ về server, tận dụng khả năng xử lý đa luồng của web server để tăng tốc độ kiểm chứng.

3. Tối ưu thuật toán vét cạn: Nghiên cứu và áp dụng các thuật toán heuristic hoặc cắt tỉa để giảm số lượng chu trình cần duyệt, từ đó giảm độ phức tạp hàm mũ của thuật toán kiểm chứng LDI.

4. Mở rộng phạm vi áp dụng: Phát triển công cụ để hỗ trợ thêm các loại lôgic thời gian khác như LTL, TCTL nhằm tăng tính linh hoạt và khả năng ứng dụng trong nhiều lĩnh vực hệ thống thời gian thực khác nhau.

5. Cải tiến giao diện người dùng: Thiết kế giao diện trực quan hơn, hỗ trợ trực quan hóa đồ thị và kết quả kiểm chứng, giúp người dùng dễ dàng thao tác và phân tích kết quả.

Các giải pháp trên nên được thực hiện trong vòng 1-2 năm tiếp theo, phối hợp với việc đánh giá hiệu quả trên các bài toán thực tế đa dạng.

Đố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, Kỹ thuật Phần mềm: Luận văn cung cấp kiến thức chuyên sâu về mô hình hóa và kiểm chứng hệ thống thời gian thực, giúp nâng cao hiểu biết và kỹ năng nghiên cứu.

2. Kỹ sư phát triển phần mềm hệ thống nhúng: Công cụ và phương pháp trong luận văn hỗ trợ kiểm tra tính đúng đắn của các hệ thống nhúng thời gian thực, giảm thiểu lỗi và tăng độ tin cậy sản phẩm.

3. Chuyên gia kiểm thử phần mềm: Phương pháp kiểm chứng mô hình tự động giúp phát hiện lỗi thiết kế sớm, tiết kiệm thời gian và chi phí kiểm thử thủ công.

4. Nhà quản lý dự án phát triển hệ thống thời gian thực: Hiểu rõ về các kỹ thuật kiểm chứng giúp quản lý rủi ro, đảm bảo chất lượng và tiến độ dự án.

Mỗi nhóm đối tượng có thể áp dụng các kiến thức và công cụ từ luận văn để cải thiện quy trình phát triển, kiểm thử và vận hành hệ thống thời gian thực trong thực tế.

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

1. Ôtômat thời gian là gì và tại sao nó quan trọng trong hệ thống thời gian thực?
   Ôtômat thời gian là mô hình toán học dùng để mô tả hành vi của hệ thống thời gian thực với các ràng buộc về thời gian. Nó giúp phân tích và kiểm chứng tính đúng đắn của hệ thống, đảm bảo hệ thống đáp ứng kịp thời các sự kiện môi trường.

2. Công thức bất biến khoảng tuyến tính (LDI) dùng để làm gì?
   LDI biểu diễn các tính chất liên quan đến tổng thời gian xuất hiện của các trạng thái trong một khoảng thời gian quan sát, giúp đặc tả các yêu cầu an toàn và hiệu năng của hệ thống thời gian thực một cách chính xác.

3. Phương pháp kiểm chứng mô hình có ưu điểm gì so với chứng minh toán học?
   Kiểm chứng mô hình là phương pháp tự động, dễ áp dụng cho các bài toán cụ thể, có khả năng phát hiện lỗi và chỉ ra vị trí lỗi trong thiết kế, trong khi chứng minh toán học đòi hỏi kiến thức chuyên sâu và khó áp dụng cho hệ thống phức tạp.

4. Bộ công cụ kiểm chứng được cài đặt như thế nào?
   Bộ công cụ được cài đặt trên nền web sử dụng ngôn ngữ PHP, mô hình MVC, cho phép người dùng nhập mô hình ôtômat và công thức LDI, thực hiện kiểm chứng tự động và hiển thị kết quả cùng các đồ thị minh họa.

5. Làm thế nào để giảm độ phức tạp của thuật toán kiểm chứng LDI?
   Có thể áp dụng xử lý song song, kỹ thuật gửi yêu cầu không đồng bộ, tối ưu thuật toán vét cạn bằng heuristic hoặc cắt tỉa chu trình để giảm số lượng trạng thái và đường đi cần duyệt, từ đó giảm thời gian kiểm chứng.

Kết luận

• Luận văn đã phân tích, thiết kế và cài đặt thành công bộ công cụ kiểm chứng mô hình cho hệ thống thời gian thực dựa trên ôtômat thời gian và công thức LDI.
• Công cụ cho phép kiểm chứng tự động các tính chất thời khoảng phức tạp, đáp ứng yêu cầu thực tế như bài toán bếp ga.
• Thuật toán kiểm chứng có độ phức tạp cao nhưng được tối ưu bằng kỹ thuật duyệt đồ thị vùng và rời rạc hóa trọng số.
• Đề xuất các giải pháp xử lý song song và tối ưu thuật toán nhằm nâng cao hiệu suất kiểm chứng trong tương lai.
• Khuyến khích áp dụng công cụ và phương pháp nghiên cứu trong phát triển và kiểm thử hệ thống thời gian thực để đảm bảo tính đúng đắn và an toàn.

Tiếp theo, cần triển khai các giải pháp cải tiến thuật toán và mở rộng phạm vi ứng dụng công cụ, đồng thời phát triển giao diện người dùng thân thiện hơn. Độc giả và nhà nghiên cứu được mời truy cập và sử dụng bộ công cụ kiểm chứng để đánh giá và đóng góp ý kiến nhằm hoàn thiện hơn nữa công trình nghiên cứu.

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

Chương 1 giới thiệu khái quát về hệ thời gian thực và bài toán kiểm tra tính đúng đắn của hệ. Chương 2 trình bày về các công cụ đặc tả hệ thống và bài toán bếp ga. Trong chương 3, luận văn mô tả bản thiết kế và xây dựng một công cụ cho phép kiểm chứng tính đúng đắn của các hệ được đặc tả dưới dạng công thức tính chất khoảng tuyến tính hoặc công thức bất biến khoảng tuyến tính của lôgic khoảng. Đây cũng là mục tiêu và là kết quả chính của luận văn.

z 2 Chương 4 mô tả các kết quả chạy chương trình trên các ví dụ và hệ bếp ga. Phần kết luận, luận văn tóm tắt lại nội dung của đề tài, những kết quả đạt được, các điểm hạn chế và hướng nghiên cứu tiếp tục trong tương lai. Về mã nguồn của chương trình được chúng tôi trình bày trong phần phụ lục. HỆ THỜI GIAN THỰC VÀ BÀI TOÁN KIỂM TRA TÍNH ĐÚNG ĐẮN CỦA HỆ THỜI GIAN THỰC Mục tiêu của chương này là giới thiệu để người đọc hiểu được một cách tổng quan về hệ thời gian thực và về bài toán kiểm tra tính đúng đắn của hệ tức kiểm tra sự thỏa mãn của thiết kế so với yêu cầu của hệ thống.

Hệ thời gian thực 1. Khái niệm về hệ thời gian thực Trong đời sống hàng ngày chúng ta đã sử dụng và tiếp xúc với rất nhiều hệ thống được gọi là hệ thời gian thực, ví dụ từ máy tính cá nhân đơn giản, các hệ thống điều khiển tay máy, điều khiển động cơ, hệ thống tín hiệu đèn giao thông cho đến các hệ thống tinh vi, phức tạp được vận hành trong các nhà máy và trong vũ trụ. Đặc trưng của hệ là tính tương tác với môi trường: khi nhận được các sự kiện phát sinh từ môi trường xung quanh, chúng thực hiện các xử lý để sản sinh ra các tín hiệu điều khiển gửi đến các thiết bị tác động để tạo ra các hoạt động nhằm đáp ứng yêu cầu, đòi hỏi của môi trường. Dạng hệ thời gian thực thứ hai rất phổ biến là các hệ thời gian thực nhúng (Embedded Real Time System), là hệ dùng để điều khiển các phần cứng chuyên dụng mà trong nó có cài đặt hệ thống tính toán.

Ví dụ, hệ vi xử lý dùng để điều khiển hỗn hợp nhiên liệu/khí trong các bộ chế hoà khí của ô tô là một hệ nhúng. Như vậy, một hệ thời gian thực là một hệ thống mà sự hoạt động tin cậy và hiệu quả không chỉ phụ thuộc vào sự chính xác của kết quả, mà còn phụ thuộc vào thời điểm đưa ra kết quả. Hệ thống sẽ là thất bại mỗi khi các yêu cầu về thời gian không được thoả mãn. Tóm lại, tính thời gian thực ở đây có thể hiểu là khả năng đáp ứng kịp thời và chính xác [1].1 mô tả mức độ đáp ứng thời gian theo bốn yêu cầu khác nhau.

z 4 Sự kiện Phản ứng Sự kiện Phản ứng T T ts tp-1 tp-2 Thời gian ts tp Thời gian a) Chính xác tại t = tp b) Trong khoảng. tp-1 ≤ t ≤ tp-2 Sự kiện Phản ứng Sự kiện Phản ứng T T ts tp Thời gian ts tp Thời gian c) Chậm nhất là. t ≤ tp d) Sớm nhất là .1: Các mức đáp ứng sự kiện về mặt thời gian Trên hình 1.1 (a) sự kiện xảy ra tại thời điểm ts, hệ thống mất khoảng thời gian T để nhận biết có sự kiện kích ứng và xử lý tức thời ngay sau đó tại thời điểm tp.1 (c) sự kiện xảy ra tại thời điểm ts hệ thống mất khoảng thời gian T để nhận biết có sự kiện kích ứng và yêu cầu phải xử lý xong trước thời điểm tp.1 (d) sự kiện xảy ra tại thời điểm ts hệ thống mất khoảng thời gian T để nhận biết có sự kiện kích ứng và yêu cầu phải được xử lý từ thời điểm tp không giới hạn thời điểm hoàn thành. Do các tính chất của hệ thời gian thực khác với các phần mềm khác là khả năng đáp ứng của nó đối với các sự kiện môi trường trong một khoảng thời gian nhất định (thường là khoảng thời gian ngắn) nên nó được định nghĩa như sau: Một hệ thời gian thực là một hệ thống mà trong đó tính đúng đắn của nó không chỉ phụ thuộc vào các kết quả lôgic được tạo ra mà còn phụ thuộc vào thời điểm mà tại đó các kết quả được đưa ra [6].

Nhiều thay đổi của các sự kiện trong thế giới thực thường xảy ra rất nhanh, mỗi hệ thống thời gian thực phải thực hiện việc xử lý và đưa ra kết quả trong một khoảng thời gian xác định hay thời điểm kết thúc (deadline). Khoảng thời gian này được xác định từ thời điểm bắt đầu và thời điểm hoàn tất công việc. Trong thực tế, nhiều yếu tố kích thích xảy ra trong khoảng thời gian rất ngắn, ví dụ vào khoảng vài mili giây, và khi đó thời gian mà hệ thống cần đáp ứng lại các yếu tố kích thích thường vào khoảng dưới 1 giây mới đảm bảo được yêu cầu mong muốn. Khoảng thời gian này bao gồm: thời gian tiếp nhận kích thích, thời gian xử lý thông tin và thời gian đáp ứng kích thích.

Phân loại hệ thời gian thực Hệ thời gian thực thường được chia thành hai loại, hệ thời gian thực cứng (Hard real time system) và hệ thời gian thực mềm (Soft real time system). Hệ thời gian thực cứng: Trong một số hệ thống, sự đáp ứng vi phạm giới hạn về thời gian cho phép có thể gây ra những ảnh hưởng trầm trọng, như đến sinh mạng con người. Trong trường hợp này, yêu cầu đáp ứng về mặt thời gian của hệ thống là rất khắt khe. Chính vì vậy, người ta đưa ra định nghĩa về hệ thời gian thực cứng như sau: Một hệ thời gian thực cứng là một hệ thống mà hoạt động không đúng đắn của nó sẽ để lại hậu quả nghiêm trọng.

Do đó hệ thời gian thực cứng buộc phải đưa ra các kết quả chính xác trong khoảng thời gian đã xác định trước. Hệ thời gian thực mềm: Ngược lại với hệ thời gian thực cứng là hệ thời gian thực mềm. Kết quả đưa ra của một hệ thống chấp nhận một sai số nhất định cả về giá trị và thời gian so với yêu cầu dự kiến. Tuy nhiên, nếu sự sai lệch này không được đảm bảo nó cũng không gây ra điều gì nghiêm trọng.

Trong trường hợp này, người ta nói rằng hệ thống có ràng buộc định thời gian mềm. Hệ thời gian thực mềm có định nghĩa như sau: Một hệ thời gian thực mềm là một hệ thống mà trong đó các hoạt động của nó được phép hoàn thành trong một sai số cho phép mà không gây hậu quả nghiêm trọng, tức là sự đáp ứng của hệ thống có thể vượt ra ngoài một giới hạn cho phép mà vẫn có thể chấp nhận được. Ví dụ về hệ thống này bao gồm những hệ thống thực hiện tương tác trực tuyến, những bộ chuyển mạch điện thoại, hay các trò chơi điện tử. Sự phân biệt giữa khoảng thời gian bắt buộc cứng hay mềm của hệ thời gian thực thường tùy thuộc vào trạng thái định lượng những giới hạn mang lại kết quả hữu dụng.

Tuy nhiên, trong thực tế, sự phân chia này nhiều khi không cần thiết, mang tính tương đối. Đặc điểm của hệ thời gian thực Một hệ thống thời gian thực có các đặc trưng tiêu biểu [1] sau: – Tính bị động: Hệ thống thường phải phản ứng lại với các sự kiện xuất hiện vào các thời điểm thường không biết trước. – Tính nhanh nhạy: Hệ thống phải xử lý thông tin một cách nhanh chóng để có thể đưa ra kết quả phản ứng một cách kịp thời. Đây là một đặc điểm tiêu biểu.

Tuy nhiên, đối với một hệ thống có tính năng thời gian thực không nhất thiết phải đáp ứng thật nhanh mà quan trọng hơn là phải có phản ứng kịp thời đối với các yêu cầu, tác động từ bên ngoài. z 6 – Tính đồng thời: Hệ thống phải có khả năng phản ứng và xử lý đồng thời nhiều sự kiện diễn ra. – Tính tiền định: Dự đoán trước được thời gian phản ứng tiêu biểu, thời gian phản ứng chậm nhất cũng như trình tự đưa ra các phản ứng. Phải lập lịch cho các sự kiện.

Đặc tả thiết kế và yêu cầu của hệ thống Để hiểu hệ thống thường nó phải có một bản đặc tả rõ ràng. Các đặc tả thường gồm 2 phần: phần thiết kế hệ thống và phần yêu cầu. Hiển nhiên, yêu cầu là khách quan, hệ thống cần được thiết kế (chủ quan) để đạt được yêu cầu này. Việc đặc tả rõ ràng bằng một công cụ nào đó giúp cho hệ thống được hiểu dưới một ý nghĩa duy nhất và cũng giúp cho việc kiểm tra tính chính xác, đúng đắn của hệ thống (tức kiểm tra đặc tả của hệ thống có thỏa mãn tính chất yêu cầu) được dễ dàng.

Để phân tích thiết kế và đặc tả hệ thống có nhiều cách, nhiều công cụ và phương pháp khác nhau, như ngôn ngữ đặc tả RAISE, UML, Z, v.v… Đối với hệ thời gian thực có thể sử dụng các công cụ như lôgic thời gian, lôgic khoảng, ôtômat thời gian. Trong luận văn sử dụng công cụ ôtômat thời gian để phân tích và đặc tả hệ thống. Kiểm tra tính đúng đắn của hệ thống Để kiểm tra tính đúng đắn của một hệ thống ta có nhiều phương pháp, chẳng hạn:  Chứng minh bằng toán học: Sử dụng các tiên đề, luật dẫn trong các hệ toán học để từ giả thiết của bài toán bằng phương pháp suy luận dần đi đến kết quả cần chứng minh tức các tính chất yêu cầu của hệ được thỏa mãn. Trong những năm của thập kỷ 70 đã có nhiều công trình trình bày các kỹ thuật chứng minh toán học như Dijkstra, Floy, Gries, v.v… Đặc trưng và cũng là điểm yếu của phương pháp này là đòi hỏi người sử dụng phải là những người am hiểu kiến thức toán học.

 Kiểm chứng mô hình: Đến thập kỷ 80 một hướng tiếp cận khác dễ dàng hơn được đề nghị đó là kiểm chứng mô hình. Emerson lần đầu tiên đưa ra thuật ngữ Kiểm chứng mô hình (Model Checking) vào năm 1981 và định nghĩa như sau [2]: Kiểm chứng mô hình là một kỹ thuật tự động mà cho trước một mô hình trạng thái hữu hạn và một tính chất lôgic, kỹ thuật sẽ cho phép kiểm tra một cách hệ thống một trạng thái (hoặc mô hình) liệu có thỏa mãn tính chất đó.