Protocol Specification, Testing and Verification, XII (eBook)

Proceedings of the IFIP TC6/WG6.1. Twelfth International Symposium on Protocol Specification, Testing and Verification, Lake Buena Vista, Florida, U.S.A., 22-25 June, 1992

R.J. Linn, M.U. Uyar (Herausgeber)

eBook Download: PDF

2016 | 1. Auflage
434 Seiten
Elsevier Science (Verlag)
978-1-4832-9334-9 (ISBN)

Infos

For more than a decade, researchers and engineers have been addressing the problem of the application of formal description techniques to protocol specification, implementation, testing and verification. This book identifies the many successes that have been achieved within the industrial framework and the difficulties encountered in applying theoretical methods to practical situations.Issues discussed include: testing and certification; verification; validation; environments and automated tools; formal specifications; protocol conversion; implementation; specification languages and models.Consideration is also given to the concerns surrounding education available to students and the need to upgrade and develop this through sponsorship of a study of an appropriate curriculum at both undergraduate and graduate levels. It is hoped this publication will stimulate such support and inspire further research in this important arena.

Inhalt

Front Cover 1
Protocol Specification, Testing and Verification, XII 4
Copyright Page 5
Table of Contents 10
Organizing Committee 8
Referees 9
PART 1: KEYNOTE SPEECH 14
Chapter 1. Formal Methods Applied to Software Production 16
ABSTRACT 16
RESEARCH ON PRODUCTION PROCESSES 17
THE NEWCORE PROJECT 18
SOFTWARE IN THE LARGE 19
SOME HOPES FOR THE FUTURE 21
Session 1.A: TESTING THEORY 24
Chapter 2. Generating Conformance Test Sequences for Combined Control and Data Flow of Communication Protocols 26
Abstract 26
1 Introduction 26
2 Objective of our Testing Method 27
3 The Model 29
4 Generation of test paths and a test sequence 32
5 Fault Coverage 37
6 Comparison with related work 38
7 Conclusion 39
References 39
Chapter 3. A test suite generation method for extended finitestate machines using axiomatic semantics approach 42
Abstract 42
1 Introduction 42
2 Extended Finite State Machines 43
3 Axiomatic Semantics Approach 45
4 Test Cases Generation 49
5 Composition of a Test Suite from Test Cases 53
6 Conclusion 54
References 55
Session I.B: TESTABILITY 58
Chapter 4. Testing Probabilistic and Nondeterministic Processes 60
Abstract 60
1 Introduction 60
2 CCS with Probability 62
3 Testing 66
4 A Simple Protocol 71
5 Conclusion and Future Work 73
Acknowlegdements: 73
References 73
Chapter 5. Testability of Formal Specifications 76
Abstract 76
1. Introduction 76
2. the SPECS-Testing experiment 77
3 . Evaluation of the SPECS-Testing experiment 81
4. Implementation relations 85
5. Recommendations and conclusions 89
References 89
Session I.C: SPECIFICATION 92
Chapter6. Structuring Protocols using Exceptions in a LOTOS Extension 94
Abstract 94
1 Introduction 94
2 The Extended LOTOS Behaviour Calculus 96
3 Syntatic and Static Semantic Extensions 101
4 Structuring Principles and Examples 102
5 The Abracadabra Protocol Specification 104
6 Conclusions 108
References 108
Chapter 7. Formal Model of a High Speed Transport Protocol 110
1. Introduction 110
2. System of Communicating Machines (SCM) 111
3. Problems with Existing Transport Protocols 112
4. Specification of a High-Speed TVansport Protocol 113
5. Analysis 122
6. Conclusion 123
References 124
Session I.D: SPECIFICATION 126
Chapter 8. On Modelling and Reasoning About Hybrid Systems 128
Abstract 128
1 Introduction 128
2 A Model of Real-Time Systems 132
3 Simulation Algorithm 136
4 Reasoning in TRACE(H) 138
5 Discussion 140
Acknowledgements 142
References 142
Chapter 9. A Queue Model Relating Synchronous and Asynchronous Communication 144
1 Introduction 144
2 Queue Contexts 147
3 Queue Equivalence 149
4 Traces of Queue Contexts 151
5 Output Deadlocks of Queue Contexts 153
6 Queue Implementation Relations 154
7 Concluding Remarks 157
References 158
PART 2: INVITED PAPER 160
Chapter 10. Protocol development success stories: Part I 162
1. INTRODUCTION 162
2. SPECIFICATION 162
3. FINDING ERRORS IN PROTOCOL SPECIFICATIONS: VALIDATION 164
4. FINDING ERRORS IN PROTOCOL SPECIFICATIONS: VERIFICATION 166
5. AUTOMATIC PROTOCOL IMPLEMENTATION 168
6. TESTING IMPLEMENTATIONS 168
7. A PREDICTION 170
8. CONCLUSIONS 171
9. ACKNOWLEDGEMENT 171
10. REFERENCES 171
Session II.A: IMPLEMENTATION 174
Chapter 11. From service specification to protocol entity implementation -An exercise in formal protocol development 176
Abstract 176
1. Introduction 176
2. Overview of FOCUS 177
3. Development on the trace level 178
4. From trace specifications to functional specifications 183
5. Development on the functional level 184
6. Conclusion 189
Acknowledgement 189
References 189
Chapter 12. Development of Satellite Communication Networks based on LOTOS 192
1 INTRODUCTION 192
2 CODE SATELLITE NETWORK 194
3 DEVELOPMENT STEPS 195
4 CONCLUSIONS 202
References 203
Session II.B: CONFORMANCE TESTING 206
Chapter 13.A test derivation method based on exploiting structure information 208
Abstract 208
1 Introduction 208
2 Requirements on test derivation methods 209
3 Formal basis 210
4 Structure based test derivation method 215
5 Conclusions 221
Chapter 14. Automatic test generation for protocol data aspects 224
Abstract 224
1 Introduction 224
2 Specification of data aspects 225
3 Test purpose derivation 230
4 Test sequence generation 231
5 Conclusion 238
References 238
Session II.C: TESTING THEORY 240
Chapter 15. Test suite generation for a FSM with a given type of implementation errors 242
1. INTRODUCTION 242
2. FAULT FUNCTION 243
3. TEST SUITE DERIVATION FROM FSM WITH A FAULT FUNCTION 245
4. STABLE IDENTIFIERS OF STATES 249
5. ADVANCEMENTS OF FF-METHOD 251
6. CONCLUSION 254
7. REFERENCES 254
Chapter 16. Improvements on UIO Sequence Generationand Partial UIO Sequences 258
Abstract 258
1 Introduction 258
2 The Finite State Machine Model 259
3 Conformance Testing and UIO sequence 261
4 An Improved UIO Sequence Generation Algorithm 261
5 Partially Unique I/O Sequence 265
6 Test Case Generation 267
7 Conclusions 269
References 270
Session II.D: CONFORMANCE TESTING 274
Chapter 17. Computing Diagnostic Tests for Incorrect Processes 276
Abstract 276
1 Introduction 276
2 Processes, Equivalences and Preorders 277
3 Computing Prebisimulation Preorder and DistinguishingFormulas 282
4 Computing Tests 283
5 Examples 286
6 Conclusions 288
References 289
Chapter 18. Automated Validation of TTCN Test Suites 292
1 Introduction 292
2 Validation Aspects 293
3. Validation Method 297
4 Validation Tool 303
5 Conclusion 306
Acknowledgements 307
References 307
PART 3: INVITED PAPER 310
Chapter 19. Formal Methods in Conformance testing: Status and Expectations 312
1. INTRODUCTION 312
2. CURRENT STATE OF THE FMCT PROJECT 313
3. CONFORMANCE TESTING TERMINOLOGY EXPRESSED IN FDTS:PICS AND PICS PROFORMA 316
4. TEST CASE GENERATION METHODS CURRENTLY UNDER STUDY 316
5. RELATED RESEARCH 322
6. REFERENCES 327
Session III.A: CONFORMANCE TESTING 330
Chapter 20. Testability in the context of SDL 332
1. INTRODUCTION 332
2. NOTATION AND TERMINOLOGY 333
3. PROPERTIES OF SDL AFFECTING TESTABILITY 335
4 RESTRICTIONS ON TESTABLE SDL SPECIFICATIONS 342
5. SUMMARY 344
ACKNOWLEDGEMENT 345
REFERENCES 345
Chapter 21. A common semantics representation for SDL and TTCN 348
Abstract 348
1 . Introduction 348
2 . Conceptual models for SDL and TTCN 349
3 . Common semantics representation (CSR) 353
4 . Conclusions 358
Acknowledgment 358
References 358
Session III.B: VERIFICATION 360
Chapter 22. Coverage Preserving Reduction Strategies for Reachability Analysis 362
1. INTRODUCTION 362
2. CLASSIC SEARCH 363
3. REDUCED SEARCH 365
4. CONFLICT SETS 369
5. FURTHER EXTENSIONS 372
6. STATE COMPRESSION 373
7. SUMMARY 376
8. REFERENCES 376
Chapter 23. The Two-Dimensional Window Protocol 378
1. INTRODUCTION 378
2. ON PROTOCOL DEFINITION AND VERIFICATION 380
3. A WINDOW PROTOCOL 382
4. A MULTIPLE WINDOW PROTOCOL 387
5. A TWO-DIMENSIONAL WINDOW PROTOCOL 390
6. CONCLUDING REMARKS 391
7. REFERENCES 392
Session III.C: CONVERSION AND ROUTING 394
Chapter 24. Module Composition and Refinement with Applications to Protocol Conversion 396
Abstract 396
1 Introduction 396
2 Background 397
3 Refinement Relations 400
4 Module Composition 402
5 An Example 404
6 Discussion 409
References 409
Chapter 25. Stepwise Assertional Design of Distance-Vector Routing Algorithms 412
Abstract 412
1. Introduction 412
2. Preliminaries: System Model and Proof Rules 414
3· Algorithm A1 415
4. Algorithm A2 418
5. Algorithm A3 419
6. Algorithm A4 420
7. Concluding Remarks 421
References 421
Author Index 428
IFIP 430

Produkt-Details

• Erscheint lt. Verlag: 20.9.2016
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• ISBN-10: 1-4832-9334-3 / 1483293343
• ISBN-13: 978-1-4832-9334-9 / 9781483293349