Xã hội phát triển, công nghệ thông tin ngày càng giữ vị trí quan trọng trong đời sống và kỹ thuật. Nó giúp cho các nhà quản lý kinh doanh, thương mại ,quân đội,các hoạt động của con người trong nhiều lĩnh vực đem lại hiệu quả cao. Đặc biệt vấn đề về điều khiển đã hỗ trợ con người đắc lực trong việc điều khiển tự đông. Việc xây dựng các phần mềm như vậy đòi hỏi phần mềm thực thi phải có độ chính xác cao đặc biệt là luôn có các ràng buộc liên quan đến thời gian. Hiện nay có rất nhiều các nghiên cứu cũng như các phần mềm hỗ trợ cho việc thiết kế hệ thống thời gian thực được ứng dụng trong nhiều lĩnh vực khác nhau ví dụ như: hệ thống điều khiển không lưu, điều khiển tàu biển, các hệ thống ô tô, máy bay, tàu hỏa Có nhiều các công cụ khác nhau từ lý thuyết đến thực nghiệm để làm việc này, tuy nhiên, đối với các hệ thống thời gian là một công cụ lý thuyết được rất nhiều người dùng với phần mềm trợ đặc tả Uppaal. Đồ án trình bày trong ba chương với nội dung mỗi chương như sau: Chương 1: Tìm hiểu về Model checking và lý thuyết hệ thời gian thực (Real timed system). Chương 2 : Tìm hiểu về lý thuyết Otomat thời gian (Timed automata) Chương 3 : Thử nghiệm đặc tả hệ thống với công cụ Uppaal.