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 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. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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. LUAN VAN CHAT LUONG download : add luanvanchat@agmail. 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.
LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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 đó. Phương pháp này thực hiện duyệt tất cả các trạng thái và kiểm tra từng trạng thái trong không gian trạng thái của hệ thống xem LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 7 chúng có thực sự hoạt động đúng đắn như các yêu cầu đã được đặc tả hay không. Việc sinh ra các trạng thái và kiểm tra được tiến hành một cách hoàn toàn tự động.