Duration Calculus

Frontmatter

1. Introduction

Abstract

A real-time system is a computing system with real-time requirements. Let us consider the following two examples of real-time systems.

Zhou Chaochen, Michael R. Hansen

2. Interval Logic

Abstract

In this chapter we give the syntax, semantics and proof system for interval logic (IL). This part is based mainly on [27, 28]. Furthermore, we develop theorems and rules of IL which are useful when constructing proofs.

Zhou Chaochen, Michael R. Hansen

3. Duration Calculus

Abstract

In this chapter we present the syntax, semantics and proof system of duration calculus. In addition, we present some theorems and rules of DC which are useful when conducting proofs.

Zhou Chaochen, Michael R. Hansen

4. Deadline-Driven Scheduler

Abstract

The deadline-driven scheduler of Liu and Layland [85] is considered in this chapter. The main idea of the scheduler was given in Chap. 1. The correctness proof for the deadline-driven scheduler will be carried out carefully to illustrate that the proof theory of the previous two chapters can manage a nontrivial proof. The steps of the proof wil not, however, be given in as much detail as in the previous chapters and we shall omit some simple steps and annotations that we have described earlier.

Zhou Chaochen, Michael R. Hansen

5. Relative Completeness

Abstract

In this chapter, we consider the question of whether there is a proof for every valid formula of DC, i.e. whether the proof system of DC is complete. When using DC formulas in specifications, we want ∫S to be the integral of a Boolean-valued function. Therefore, to show the completeness of DC, it must be shown that the axioms DCA1 — DCA6, together with the rules IR1 and IR2 and the axioms and rules of IL, are enough to ensure that temporal variables of the form ∫S are definable by integrals.

Zhou Chaochen, Michael R. Hansen

6. Decidability

Abstract

In this chapter we consider a subset of formulas of DC for which the satisfiability of a formula is decidable. Since a formula ø is valid if the formula ¬ø is not satisfiable, we can decide whether a formula in the subset is valid as well. The decidability results presented here are based on [167].

Zhou Chaochen, Michael R. Hansen

7. Undecidability

Abstract

All the disappointing news comes in this chapter: even for a very restricted subset of DC formulas, it is undecidable whether a formula in the subset is satisfiable.

Zhou Chaochen, Michael R. Hansen

8. Model Checking: Linear Duration Invariants

Abstract

In Chap. 7, it was proved that the satisfiability (and validity) of simple subclasses of DC formulas is undecidable for both the continuous- and the discrete-time domains. In Chap. 6, decidable subclasses of DC formulas were identified. Some are decidable for both the continuous- and the discrete-time domains, while others are decidable for discrete time only.

Zhou Chaochen, Michael R. Hansen

9. State Transitions and Events

Abstract

A real-time system may comprise both states and events. A state of a system characterizes a stable aspect of the system behavior. By stable, we mean that once the system enters a state, it will stay in that state throughout a period. An event of a system characterizes an instant interaction of the system with its environment. This can drive both the system and its environment to change their behavior dramatically.

Zhou Chaochen, Michael R. Hansen

10. Superdense State Transitions

Abstract

In the Boolean state model, we assume state stability. That is, whenever a system enters a state, it will stay in the state throughout some period, although the length of the period can be arbitrarily small. Therefore, a state transition is a transition of a system from one stable state to another, and two consecutive state transitions must pass through an intermediate stable state which separates these two state transitions from each other.

Zhou Chaochen, Michael R. Hansen

11. Neighborhood Logic

Abstract

The chop-based interval temporal logics, such as ITL [43], IL and DC, are useful for the specification and verification of safety properties of real-time systems. In these logics, one can easily express properties such as

• “if ø holds for an interval, then there is a subinterval where ψ holds”, and
• “if ø holds for an interval, then ψ holds for all subintervals”.

Zhou Chaochen, Michael R. Hansen

12. Probabilistic Duration Calculus

Abstract

This chapter provides a DC-based approach to the analysis of the dependability of real-time systems.

Zhou Chaochen, Michael R. Hansen

Backmatter