Recently,switched Ethernet has become an active area of research because of its wide uses in industry.However,its uses have various real-time constraints on data communications.This paper analyzes the performance of t...Recently,switched Ethernet has become an active area of research because of its wide uses in industry.However,its uses have various real-time constraints on data communications.This paper analyzes the performance of the line topology switched Ethernet as a data acquisition network.Network calculus theory,which has been successfully applied to assess the real-time performance of packet-switched networks,is used to analyze the networks.To properly describe the activity of switches,a novel approach of modeling data flows into or out of switches is addressed.Based on our model,a concisely analytical expression of the maximal end-to-end delay in line topology switched Ethernet is derived.Finally,the relative simulation results are demonstrated.These results agree well with the analytical results,and thus they validate the data flow modeling techniques.展开更多
The Timed RAISE Specification Language (Timed RSL) is an extension of RAISE Specification Language by adding time constructors for specifying real-time applications. Duration Calculus (DC) is a real-time interval log...The Timed RAISE Specification Language (Timed RSL) is an extension of RAISE Specification Language by adding time constructors for specifying real-time applications. Duration Calculus (DC) is a real-time interval logic, which can be used to specify and reason about timing and logical constraints on dura- tion properties of Boolean states in a dynamic system. This paper gives a denotational semantics to a subset of Timed RSL expressions, using Duration Calculus extended with super-dense chop modality and notations to capture time point properties of piecewise continuous states of arbitrary types. Using this semantics, the paper presents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requirements.展开更多
It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this...It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether M satisfies D. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.展开更多
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.展开更多
The accumulation calculus (AC for short) is an interval based temporal logic to specify and reason about hybrid real-time systems. This paper presents a formal proof system for AC, and proves that the system is comple...The accumulation calculus (AC for short) is an interval based temporal logic to specify and reason about hybrid real-time systems. This paper presents a formal proof system for AC, and proves that the system is complete relative to that of Interval Temporal Logic (ITL for short) on real domain.展开更多
Mean Value Calculus ( MVC) is a real-time logic which can be used to specify and verify real-time systems . As a conservative extension of Duration Calculus (DC) , MVC increases the expressive power but keeps the prop...Mean Value Calculus ( MVC) is a real-time logic which can be used to specify and verify real-time systems . As a conservative extension of Duration Calculus (DC) , MVC increases the expressive power but keeps the properties of DC . ln this paper we present decidability results of MVC . An interesting result is that propositional MVC with chop star operator is still decidable, which develops the results or and .展开更多
文摘Recently,switched Ethernet has become an active area of research because of its wide uses in industry.However,its uses have various real-time constraints on data communications.This paper analyzes the performance of the line topology switched Ethernet as a data acquisition network.Network calculus theory,which has been successfully applied to assess the real-time performance of packet-switched networks,is used to analyze the networks.To properly describe the activity of switches,a novel approach of modeling data flows into or out of switches is addressed.Based on our model,a concisely analytical expression of the maximal end-to-end delay in line topology switched Ethernet is derived.Finally,the relative simulation results are demonstrated.These results agree well with the analytical results,and thus they validate the data flow modeling techniques.
基金This work is partially supported by the National Natural Science Foundation of China (No. 69773025).
文摘The Timed RAISE Specification Language (Timed RSL) is an extension of RAISE Specification Language by adding time constructors for specifying real-time applications. Duration Calculus (DC) is a real-time interval logic, which can be used to specify and reason about timing and logical constraints on dura- tion properties of Boolean states in a dynamic system. This paper gives a denotational semantics to a subset of Timed RSL expressions, using Duration Calculus extended with super-dense chop modality and notations to capture time point properties of piecewise continuous states of arbitrary types. Using this semantics, the paper presents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requirements.
文摘It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether M satisfies D. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.
文摘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.
基金This work is supported partially by the National Natural Science Foundation of China under the grant No.69703008.
文摘The accumulation calculus (AC for short) is an interval based temporal logic to specify and reason about hybrid real-time systems. This paper presents a formal proof system for AC, and proves that the system is complete relative to that of Interval Temporal Logic (ITL for short) on real domain.
文摘Mean Value Calculus ( MVC) is a real-time logic which can be used to specify and verify real-time systems . As a conservative extension of Duration Calculus (DC) , MVC increases the expressive power but keeps the properties of DC . ln this paper we present decidability results of MVC . An interesting result is that propositional MVC with chop star operator is still decidable, which develops the results or and .
