Hệ thống thời gian thực = hệ thống rời rạc + biến đồng hồ

Bài báo này giới thiệu một cách nhẹ nhàng nhưng nghiêm ngặt phương pháp đồng hồ trong lập trình thời gian thực. Chúng tôi trình bày với độ chính xác toán học, giả định không có yêu cầu tiên quyết nào ngoài sự quen thuộc với ký hiệu logic và lập trình, các khái niệm cần thiết để hiểu, viết và thực thi các chương trình đồng hồ. Để giữ gìn phong cách trình bày, tất cả các tài liệu tham khảo được tập hợp trong phần chú thích tài liệu ở cuối mỗi phần. Phụ lục đầu tiên trình bày các quy tắc chứng minh để xác minh các thuộc tính tạm thời của các chương trình đồng hồ. Phụ lục thứ hai chỉ ra những tài liệu đã chọn về các phương pháp và công cụ hình thức trong lập trình với đồng hồ. Đặc biệt, tự động hóa thời gian, là một máy trạng thái hữu hạn được trang bị đồng hồ, đã trở thành một hình mẫu tiêu chuẩn cho việc kiểm tra mô hình thời gian thực; nó là cơ sở cho các công cụ HyTech, Kronos và Uppaal, được thảo luận ở những nơi khác trong tập này.