This paper studies how to describe the real-time behaviour of programs using duration calculus. Since program variables are interpreted as functions over time in real-time programming, and it is inevitable to introduc...This paper studies how to describe the real-time behaviour of programs using duration calculus. Since program variables are interpreted as functions over time in real-time programming, and it is inevitable to introduce quantifications over program variables in order to describe local variable declaration and declare local channel and so on. Therefore to establish a higher-order duration calculus (HDC) is necessary. We first establish HDC, then show some real-time properties of programs in terms of HDC, and then, prove that HDC is complete on abstract domains under the assumption that all program variables vary finitely.展开更多
This paper presents another formal proof for the correctness of the Deadline Driven Scheduler (DDS). This proof is given in terms of Duration Calculus which provides abstraction for random preemption of processor. Com...This paper presents another formal proof for the correctness of the Deadline Driven Scheduler (DDS). This proof is given in terms of Duration Calculus which provides abstraction for random preemption of processor. Compared with other approaches, this proof relies on many intuitive facts. Therefore this proof is more intuitive, while it is still formal.展开更多
文摘This paper studies how to describe the real-time behaviour of programs using duration calculus. Since program variables are interpreted as functions over time in real-time programming, and it is inevitable to introduce quantifications over program variables in order to describe local variable declaration and declare local channel and so on. Therefore to establish a higher-order duration calculus (HDC) is necessary. We first establish HDC, then show some real-time properties of programs in terms of HDC, and then, prove that HDC is complete on abstract domains under the assumption that all program variables vary finitely.
基金UNU/IIST, and was done during the author's stay at UNU/IIST(July 1998 to August 1999), and partially supported by the National
文摘This paper presents another formal proof for the correctness of the Deadline Driven Scheduler (DDS). This proof is given in terms of Duration Calculus which provides abstraction for random preemption of processor. Compared with other approaches, this proof relies on many intuitive facts. Therefore this proof is more intuitive, while it is still formal.