Muutke küpsiste eelistusi

Duration Calculus: A Formal Approach to Real-Time Systems 2004 ed. [Kõva köide]

,
Teised raamatud teemal:
  • Kõva köide
  • Hind: 95,02 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 111,79 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
Duration Calculus: A Formal Approach to Real-Time Systems 2004 ed.Suurem pilt
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9783540408239.html
Märksõnad:
A comprehensive introduction to interval logic and duration calculus for modelling, analysing and verifying real-time systems. The Duration Calculus (DC) represents a logical approach to 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 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 to specify and reason about properties of state durations. The text covers theory (completeness, decidability, undecidability, model-checking), results, as well as case studies (Deadline Driven Scheduler).

Duration calculus constitutes a formal approach to the development of real-time systems; as an interval logic with special features for expressing and analyzing time durations of states in real-time systems, it allows for representing and formally reasoning about requirements and designs at an appropriate level of abstraction.This book presents the logical foundations of duration calculus in a coherent and thorough manner. Through selective case studies it explains how duration calculus can be applied to the formal specification and verification of real-time systems. The book also contains an extensive survey of the current research in this field.The material included in this book has been used for graduate and postgraduate courses, while it is also suitable for experienced researchers and professionals.
1. Introduction
1(22)
1.1 Real-Time Systems
1(8)
1.1.1 Two Examples
1(2)
1.1.2 Real Time
3(1)
1.1.3 State Models
4(2)
1.1.4 State Durations
6(3)
1.2 Interval Logic
9(5)
1.2.1 Interval Variables
9(1)
1.2.2 Interval Modalities
10(4)
1.3 Duration Calculus
14(7)
1.3.1 Models
14(4)
1.3.2 Applications
18(2)
1.3.3 Tools
20(1)
1.4 Book Structure
21(2)
2. Interval Logic
23(18)
2.1 Syntax
23(1)
2.2 Semantics
24(3)
2.3 Proof System
27(7)
2.3.1 Deduction
31(3)
2.4 Theorems
34(7)
3. Duration Calculus
41(26)
3.1 Syntax
41(1)
3.2 Semantics
41(4)
3.3 Proof System
45(6)
3.3.1 Soundness
46(2)
3.3.2 Deduction
48(3)
3.4 Theorems
51(9)
3.5 Example: Gas Burner
60(7)
3.5.1 Informal Argument
60(2)
3.5.2 Proof
62(5)
4. Deadline-Driven Scheduler
67(22)
4.1 Formalization of the Deadline-Driven Scheduler
67(9)
4.1.1 Shared Processor
68(1)
4.1.2 Periodic Requests and Deadlines
69(3)
4.1.3 Requirement
72(2)
4.1.4 Scheduler
74(2)
4.2 Liu and Layland's Theorem
76(13)
5. Relative Completeness
89(10)
5.1 Ideas Behind the Proof
89(1)
5.2 Proof of Relative Completeness
90(9)
6. Decidability
99(12)
6.1 Discrete-Time Duration Calculus
99(3)
6.1.1 Discrete Time Versus Continuous Time
100(1)
6.1.2 Expressiveness of Discrete-Time RDC
101(1)
6.2 Decidability for Discrete Time
102(4)
6.3 Decidability for Continuous Time
106(3)
6.4 Complexity, Tools and Other Decidable Subclasses
109(2)
7. Undecidability
111(14)
7.1 Extensions of RDC
111(3)
7.1.1 RDC1(r)
111(1)
7.1.2 RDC2
112(1)
7.1.3 RDC3
112(1)
7.1.4 Two-Counter Machines
113(1)
7.2 Undecidability of RDC1 (r)
114(4)
7.3 Undecidability of RDC2
118(4)
7.4 Undecidability of RDC3
122(3)
8. Model Checking: Linear Duration Invariants
125(20)
8.1 Example
126(5)
8.2 Real-Time Automata
131(2)
8.3 Linear Duration Invariants
133(2)
8.4 Reduction
135(8)
8.4.1 Congruent Equivalence
136(5)
8.4.2 Closure Properties of Normal Forms
141(1)
8.4.3 An Algorithm Deriving Normal Forms
142(1)
8.4.4 Infinite Term
143(1)
8.5 Generalization
143(2)
9. State Transitions and Events
145(20)
9.1 Introduction
145(3)
9.2 Transition Formulas
148(5)
9.2.1 Formulas S, S, S and S
148(2)
9.2.2 Formulas S, S, S and S
150(2)
9.2.3 Example: NOR Circuit
152(1)
9.3 Calculus for State Transitions
153(7)
9.3.1 Proof System: Part I
154(3)
9.3.2 Proof System: Part II
157(2)
9.3.3 Soundness and Relative Completeness
159(1)
9.4 Example: Automaton
160(5)
9.4.1 Specification
161(1)
9.4.2 Verification
162(3)
10. Superdense State Transitions 165(24)
10.1 Introduction
165(5)
10.1.1 Superdense Computation
166(3)
10.1.2 Superdense Chop
169(1)
10.2 Calculus for Superdense State Transitions
170(5)
10.2.1 Syntax
170(1)
10.2.2 Semantics
170(1)
10.2.3 Proof System
171(2)
10.2.4 Theorems
173(2)
10.3 Real-Time Semantics
175(14)
10.3.1 Program Notation
175(1)
10.3.2 Program States
176(4)
10.3.3 Program Semantics
180(5)
10.3.4 Program Specification
185(4)
11. Neighborhood Logic 189(20)
11.1 Introduction
189(2)
11.2 Syntax and Semantics
191(2)
11.3 Adequacy of Neighborhood Modalities
193(1)
11.4 Proof System
194(7)
11.4.1 Axioms and Rules
195(2)
11.4.2 Theorems
197(4)
11.5 Completeness for an Abstract Domain
201(3)
11.6 NL-Based Duration Calculus
204(5)
11.6.1 State Transitions, Liveness and Fairness
204(2)
11.6.2 Example: Delay-Insensitive Circuits
206(3)
12. Probabilistic Duration Calculus 209(18)
12.1 Introduction
209(2)
12.2 Probabilistic Automata
211(4)
12.2.1 State Sequence
212(1)
12.2.2 Satisfaction Probability
213(2)
12.3 Probabilistic Duration Calculus: Axioms and Rules
215(4)
12.3.1 Syntax
215(1)
12.3.2 Proof System: Part I
216(2)
12.3.3 Proof System: Part II
218(1)
12.4 Example: Gas Burner
219(8)
12.4.1 Calculation of μ(-Des1)
220(3)
12.4.2 Calculation of μ(-dDes2)
223(4)
References 227(12)
Abbreviations 239(2)
Symbol Index 241(2)
Index 243


Professor ZHOU Chaochen, Institute of Software, Chinese Academy of Sciences. Members of Chinese Academy of Sciences and the Third World Academy of Sciences. Former Director of International Institute for Software Technology, United Nations University. He has had about 30 years research experience in the area of formal techniques for computing systems, in particular for distributed and real-time systems.

Associate Prof. Michael R. Hansen. Informatics and Mathematical Modelling, Technical University of Denmark Research interests: Formal Methods, Computer Based Systems, Real-time systems, Hybrid systems, Duration Calculus.