tailieunhanh - Đặc tả hình thức các điều kiện đúng cho thực hiện song song của hệ thống giao tác trong cơ sở dữ liệu thời gian thực.

Đặc tả hình thức các điều kiện đúng cho thực hiện song song của hệ thống giao tác trong cơ sở dữ liệu thời gian thực. "Bất kỳ hệ vật chất nào nếu không tiếp nhận thêm năng lượng từ bên ngoài môi trường thì chiều biến đổi nó là tăng liên tục entropi (thông tin cấu trúc giảm dần) cho đến khi trình độ tổ chức suy giảm và tiến tới mất cấu trúc, thành một thứ đồng nhất rất ít biến đổi và vận động.". | Tạp chí Tin học và Đĩêu khiền học T. 20 s. 1 2004 263-273 A FORMAL SPECIFICATION OF THE CORRECTNESS CRITERIA FOR CONCURRENT EXECUTIONS OF A TRANSACTION SYSTEM IN REAL TIME DATABASES DOAN VAN BAN1 NGUYEN HUU NGU2 HO VAN HUONG3 1 Institute of Information Technology 2 Vietnam National University Hanoi 3 Governmental Cipher Department Hanoi Abstract. In this paper we present the correctness criteria for concurrent executions of a transaction system and a formal specification of the temporal consistency in Real Time Databases using Duration Calculus DC . We also give a formal verification of some conditions for maintaining the temporal consistency of the data. Tóm tắt. Trong bài báo chúng tôi sử dụng logic tính toán khoảng để đặc tả hình thức các điều kiện đúng cho thực hiện song song của hệ thống giao tác trong cơ sở dữ liệu thời gian thực. Sau đó đặc tả và kiểm chứng hình thức một số điều kiện duy trì nhất quán thời gian của dữ liệu. 1. INTRODUCTION In the past two decades the research in RTDBS has received a lot of attention 6 11 . It consists of two different important areas in computer science real time systems and database systems. Similar to conventional real time systems transactions in RTDBS are usually associated with time constraint . deadline. On the other hand RTDBS must maintain a database for useful information support the manipulation of database and process transactions 11 . RTDBS are used in a wide range of applications such as avionic and space air traffic control systems robotics nuclear power plants integrated manufacturing systems programmed stock trading systems and network management systems. The main goal of this paper is to formalise some aspects of RTDBS in particular the correctness criteria for concurrent executions of a transaction system using DC. This will allow us to verify the some conditions for maintaining the temporal consistency of the data using the proof system of the DC. The results of this paper is a part in our work. We .