Zhou C., Hansen M.R. Duration Calculus. A Formal Approach to Real-Time Systems

Springer, 2004, -256 p.Duration calculus (abbreviated to DC) represents a logical approach to the formal design of real-time systems. In DC, real numbers are used to model time, and Boolean-valued (i.e. {0,1}-valued) functions over time are used to model states of real-time systems. The duration of a state in a time interval is the accumulated presence time of the state in the interval. DC extends interval logic to a calculus that can be used to specify and reason about properties of state durations.
Research on DC began during the ProCoS project (ESPRIT BRA 3104), when the project was investigating formal techniques for designing safety-critical real-time systems. In a project case study of a gas burner system, it was realized that state duration was useful for specifying the real-time behavior of computing systems. A research program on state duration was therefore initiated by the project in 1990. The first paper on DC was published in 1991. Since then, research on DC has covered the development of logical calculi, their applications and mechanical support tools. The success of DC has also stimulated similar research on other formal approaches.
The aim of this book is to present DC in a systematic and coherent way.
The book emphasizes the Boolean state model of real-time systems and its formalization in DC. The model comprises Boolean states, state transitions and events, and superdense transitions. The formalization is carried out in DC with both contracting and expanding interval modalities, so 1.1 i at not only safety properties but also liveness and fairness properties of real-time systems can be handled. In order to analyze the dependability of real-time systems, a probabilistic duration calculus is introduced.
The hook explains how DC can be applied to formal specification and verification of real-time systems through selected case studies, which include software systems, e.g. a real-time scheduler, and software-embedded systems (also called hybrid systems), e.g. a gas burner.
The hook provides readers with theoretical results on the completeness, decidability and a model-checking algorithm of DC. These results are fundamental to the mechanical support tools for DC, but the tools themselves are not elaborated on in the book.Interval Logic
Duration Calculus
Deadline-Driven Scheduler
Relative Completeness
Decidability
Undecidability
Model Checking: Linear Duration Invariants
State Transitions and Events
Superdense State Transitions
Neighborhood Logic
Probabilistic Duration Calculus