search for books and compare prices
Tables of Contents for Specification and Development of Interactive Systems
Chapter/Section Title
Page #
Page Count
Preface
v
Examples
xiii
Introduction
1
18
Systems
2
1
Specifications
3
3
Refinement
6
1
Application Domains
7
1
Development Process and Methodology
8
1
Rationale of Focus
9
4
Classification of Modeling Techniques
9
1
Description Paradigm
10
3
Overview of the Book
13
2
Part 1: Introductory Section
13
1
Part 2: Mathematical Foundations
14
1
Part 3: Specification
14
1
Part 4: Refinement
14
1
How the Book Should Be Read
15
4
A Guided Tour
19
32
Plan for the Tour
19
2
Station 1: Unbounded Buffer
21
8
Streams
21
1
Informal Specification
22
1
Task 1.1: A/G Specification
23
2
Task 1.2: Equational Specification
25
3
Task 1.3: Equational Specification with Local States
28
1
Station 2: Unbounded Lossy Buffer
29
4
Task 2.1: Combined Equational and A/G Specification with Oracles
30
2
Task 2.2: Table-Based Specification
32
1
Station 3: Driver
33
1
Station 4: Composite Specifications
34
3
Task 4.1: Graphical Specification
34
1
Task 4.2: Constraint-Based Specification
34
1
Task 4.3: Behavioral Refinement
35
1
Task 4.4: Glass-Box Specification
36
1
Station 5: Time-Sensitive Buffer
37
3
Timed Streams
37
1
Task 5.1: A/G Specification
38
1
Timed versus Untimed Specifications
39
1
Task 5.2: Conditional Behavioral Refinement
40
1
Station 6: Timed Lossy Buffer
40
5
Informal Specification
41
1
Task 6.1: A/G Specification
41
1
Task 6.2: Conditional Interface Refinement
42
3
Station 7: Timed Driver
45
3
Task 7.1: A/G Specification
46
1
Task 7.2: State Transition Diagram
47
1
Task 7.3: Refinement
48
1
Station 8: Timed Composite Specification
48
3
Development
48
3
Basics
51
6
Sets
51
1
Tuples
52
1
Functions
53
1
Types
53
1
Logic
54
3
Streams
57
12
Formal Definition of Streams
59
1
Basic Operators on Streams
59
3
Additional Operators on Streams
62
2
Formal Definition of Timed Streams
64
1
Operators on Timed Streams
65
4
Specifications
69
32
Classification of Specifications
70
3
Elementary Specifications
73
11
Syntax
73
1
Examples
74
6
Semantics
80
3
Graphical Representation of Syntactic Interfaces
83
1
Composite Specifications
84
4
Graphical Style
84
1
Constraint Style
85
1
Operator Style
86
1
Methodological Advice
87
1
Black-Box and Glass-Box Views
88
1
Parameterized Specifications
89
2
Sheafs and Replications
91
10
Sheafs of Channels
91
2
Specification Replication
93
3
Dependent Replications
96
5
Examples
101
14
Alternating Bit Protocol
101
3
Steam Boiler
104
3
Memory Components
107
8
Basic Definitions
108
1
Sequential Memory Component
109
1
Concurrent Memory Component
110
1
Repetitive Memory Component
111
4
Properties of Specifications
115
22
Safety and Liveness Properties
115
6
Formalization of Safety
116
2
Formalization of Liveness
118
1
Decomposition into Safety and Liveness Parts
119
1
Safety and Liveness for Specifications
120
1
Realizability
121
8
Strategies
123
1
Weak and Strong Realizability
123
3
Full Realizability
126
2
Preserving Realizability by Composition
128
1
Causality for Specifications
129
8
Adding Causality to Specifications
129
2
A Proof Principle Based on Strong Causality
131
1
Causality and Feedback
132
5
Equational Specification of State Transitions
137
24
I/O Transitions
140
7
Local States
147
3
Control States
150
5
Oracles
155
6
Access Control System
161
16
System Architecture
161
4
Functional Properties of the Controllers
165
5
Central Controller
165
1
Local Controller
165
3
Panel Controller
168
2
Introducing Exception Handling
170
2
Imposing Timing Constraints
172
5
Introducing Timeouts
172
3
Imposing Constraints on the Response Time
175
2
Tables and Diagrams
177
18
State Transition Tables
178
4
State Transition Diagrams
182
6
Semantics of State Transition Tables and Diagrams
188
7
Syntax of State Transition Diagrams
188
1
Semantics of Deterministic State Transition Diagrams
189
2
Semantics of Nondeterministic State Transition Tables
191
4
Abracadabra Protocol
195
18
Informal Specification
195
3
Protocol Data Units and Parameters
196
1
Connection Phase
197
1
Data Transfer Phase
197
1
Disconnection Phase
197
1
Error Phase
198
1
Underlying Medium Service
198
1
Formalization
198
15
Overall Structure
198
2
Sender/Receiver
200
2
Formalization of State Transitions
202
11
A/G Specifications
213
16
Simple Examples
214
7
Semantics
221
2
More Examples
223
6
Memory with Locking
229
12
Black-Box Description
229
5
Distributed Implementation
234
7
Refinement
241
12
Behavioral Refinement
242
1
Interface Refinement
242
3
Conditional Refinement
245
2
Verification
247
2
Glass-Box Refinement
249
1
Development Method
250
3
Behavioral Refinement
253
16
Definition
253
1
Simple Examples
254
5
Logical Properties
259
1
More Examples
260
2
Synchronizing the Communication
262
7
Interface Refinement
269
30
Definition
270
1
A Priming Convention for Channel Identifiers
271
1
Simple Examples
272
9
Methodological Issues
281
3
Refinement Pairs
281
1
Schematic Interface Refinement
282
1
Realizability
283
1
Logical Properties
284
2
More Examples
286
6
Generalizing Interface Refinement
292
7
Conditional Refinement
299
16
Definition
299
2
Simple Examples
301
2
Logical Properties
303
1
More Examples
304
11
Final Remarks
315
4
How Our Approach Generalizes
315
1
What We Did Not Cover
316
3
A. Operators for Stream Tuples
319
4
Generalized Operators
319
1
Tuple Filtering Operator
320
1
Timed Filtering Operator
321
2
B. Glossary of Terms
323
6
Sets
323
1
Tuples
323
1
Functions
324
1
Types
324
1
Logic
325
1
Arithmetics
325
1
Streams
326
1
Tuples of Streams
327
1
Specifications
327
1
Strategies
328
1
Refinement
328
1
Frame Labels
328
1
C. Bibliography
329
6
D. Glossary
335
10
Index
345