search for books and compare prices
Tables of Contents for Formal Systems Specification
Chapter/Section Title
Page #
Page Count
Manfred Broy
Leslie Lamport
The RPC-Memory Specification Problem -- Problem Statement
1
4
1 The Procedure Interface
1
1
2 A Memory Component
1
1
3 Implementing the Memory
2
1
3.1 The RPC Component
2
1
3.2 The Implementation
3
1
4 Implementing the RPC Component
3
2
4.1 A Lossy RPC
3
1
4.2 The RPC Implementation
4
1
Manfred Broy
Stephan Merz
Katharina Spies
The RPC-Memory Case Study: A Synopsis
5
16
1 About this Book
5
1
2 The Problem
6
2
3 The Solutions
8
11
3.1 Criteria for Classification
8
3
3.2 Reviews of Individual Contributions
11
8
4 Conclusion
19
2
Martin Abadi
Leslie Lamport
Stephan Merz
A TLA Solution to the RPC-Memory Specification Problem
21
46
Introduction
21
1
1 The Procedure Interface
22
5
1.1 The Module and its Parameters
23
1
1.2 State Functions, State Predicates, and Actions
24
1
1.3 Temporal Formulas
25
2
2 A Memory Component
27
9
2.1 The Parameters
27
1
2.2 The Memory Specification
28
6
2.3 Solution to Problem 1
34
2
3 Implementing the Memory
36
16
3.1 The RPC Component
36
5
The Parameters Module
37
2
Problem 2: The RPC Component's Specification
39
2
3.2 The Implementation
41
11
The Memory Clerk
41
1
The Implementation Proof
42
10
4 Implementing the RPC Component
52
11
4.1 A Lossy RPC
53
1
4.2 The RPC Implementation
54
9
The RPC Clerk
54
2
The Implementation Proof
56
7
References
63
2
Index
65
2
Egidio Astesiano
Gianna Reggio
A Dynamic Specification of the RPC-Memory Problem
67
42
1 Introduction
67
2
2 Dynamic Specifications (DSPECs)
69
6
2.1 The formal model for dynamic systems
69
1
2.2 Dynamic structures
70
1
2.3 A logic for DSPECs
71
3
2.4 Dynamic specifications
74
1
3 A Development Process for Dynamic Systems
75
4
3.1 Development process
75
1
3.2 How to write a DSPEC
76
3
Simple dynamic system
77
1
Concurrent dynamic system
78
1
3.3 Specification presentation
79
1
4 MC Requirement Specification (PHASE 1)
79
6
Natural description
79
1
Border determination
79
1
Basic data structures
79
2
Interactions
81
1
States
81
1
Activity
82
2
Shadow spots
84
1
5 The Reusable Specification of RPC
85
4
The acceptable actual parameters
85
1
Interactions
86
1
States
87
1
Activity
87
2
6 MC Development (First Step of PHASE 2)
89
15
Natural description
89
1
Basic data structures
90
3
Components of MC
93
1
The reliable memory component RMC
93
1
The remote procedure caller RPC
93
1
The clerk CLERK
94
1
Interactions
94
1
States
95
1
Activity
95
3
Interactions (of MC)
98
1
States (of MC)
98
1
Activity (of MC)
99
3
Correctness justification
102
2
7 Discussing our Solution
104
5
Eike Best
A Memory Module Specification Using Composable High-Level Petri Nets
109
52
1 Introduction
109
1
2 The M-net Model
110
7
2.1 Definition of M-nets
110
2
2.2 Transition rule and unfolding
112
2
2.3 Composition Operations
114
3
3 Bahavioural Notions
117
6
3.1 Occurrence sequences and permutations
117
2
3.2 Collapsing transitions
119
1
3.3 Implementation relation
120
3
4 Memory Specification
123
7
4.1 Notation
123
1
4.2 Reliable and unreliable memory
124
6
5 Memory Implementation
130
9
5.1 The RPC module
131
2
5.2 The implementation
133
2
5.3 Main result
135
2
5.4 Progress and fairness
137
2
6 A Lossy Remote Procedure Call Component
139
4
6.1 Time M-nets
140
1
6.2 Lossy RPC module
140
3
7 Discussion
143
5
7.1 In retrospect
143
2
7.2 Answers to [6]
145
1
7.3 Safety and liveness specifications
146
2
A Proofs
148
13
Johan Blom
Bengt Jonsson
Constraint Oriented Temporal Logic Specification
161
22
1 Introduction
161
2
2 Temporal Logic
163
1
2.1 Syntax and Informal Semantics
163
1
3 Semantics
164
1
4 Using LTL to Specify Concurrent Systems
165
3
4.1 Specification of State Changes
165
1
4.2 State transition diagrams
166
1
4.3 Specifying Components
167
1
4.4 Combining components
168
1
5 Overall Structure of the Specification
168
1
6 The Memory Cells
169
2
7 The Memory Interface
171
5
7.1 Unreliable Memory Interface
171
3
7.2 Reliable Memory Interface
174
1
7.3 Solution to Problem 1
174
2
8 Problem 2 -- The RPC Component
176
1
8.1 Solution to Problem 2
177
1
9 Problem 3 -- The Clerk Component
177
6
9.1 Solution to Problem 3
180
3
Manfred Broy
A Functional Solution to the RPC-Memory Specification Problem
183
30
1 Introduction
183
1
2 The Basic System Model
184
2
3 Basic Message Sets Involved
186
1
4 The Unreliable and the Reliable Memory Component
187
4
5 The Remote Procedure Call Component
191
2
6 Implementation with the Help of a Clerk
193
1
7 The Composed System
194
1
8 Specification of the Lossy RPC Component
195
1
9 A Clerk for the Lossy RPC Component
196
1
10 Composing the Clerk and the Lossy RPC Component
197
1
11 Conclusion
197
16
A Mathematical Basis
198
2
B State Transition Specification of the Memory Component
200
2
C A Trace Solution to the Memory Specification Problem
202
2
D Proof of the Verification Conditions
204
9
Jorge Cuellar
Dieter Barnard
Martin Huber
A Solution Relying on the Model Checking of Boolean Transition Systems
213
40
0 Introduction
213
2
1 The Procedure Interface
215
5
1.1 Data types
215
1
1.2 Interfaces in TLT
216
4
2 A Memory Component
220
9
2.1 The Memory Specification
222
1
2.2 The Server Specificaition
223
2
2.3 Result and UserConnector Modules
225
1
2.4 Conjunction of Modules
226
2
2.5 Solution to Problem 1(a)(i)
228
1
2.6 The Reliable Server Specification
228
1
2.7 The Refinement of Server
229
1
3 A RPC Component
229
6
3.1 The RPC Specification
230
2
3.2 The RPC Implementation
232
2
3.3 The Refinement of Server
234
1
4 A Lossy RPC Component
235
7
4.1 Timed Instructions
235
2
4.2 The Lossy RPC Specification
237
3
4.3 The Supervising Clerk
240
1
4.4 Proof of the Real-time Property in Problem 5(b)
241
1
5 Conclusion
242
2
An Introduction to TLT
244
9
A.1 Concrete States and Transitions
244
1
A.2 Boolean Algebras
244
1
A.3 Boolean Transition Systems
245
1
A.4 Conjunction of Boolean Transition Systmes
245
2
A.5 Parameterization of Boolean Transition Systems
247
3
A.6 Translating the Program Notation
250
3
Reinhard Gotzhein
Applying a Temporal Logic to the RPC-Memory Specification Problem
253
22
1 Introduction
253
1
2 The Formalism
254
9
2.1 Elementary concepts
254
1
2.2 System architecture
255
1
2.3 System bahaviour
256
6
2.4 System
262
1
2.5 System refinement
262
1
3 The Memory Component
263
8
3.1 A temporal logic
264
1
3.2 Specification of the unreliable memory component
265
4
3.3 Refinements of the unreliable memory component
269
2
4 Are Architectural Requirements Important?
271
1
5 Conclusion
272
3
Jozef Hooman
Using PVS for an Assertional Verification of the RPC-Memory Specification Problem
275
30
0 Introduction
275
7
0.1 Formal Bakcground
276
1
0.2 Basic PVS Framework
277
5
1 The Procedure Interface
282
2
2 A Memory Component
284
10
2.1 Basic Properties of Memory
284
1
2.2 Inner Memory
285
3
Equivalent Formulation of the Inner Memory
286
2
2.3 Memory
288
2
2.4 Simplifying the Memory Specification
290
2
2.5 Reliable Memory
292
1
Correctness of Reliable Memory
293
1
2.6 Failing Memory
293
1
Correctness of Failing Memory
293
1
3 Implementing the Memory
294
5
3.1 The RPC Component
294
2
3.2 The Implementation
296
3
Correctness of the Implementation
298
1
4 Implementing the RPC Component
299
4
4.1 A Lossy RPC
299
1
4.2 The RPC Implementation
300
3
Correctness of the RPC Implementation
302
1
5 Concluding Remarks
303
2
Hardi Hungar
Specification and Verification Using a Visual Formalism on Top of Temporal Logic
305
36
1 Specifics of this Solution
305
3
1.1 Methodology
305
1
1.2 Problem Coverage
306
2
2 The Implementation Language
308
4
2.1 Processes and Programs
308
1
2.2 The Semantics of Programs
309
3
3 The Specification Language
312
4
3.1 The Logic
312
1
3.2 Symbolic Timing Diagrams
313
3
4 Specification of the Memory Component
316
6
4.1 The Protocol of Calls and Replies
316
2
4.2 Specification of the Functional Behavior
318
3
4.3 Reliability
321
1
5 Implementing the Memory
322
6
5.1 Specification and Verification of the Protocol
322
2
5.2 Specification and Verification of the Functional Behavior
324
4
6 Verifying an Implementation
328
8
6.1 Practical Experiments
335
1
7 Observations
336
1
7.1 Timing Diagrams Versus Temporal Logic
336
1
7.2 Adequateness of Temporal Logic
336
1
8 Conclusion
337
4
Nils Klarlund
Mogens Nielsen
Kim Sunesen
A Case Study in Verification Based on Trace Abstractions
341
34
1 Introduction
341
4
2 Monadic Second-Order Logic on Strings
345
5
2.1 FIDO
347
2
2.2 Automated translation and validity checking
349
1
3 Systems
350
4
3.1 Composition
351
2
3.2 Implementation
353
1
4 Relational Trace Abstractions
354
2
4.1 Decomposition
355
1
5 The RPC-Memory Specification Problem
356
6
5.1 The procedure interface
356
1
5.2 A memory component
357
5
Problem 1
362
1
6 Implementing the Memory
362
7
6.1 The RPC component
363
4
Problem 2
367
1
6.2 The implementation
367
2
Problem 3
369
1
7 Verifying the Implementation
369
6
Reino Kurki-Suonio
Incremental Specification with Joint Actions: The RPC-Memory Specificaiton Problem
375
30
1 Introduction
375
1
2 Foundations in TLA
376
5
2.1 Correspondence to Canonical TLA Expressions
376
1
2.2 Objects and Actions
377
1
2.3 Refinement by Superposition
378
1
2.4 Combination of Specifications
379
1
2.5 Modeling vs. Specification
380
1
3 Components and Processes
381
1
3.1 Component and Process Classes
381
1
3.2 Computational Steps by Processes
381
1
4 Procedure Calls
382
6
4.1 Interface Processes
382
1
4.2 Calls and Returns
383
3
4.3 Notes on the Formalism
386
1
4.4 Safety Properties
387
1
4.5 Reliable Procedue Calls
387
1
4.6 Call Structures
388
1
5 Memory Components
388
3
5.1 Memory Class
388
1
5.2 Memory Actions
389
1
5.3 Liveness Properties
390
1
5.4 Reliable Memory
390
1
5.5 Simplified Memory
391
1
6 The RPC Component
391
2
6.1 RPC Component Class
391
1
6.2 RPC Actions
392
1
7 Implementing the Memory
393
4
7.1 RPC-Memory Classes
393
1
7.2 RPC-Memory Actions
393
1
7.3 Correctness of the Implementation
394
3
8 Lossy RPC Component
397
2
8.1 Superposing Real-Time Properties
397
1
8.2 Zeno Behaviors
397
1
8.3 Classes for Lossy RPC
398
1
8.4 Actions for Lossy RPC
398
1
9 RPC Implementation
399
3
9.1 Classes for RPC Implemetation
399
1
9.2 Actions for RPC Implementation
400
1
9.3 Receivers with Bounded Response Times
401
1
9.4 Correctness of the Implementation
401
1
10 Concluding Remarks
402
3
Kim G. Larsen
Bernhard Steffen
Carsten Weise
The Methodology of Modal Constraints
405
32
1 Introduction
405
2
2 Modal Transition Systems
407
3
3 Actions, Design Patterns and Projective Views
410
5
3.1 Abstract Actions
410
1
3.2 Projective Views
411
2
3.3 Generalizations
413
1
3.4 Sufficient Proof Condition
414
1
4 Specification of the Untimed Problem
415
10
4.1 Specification of the Memory Component
415
5
4.2 Specification of the RPC Mechanism
420
3
4.3 The Clerk
423
2
5 Applying the Method
425
4
5.1 Formal Specification of the Implementation
425
1
5.2 Proof of Correctness
426
3
Step 1: Application of the Sufficient Proof Condition
426
1
Step 2: Skolemization
427
1
Step 3(a): Abstraction by Refinement
427
1
Step 3(b): Abstraction by Factorization
427
2
6 Timed Modal Specification
429
1
7 Specification of the Timed Problem
430
1
8 Applying the Method
431
2
9 Conclusion and Future Work
433
4
Judi Romijn
Tackling the RPC-Memory Specification Problem with I/O Automata
437
40
1 Introduction
437
3
1.1 Notes on the problem specification
438
1
Ambiguities
438
1
Observable versus internal behaviour
438
1
Fairness and real time
438
1
1.2 Notes on the I/O automata model
438
2
Benefits
438
1
Imperfections
439
1
What we added to the classic model
439
1
1.3 Further remarks
440
1
Acknowledgments
440
1
2 Preliminaries
440
1
2.1 Fair I/O automata
440
1
2.2 Details on fair I/O automata
440
1
Specification
440
1
Presentation
441
1
Proofs
441
1
3 Specifications and Varifications for Problem 1
441
6
3.1 Problem 1(a): Specification of two Memory Components
441
4
Data types
442
1
The Memory component
442
1
Liveness
443
2
The Reliable Memory component
445
1
Liveness
445
1
3.2 Problem 1(b): RelMemory implements Memory
445
1
Safety
445
1
Deadlock Freeness
446
1
Implementation
446
1
3.3 Problem 1(c): Nothing but MEM_FAILUREp actions?
446
1
4 Specificatons and Verifications for Problem 2
447
1
4.1 Problem 2: Specification of the RPC component
447
1
Data types
447
1
Specification
447
1
Liveness
448
1
5 Specifications and Verifications for Problem 3
448
12
5.1 Problem 3: Specification of the composition
448
5
Data types
448
1
A front end for the RPC component
449
1
Liveness
449
1
Renaming component RelMemory
449
2
Liveness
451
1
The implementation
451
1
Liveness
451
2
5.2 Set-up for the verification
453
1
An intermediate automaton
453
1
Liveness
453
1
5.3 Problem 3: MemoryImp implements Memory
453
7
Memory* implements Memory
453
3
MemoryImp implements Memory*
456
1
Invariants
456
2
Safety
458
1
Deadlock freeness
459
1
The main result
460
1
6 Specifications for Problem 4
460
1
6.1 Problem 4: Specification of a lossy RPC
460
1
Data types
461
1
7 Specifications and Verifications for Problem 5
461
10
7.1 Problem 5(a): The RPC implementation RPCImp
461
2
Data types
461
1
Specification
461
2
The composition
463
1
7.2 Problem 5(b): RPCImp implements RPC
463
8
A new implementation and specification
465
1
Admissible trace inclusion
466
1
Weak refinement
467
1
Fairness is preserved
468
3
A Safe and Fair I/O Automata
471
2
A.1 Safe I/O automata
471
1
Enabling of actions
471
1
Executions
471
1
Traces
471
1
A.2 Fair I/O automata
472
1
Enabling of sets
472
1
Fair executions
472
1
Fair traces
472
1
Implementation relation
472
1
Fairness as a liveness condition
472
1
B Timed and Fair Timed I/O Automata
473
4
B.1 Timed I/O automata
473
1
Timed Traces
473
1
B.2 Fair timed I/O automata
474
3
Enabling of sets
474
1
Fair executions
475
1
Fair timed traces
475
1
Implementation relation
475
2
Ketil Stolen
Using Relations on Strems to Solve the RPC-Memory Specificaiton Problem
477
44
1 Introduction
477
1
2 Streams and Operators on Streams
478
1
3 Problem I: The Memory Component
479
11
3.1 Basic Definitions
480
1
3.2 The Sequential Memory Component
481
1
3.3 The Concurrent Memory Component
482
1
3.4 The Repetitive Memory Component
483
2
3.5 Timed Streams and Operators on Timed Streams
485
1
3.6 The Reliable Memory Component
486
2
3.7 The Unreliable Memory Component
488
2
3.8 Implementation
490
1
4 Problem II: The RPC Component
490
5
4.1 Basic Definitions
490
1
4.2 The Sequential RPC Component
491
3
4.3 The RPC Component
494
1
5 Problem III: Implementing the Unreliable Memory Component
495
11
5.1 Basic Assumptions
495
1
5.2 The Sequential Clerk Component
496
1
5.3 The Clerk Component
497
1
5.4 The Implementation
497
1
5.5 Verification
498
8
6 Problem IV: The Lossy RPC Component
506
2
6.1 The Sequential Lossy RPC Component
506
2
7 Problem V: Implementing the RPC Component
508
6
7.1 The Sequential RPC Clerk Component
508
2
7.2 The Implementation
510
1
7.3 Verification
510
4
8 Conclusions
514
1
9 Acknowledgements
515
1
A Specifying the Hand-Shake Protocol
515
6
Rob T. Udink
Joost N. Kok
The RPC-Memory Specification Problem: UNITY + Refinement Calculus
521
20
1 Introduction
521
1
2 The ImpUNITY Programming Language
522
3
3 The ImpUNITY Logic
525
2
4 Program Refinement
527
2
5 The RPC-Memory Specification Problem
529
4
5.1 Implementing the RPC Component
533
1
6 Refinement Steps for The Memory Component
533
6
7 Conclusions
539
2
List of Authors
541