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.展开更多
Many process control systems are a kind of hybrid systems. In order to develop a satisfied control strategy, i. e., to make the whole system satisfy some processing requirements, the knowledge of plant is indispensabl...Many process control systems are a kind of hybrid systems. In order to develop a satisfied control strategy, i. e., to make the whole system satisfy some processing requirements, the knowledge of plant is indispensable. This paper proposes a formal model for the general plant for a kind of process control systems. Based on the model, requirements for the system can be specified from goals, and the controller can be designed according to plant based formal approach . An industrial process control system is used to illustrate our models and methods. Duration Calculus, a real time interval logic, is utilized to specify some characters of the model and development of control program for the exemplified system.展开更多
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 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 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.
文摘Many process control systems are a kind of hybrid systems. In order to develop a satisfied control strategy, i. e., to make the whole system satisfy some processing requirements, the knowledge of plant is indispensable. This paper proposes a formal model for the general plant for a kind of process control systems. Based on the model, requirements for the system can be specified from goals, and the controller can be designed according to plant based formal approach . An industrial process control system is used to illustrate our models and methods. Duration Calculus, a real time interval logic, is utilized to specify some characters of the model and development of control program for the exemplified system.
文摘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.
基金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.
