Linn / Uyar Protocol Specification, Testing and Verification, XII

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
1. Auflage 2016
ISBN: 978-1-4832-9334-9
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band Volume 8, 434 Seiten, Web PDF

Reihe: IFIP Transactions C: Communication Systems

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.

Autoren/Hrsg.

Linn, R. J.

Uyar, M. Ü.

Inhaltsverzeichnis

1;Front Cover;1
2;Protocol Specification, Testing and Verification, XII;4
3;Copyright Page;5
3.1;Table of Contents;10
4;Organizing Committee;8
5;Referees;9
6;PART 1: KEYNOTE SPEECH;14
6.1;Chapter 1. Formal Methods Applied to Software Production;16
6.1.1;ABSTRACT;16
6.1.2;RESEARCH ON PRODUCTION PROCESSES;17
6.1.3;THE NEWCORE PROJECT;18
6.1.4;SOFTWARE IN THE LARGE;19
6.1.5;SOME HOPES FOR THE FUTURE;21
7;Session 1.A: TESTING THEORY;24
7.1;Chapter 2. Generating Conformance Test Sequences for Combined Control and Data Flow of Communication Protocols;26
7.1.1;Abstract;26
7.1.2;1 Introduction;26
7.1.3;2 Objective of our Testing Method;27
7.1.4;3 The Model;29
7.1.5;4 Generation of test paths and a test sequence;32
7.1.6;5 Fault Coverage;37
7.1.7;6 Comparison with related work;38
7.1.8;7 Conclusion;39
7.1.9;References;39
7.2;Chapter 3. A test suite generation method for extended finitestate machines using axiomatic semantics approach;42
7.2.1;Abstract;42
7.2.2;1 Introduction;42
7.2.3;2 Extended Finite State Machines;43
7.2.4;3 Axiomatic Semantics Approach;45
7.2.5;4 Test Cases Generation;49
7.2.6;5 Composition of a Test Suite from Test Cases;53
7.2.7;6 Conclusion;54
7.2.8;References;55
8;Session I.B: TESTABILITY;58
8.1;Chapter 4. Testing Probabilistic and Nondeterministic Processes;60
8.1.1;Abstract;60
8.1.2;1 Introduction;60
8.1.3;2 CCS with Probability;62
8.1.4;3 Testing;66
8.1.5;4 A Simple Protocol;71
8.1.6;5 Conclusion and Future Work;73
8.1.7;Acknowlegdements:;73
8.1.8;References;73
8.2;Chapter 5. Testability of Formal Specifications;76
8.2.1;Abstract;76
8.2.2;1. Introduction;76
8.2.3;2. the SPECS-Testing experiment;77
8.2.4;3 . Evaluation of the SPECS-Testing experiment;81
8.2.5;4. Implementation relations;85
8.2.6;5. Recommendations and conclusions;89
8.2.7;References;89
9;Session I.C: SPECIFICATION;92
9.1;Chapter6. Structuring Protocols using Exceptions in a LOTOS Extension;94
9.1.1;Abstract;94
9.1.2;1 Introduction;94
9.1.3;2 The Extended LOTOS Behaviour Calculus;96
9.1.4;3 Syntatic and Static Semantic Extensions;101
9.1.5;4 Structuring Principles and Examples;102
9.1.6;5 The Abracadabra Protocol Specification;104
9.1.7;6 Conclusions;108
9.1.8;References;108
9.2;Chapter 7. Formal Model of a High Speed Transport Protocol;110
9.2.1;1. Introduction;110
9.2.2;2. System of Communicating Machines (SCM);111
9.2.3;3. Problems with Existing Transport Protocols;112
9.2.4;4. Specification of a High-Speed TVansport Protocol;113
9.2.5;5. Analysis;122
9.2.6;6. Conclusion;123
9.2.7;References;124
10;Session I.D: SPECIFICATION;126
10.1;Chapter 8. On Modelling and Reasoning About Hybrid Systems;128
10.1.1;Abstract;128
10.1.2;1 Introduction;128
10.1.3;2 A Model of Real-Time Systems;132
10.1.4;3 Simulation Algorithm;136
10.1.5;4 Reasoning in TRACE(H);138
10.1.6;5 Discussion;140
10.1.7;Acknowledgements;142
10.1.8;References;142
10.2;Chapter 9. A Queue Model Relating Synchronous and Asynchronous Communication;144
10.2.1;1 Introduction;144
10.2.2;2 Queue Contexts;147
10.2.3;3 Queue Equivalence;149
10.2.4;4 Traces of Queue Contexts;151
10.2.5;5 Output Deadlocks of Queue Contexts;153
10.2.6;6 Queue Implementation Relations;154
10.2.7;7 Concluding Remarks;157
10.2.8;References;158
11;PART 2: INVITED PAPER;160
11.1;Chapter 10. Protocol development success stories: Part I;162
11.1.1;1. INTRODUCTION;162
11.1.2;2. SPECIFICATION;162
11.1.3;3. FINDING ERRORS IN PROTOCOL SPECIFICATIONS: VALIDATION;164
11.1.4;4. FINDING ERRORS IN PROTOCOL SPECIFICATIONS: VERIFICATION;166
11.1.5;5. AUTOMATIC PROTOCOL IMPLEMENTATION;168
11.1.6;6. TESTING IMPLEMENTATIONS;168
11.1.7;7. A PREDICTION;170
11.1.8;8. CONCLUSIONS;171
11.1.9;9. ACKNOWLEDGEMENT;171
11.1.10;10. REFERENCES;171
12;Session II.A: IMPLEMENTATION;174
12.1;Chapter 11. From service specification to protocol entity implementation -An exercise in formal protocol development;176
12.1.1;Abstract;176
12.1.2;1. Introduction;176
12.1.3;2. Overview of FOCUS;177
12.1.4;3. Development on the trace level;178
12.1.5;4. From trace specifications to functional specifications;183
12.1.6;5. Development on the functional level;184
12.1.7;6. Conclusion;189
12.1.8;Acknowledgement;189
12.1.9;References;189
12.2;Chapter 12. Development of Satellite Communication Networks based on LOTOS;192
12.2.1;1 INTRODUCTION;192
12.2.2;2 CODE SATELLITE NETWORK;194
12.2.3;3 DEVELOPMENT STEPS;195
12.2.4;4 CONCLUSIONS;202
12.2.5;References;203
13;Session II.B: CONFORMANCE TESTING;206
13.1;Chapter 13.A test derivation method based on exploiting structure information;208
13.1.1;Abstract;208
13.1.2;1 Introduction;208
13.1.3;2 Requirements on test derivation methods;209
13.1.4;3 Formal basis;210
13.1.5;4 Structure based test derivation method;215
13.1.6;5 Conclusions;221
13.2;Chapter 14. Automatic test generation for protocol data aspects;224
13.2.1;Abstract;224
13.2.2;1 Introduction;224
13.2.3;2 Specification of data aspects;225
13.2.4;3 Test purpose derivation;230
13.2.5;4 Test sequence generation;231
13.2.6;5 Conclusion;238
13.2.7;References;238
14;Session II.C: TESTING THEORY;240
14.1;Chapter 15. Test suite generation for a FSM with a given type of implementation errors;242
14.1.1;1. INTRODUCTION;242
14.1.2;2. FAULT FUNCTION;243
14.1.3;3. TEST SUITE DERIVATION FROM FSM WITH A FAULT FUNCTION;245
14.1.4;4. STABLE IDENTIFIERS OF STATES;249
14.1.5;5. ADVANCEMENTS OF FF-METHOD;251
14.1.6;6. CONCLUSION;254
14.1.7;7. REFERENCES;254
14.2;Chapter 16. Improvements on UIO Sequence Generationand Partial UIO Sequences;258
14.2.1;Abstract;258
14.2.2;1 Introduction;258
14.2.3;2 The Finite State Machine Model;259
14.2.4;3 Conformance Testing and UIO sequence;261
14.2.5;4 An Improved UIO Sequence Generation Algorithm;261
14.2.6;5 Partially Unique I/O Sequence;265
14.2.7;6 Test Case Generation;267
14.2.8;7 Conclusions;269
14.2.9;References;270
15;Session II.D: CONFORMANCE TESTING;274
15.1;Chapter 17. Computing Diagnostic Tests for Incorrect Processes;276
15.1.1;Abstract;276
15.1.2;1 Introduction;276
15.1.3;2 Processes, Equivalences and Preorders;277
15.1.4;3 Computing Prebisimulation Preorder and DistinguishingFormulas;282
15.1.5;4 Computing Tests;283
15.1.6;5 Examples;286
15.1.7;6 Conclusions;288
15.1.8;References;289
15.2;Chapter 18. Automated Validation of TTCN Test Suites;292
15.2.1;1 Introduction;292
15.2.2;2 Validation Aspects;293
15.2.3;3. Validation Method;297
15.2.4;4 Validation Tool;303
15.2.5;5 Conclusion;306
15.2.6;Acknowledgements;307
15.2.7;References;307
16;PART 3: INVITED PAPER;310
16.1;Chapter 19. Formal Methods in Conformance testing: Status and Expectations;312
16.1.1;1. INTRODUCTION;312
16.1.2;2. CURRENT STATE OF THE FMCT PROJECT;313
16.1.3;3. CONFORMANCE TESTING TERMINOLOGY EXPRESSED IN FDTS:PICS AND PICS PROFORMA;316
16.1.4;4. TEST CASE GENERATION METHODS CURRENTLY UNDER STUDY;316
16.1.5;5. RELATED RESEARCH;322
16.1.6;6. REFERENCES;327
17;Session III.A: CONFORMANCE TESTING;330
17.1;Chapter 20. Testability in the context of SDL;332
17.1.1;1. INTRODUCTION;332
17.1.2;2. NOTATION AND TERMINOLOGY;333
17.1.3;3. PROPERTIES OF SDL AFFECTING TESTABILITY;335
17.1.4;4 RESTRICTIONS ON TESTABLE SDL SPECIFICATIONS;342
17.1.5;5. SUMMARY;344
17.1.6;ACKNOWLEDGEMENT;345
17.1.7;REFERENCES;345
17.2;Chapter 21. A common semantics representation for SDL and TTCN;348
17.2.1;Abstract;348
17.2.2;1 . Introduction;348
17.2.3;2 . Conceptual models for SDL and TTCN;349
17.2.4;3 . Common semantics representation (CSR);353
17.2.5;4 . Conclusions;358
17.2.6;Acknowledgment;358
17.2.7;References;358
18;Session III.B: VERIFICATION;360
18.1;Chapter 22. Coverage Preserving Reduction Strategies for Reachability Analysis;362
18.1.1;1. INTRODUCTION;362
18.1.2;2. CLASSIC SEARCH;363
18.1.3;3. REDUCED SEARCH;365
18.1.4;4. CONFLICT SETS;369
18.1.5;5. FURTHER EXTENSIONS;372
18.1.6;6. STATE COMPRESSION;373
18.1.7;7. SUMMARY;376
18.1.8;8. REFERENCES;376
18.2;Chapter 23. The Two-Dimensional Window Protocol;378
18.2.1;1. INTRODUCTION;378
18.2.2;2. ON PROTOCOL DEFINITION AND VERIFICATION;380
18.2.3;3. A WINDOW PROTOCOL;382
18.2.4;4. A MULTIPLE WINDOW PROTOCOL;387
18.2.5;5. A TWO-DIMENSIONAL WINDOW PROTOCOL;390
18.2.6;6. CONCLUDING REMARKS;391
18.2.7;7. REFERENCES;392
19;Session III.C: CONVERSION AND ROUTING;394
19.1;Chapter 24. Module Composition and Refinement with Applications to Protocol Conversion;396
19.1.1;Abstract;396
19.1.2;1 Introduction;396
19.1.3;2 Background;397
19.1.4;3 Refinement Relations;400
19.1.5;4 Module Composition;402
19.1.6;5 An Example;404
19.1.7;6 Discussion;409
19.1.8;References;409
19.2;Chapter 25. Stepwise Assertional Design of Distance-Vector Routing Algorithms;412
19.2.1;Abstract;412
19.2.2;1. Introduction;412
19.2.3;2. Preliminaries: System Model and Proof Rules;414
19.2.4;3· Algorithm A1;415
19.2.5;4. Algorithm A2;418
19.2.6;5. Algorithm A3;419
19.2.7;6. Algorithm A4;420
19.2.8;7. Concluding Remarks;421
19.2.9;References;421
20;Author Index;428
21;IFIP;430