Parker / Rose Formal Description Techniques, IV

Proceedings of the IFIP TC6/WG6.1 Fourth International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, FORTE '91, Sydney, Australia, 19-22 November 1991
1. Auflage 2013
ISBN: 978-1-4832-9333-2
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band Volume 2, 596 Seiten, Web PDF

Reihe: IFIP Transactions C: Communication Systems

Formality is becoming accepted as essential in the development of complex systems such as multi-layer communications protocols and distributed systems. Formality is mandatory for mathematical verification, a procedure being imposed on safety-critical system development. Standard documents are also becoming increasingly formalised in order to capture notions precisely and unambiguously. This FORTE '91 proceedings volume has focussed on the standardised languages SDL, Estelle and LOTOS while, as with earlier conferences, remaining open to other notations and techniques, thus encouraging the continuous evolution of formal techniques. This useful volume contains 29 submitted papers, three invited papers, four industry reports, and four tool reports organised to correspond with the conference sessions.

Autoren/Hrsg.

Parker, K. R.

Rose, G. A.

Inhaltsverzeichnis

1;Front Cover;1
2;Formal Description Techniques, IV;4
3;Copyright Page;5
4;Table of Contents;8
5;Preface;6
6;Committee Members;12
7;Invited Speakers;13
8;Sponsors and Cooperating Organizations;14
9;List of Authors;15
10;List of Referees;16
11;Part I: APPLICATIONS I;18
11.1;Chapter 1. Using LOTOS in a Design Environment;18
11.1.1;Abstract;18
11.1.2;1. Introduction;18
11.1.3;2 LOTOS as a Design Representation Language;20
11.1.4;3 A Formal Structural Representation;22
11.1.5;4 Composing Component Behaviours;25
11.1.6;5 Example — a Telephone System;26
11.1.7;6 Conclusions;29
11.1.8;Bibliography;31
11.2;Chapter 2. Using VDM to Specify OSI Managed Objects;34
11.2.1;Abstract;34
11.2.2;1 Introduction;35
11.2.3;2 An Informal Description of the Discriminator Managed Object;36
11.2.4;3 Developing the VDM Specification;38
11.2.5;4 Overview of the VDM Specification;41
11.2.6;5 Conclusions;46
11.2.7;References;47
12;Part II: INVITED PAPER;50
12.1;Chapter 3. What is the Method in Formal Methods?;50
12.1.1;Abstract;50
12.1.2;1 Introduction;50
12.1.3;2 Design methods;51
12.1.4;3 Formalism and the design of information systems;56
12.1.5;4 A formal framework for validation;59
12.1.6;5 Conclusions;64
12.1.7;References;66
13;Part III: PERFORMANCE AND RELIABILITY;68
13.1;Chapter 4. Io: An Estelle Simulator for Performance Evaluation;68
13.1.1;Abstract;68
13.1.2;1 Introduction;69
13.1.3;2 Simulation in Estelle;69
13.1.4;3 The Simulation Tool;73
13.1.5;4 Current Status and Future Work;79
13.1.6;References;80
13.1.7;Appendix;81
13.2;Chapter 5. Modeling Timeouts and Unreliable Media with a Timed Probabilistic Calculus;84
13.2.1;Abstract;84
13.2.2;1 Introduction;84
13.2.3;2 Background and Motivation;85
13.2.4;3 Timed Probabilistic CCS;90
13.2.5;4 The Alternating Bit Protocol;94
13.2.6;5 Verification;97
13.2.7;6 Conclusions;98
13.2.8;References;99
14;Part IV: INDUSTRY REPORTS;100
14.1;Chapter 6. Formal Methods at AT&T - An Industrial Usage Report;100
14.1.1;ABSTRACT;100
14.1.2;1. INTRODUCTION;100
14.1.3;2. THE NewCoRe PROJECT;103
14.1.4;3. CONCLUSION;107
14.1.5;REFERENCES;107
14.2;Chapter 7. The Adoption of Formal Methods Within OTC;108
14.2.1;Abstract;108
14.2.2;1 Introduction;108
14.2.3;2 Background;109
14.2.4;3 Bridging the Gap between Academia and Industry;109
14.2.5;4 Achievements and Failures in Adopting Formal Techniques;111
14.2.6;5 Perceived Problems and Future Directions;111
14.2.7;6 Conclusions;114
14.2.8;Acknowledgments;115
14.2.9;References;115
14.3;Chapter 8. Linking Specifications with Implementations;116
14.3.1;Abstract;116
14.3.2;1. INTRODUCTION;116
14.3.3;2. OVERVIEW OF THE SPECS PROJECT;116
14.3.4;3. RATIONALE FOR THE INTERMEDIATE LAYER;117
14.3.5;4. THE DESIGN CRITERIA OF THE INTERMEDIATE LAYER;119
14.3.6;5. THE STRUCTURE OF I-CRL;122
14.3.7;6. CONCLUSION;124
14.3.8;References;125
14.4;Chapter 9. Experience of Using LOTOS Within the CIM-OSA Project;126
14.4.1;Abstract;126
14.4.2;1 Introduction to CIM-OSA;126
14.4.3;2 The Benefits of FDTs for CIM-OSA;127
14.4.4;3 Our Strategy for the Application of LOTOS;128
14.4.5;4 Interface Descriptions;128
14.4.6;5 Compositional Descriptions;131
14.4.7;6 Conclusions;132
14.4.8;Acknowledgements;133
14.4.9;References;133
15;Part V: APPLICATIONS II;134
15.1;Chapter 10. An Exercise in Protocol Synthesis;134
15.1.1;Abstract;134
15.1.2;1 Introduction;134
15.1.3;2 The Service Specification;135
15.1.4;3 The Theory;138
15.1.5;4 The Tools;139
15.1.6;5 The Derivation;139
15.1.7;6 Discussion and Future Directions;145
15.1.8;7 Conclusion;146
15.1.9;Acknowledgements;146
15.1.10;References;146
15.2;Chapter 11. Specification of a Distributed Coordination Function in LOTOS;150
15.2.1;Abstract;150
15.2.2;1 Introduction;150
15.2.3;2 Transaction Processing;151
15.2.4;3 The applied design method;153
15.2.5;4 Technical Approach;154
15.2.6;5 Selection of the functionalities and possible design cycles;155
15.2.7;6 TP Protocol Architecture;156
15.2.8;7 TP - MACF structures;159
15.2.9;8 Status of the work;163
15.2.10;9 Acknowledgement;163
15.2.11;10 Conclusions;164
15.2.12;References;164
15.3;Chapter 12. XP, an experiment in modular specification;166
15.3.1;Abstract;166
15.3.2;1. Introduction & Motivation;166
15.3.3;2. OBJECTS;167
15.3.4;3. MODULES AND VISIBILITY OF OBJECTS;170
15.3.5;4. OVERLOADING & ORIGINS;172
15.3.6;5. COMMUNICATION;173
15.3.7;6. SEMANTICS;175
15.3.8;7. IMPLEMENTATION;176
15.3.9;8. EXAMPLES;177
15.3.10;9. COMPARISON WITH EXTENDED LOTOS;179
15.3.11;10. CONCLUSIONS;179
15.3.12;11. REFERENCES;180
16;Part VI: INVITED PAPER;182
16.1;Chapter 13. Understanding Interfaces;182
16.1.1;Abstract;182
16.1.2;1. Introduction;182
16.1.3;2. Exploring Interface Semantics;184
16.1.4;3. Definitions;192
16.1.5;4. Composition Theorem;195
16.1.6;5. Implementation Theorems;199
16.1.7;6. Concluding Remarks;200
16.1.8;Acknowledgement;200
16.1.9;References;200
17;Part VII: CHANGE MANAGEMENT;202
17.1;Chapter 14. Modelling Dynamic Communication Structures in LOTOS;202
17.1.1;Abstract;202
17.1.2;1 Introduction;202
17.1.3;2 Dynamic Communication Structures;203
17.1.4;3 The Handover Procedure in GSM;209
17.1.5;4 Handover in LOTOS;210
17.1.6;5 Conclusions;216
17.1.7;Acknowledgment;216
17.1.8;References;216
17.2;Chapter 15. Dynamic Configuration in LOTOS;218
17.2.1;Abstract;218
17.2.2;1 Introduction;218
17.2.3;2 An Object-Based Language: OL1;220
17.2.4;3 Translation of OL1 into LOTOS;226
17.2.5;4 Semantics Preservation;229
17.2.6;5 Conclusion;230
17.2.7;Acknowledgment;231
17.2.8;References;231
17.2.9;Appendix: Definition of Types;233
18;Part VIII: TIMED EXTENSIONS;234
18.1;Chapter 16. An upward compatible timed extension to LOTOS;234
18.1.1;Abstract;234
18.1.2;1. Introduction;234
18.1.3;2. Upward compatibility with LOTOS;235
18.1.4;3. Basic choices related to the timed extension;236
18.1.5;4. Modelling urgency on action occurrences;238
18.1.6;5. Possible semantics for the timed extension;239
18.1.7;6. The proposed operational semantics of TLOTOS;242
18.1.8;7. Examples;245
18.1.9;8. Comparison with other works;246
18.1.10;9. Conclusion;247
18.1.11;Acknowledgements;248
18.1.12;References;248
18.2;Chapter 17. Mapping Time-Extended LOTOS To Standard LOTOS;250
18.2.1;Abstract;250
18.2.2;1 Introduction;250
18.2.3;2 Motivation and Requirements;251
18.2.4;3 Representing Time;252
18.2.5;4 Principles of T - LOTOS;252
18.2.6;5 Mapping Algorithm Using t-events;253
18.2.7;6 Mapping Algorithm Using Time-Stamps;258
18.2.8;7 Further Work;261
18.2.9;8 Conclusion;264
18.2.10;Acknowledgements;264
18.2.11;References;264
18.3;Chapter 18. LOTOS-like process algebras with urgent or timed interactions;266
18.3.1;Abstract;266
18.3.2;1. Introduction;266
18.3.3;2. U-LOTOS: syntax and informal semantics;268
18.3.4;3. Formal semantics;271
18.3.5;4. Expressivity;273
18.3.6;5. T-LOTOS;275
18.3.7;6. Conclusions;277
18.3.8;Acknowledgement;279
18.3.9;References;280
18.3.10;Appendix A;281
19;Part IX: TRANSFORMATIONS;282
19.1;Chapter 19. Event structures for design and transformation in LOTOS;282
19.1.1;Abstract;282
19.1.2;1 Introduction;282
19.1.3;2 Event structures;284
19.1.4;3 Decomposition of functionality;287
19.1.5;4 Specification of a FIFO buffer;289
19.1.6;5 Action refinement of a FIFO buffer;292
19.1.7;6 Conclusions;293
19.1.8;Acknowledgements;294
19.1.9;References;294
19.1.10;Appendix: Different event structure models;295
19.2;Chapter 20. A calculus to define correct transformations of LOTOS specifications;298
19.2.1;Abstract;298
19.2.2;1. Introduction;298
19.2.3;2. The Basic Calculus;299
19.2.4;3 Transformations;303
19.2.5;4 Example;311
19.2.6;5 Conclusion;312
19.2.7;Aknowledgments;312
19.2.8;References;312
19.3;Chapter 21. Inverse Expansion;314
19.3.1;Abstract;314
19.3.2;1 Introduction;314
19.3.3;2 Description of the transformations;316
19.3.4;3 The Language;317
19.3.5;4 Pure Interleaving Decomposition;317
19.3.6;5 Visible Communication Decomposition;318
19.3.7;6 Recursive Behaviours;322
19.3.8;7 Conclusions and other works;323
19.3.9;A Pure Interleaving Decomposition Proof;324
19.3.10;. Visible Communication Decomposition Proof;325
19.3.11;C REFERENCES;329
20;Part X: TOOLS AND ENVIRONMENT;330
20.1;Chapter 22. A LOTOS Data Facility Compiler (DAFY);330
20.1.1;Abstract;330
20.1.2;1. Introduction;330
20.1.3;2. The language extensions;331
20.1.4;3. Definition of the extension invocation syntax and of the translations produced;333
20.1.5;4. Design of the tool;336
20.1.6;5. Conclusion;339
20.1.7;6. Acknowledgments;340
20.1.8;7. Bibliography;340
20.1.9;Annex A : Specification using some extensions of the language;342
20.1.10;Annex . : Translation produced by DAFY;342
20.2;Chapter 23. The superimposition of Estelle programs;346
20.2.1;Abstract;346
20.2.2;1 Introduction;346
20.2.3;2 What is the Superimposition ?;347
20.2.4;3 Estelle and the Superimposition;354
20.2.5;4 An informal explanation of the transformation method;359
20.2.6;5 The implementation of the compiler;360
20.2.7;6 Conclusion;360
20.2.8;References;361
20.3;Chapter 24. Design and Implementation of an Application Interface for LOTOS Processors;362
20.3.1;Abstract;362
20.3.2;1 Introduction;362
20.3.3;2 Design policy;363
20.3.4;3 Service functions of LIpS;364
20.3.5;4 Modules and related service functions;365
20.3.6;5 Simulation for non-determinism;367
20.3.7;6 ADT manipulation;373
20.3.8;7 Internal representation language;375
20.3.9;8 Concluding remarks;375
20.3.10;Acknowledgements;377
20.3.11;References;377
21;Part XI: VALIDATION;378
21.1;Chapter 25. Formal specification, validation and implementation of an Application protocol with Estelle;378
21.1.1;Abstract;378
21.1.2;1. INTRODUCTION;378
21.1.3;2. ELDA SPECIFICATION;379
21.1.4;3. VALIDATION;381
21.1.5;4. AUTOMATIC IMPLEMENTATION;386
21.1.6;5. CONCLUSION;389
21.1.7;6. ACKNOWLEDGEMENTS;390
21.1.8;7. REFERENCES;390
21.2;Chapter 26. Specification and Validation of a Simple Overtaking Protocol using LOTOS;394
21.2.1;Abstract;394
21.2.2;1 Introduction;394
21.2.3;2 Specification of the Overtaking Protocol;395
21.2.4;3 Validation of the Overtaking Protocol;400
21.2.5;4 Discussion;405
21.2.6;5 Conclusions;406
21.2.7;6 Acknowledgments;407
21.2.8;References;407
21.3;Chapter 27. Protocol Trace Analysis based on Formal Specifications;410
21.3.1;Abstract;410
21.3.2;1 Introduction;410
21.3.3;2 Related Works;411
21.3.4;3 Experiments on Finite State Machines;413
21.3.5;4 Unified Model for Trace Analysis and Test Case Generation;414
21.3.6;5 Trace Analysis in External Test Architectures;417
21.3.7;6 Case Study;418
21.3.8;7 Test Case Generation;421
21.3.9;8 Summary;422
21.3.10;References;422
22;Part XII: LANGUAGE ISSUES;426
22.1;Chapter 28. Inheritance in LOTOS;426
22.1.1;Abstract;426
22.1.2;1 Introduction;426
22.1.3;2 Basic Object Oriented definitions;427
22.1.4;3 Inheritance;429
22.1.5;4 Inheritance in LOTOS: problems;429
22.1.6;5 Solving the subtyping problem;430
22.1.7;6 Solving the redirection problem;433
22.1.8;7 Conclusions;435
22.1.9;Acknowledgements;436
22.1.10;References;436
22.1.11;A Proofs;437
22.1.12;. Inference rules for self;441
22.2;Chapter 29. Mixing LOTOS and SDL Specifications;442
22.2.1;Abstract;442
22.2.2;1 Introduction;442
22.2.3;2 SDL and LOTOS;444
22.2.4;3 Overview of the Mixing Model;445
22.2.5;4 Semantics of Mixed Specifications;450
22.2.6;5 Run-time Support for Mixing;452
22.2.7;6 Conclusion;455
22.2.8;7 Acknowledgements;455
22.2.9;References;455
22.3;Chapter 30. .ß: a Virtual LOTOS Machine;458
22.3.1;Abstract;458
22.3.2;1 INTRODUCTION;458
22.3.3;2 THE ABSTRACT MODEL;460
22.3.4;3 THE LANGUAGE;461
22.3.5;4 SEMANTICS;467
22.3.6;5 IMPLEMENTATION;470
22.3.7;6 CONCLUSIONS;471
22.3.8;References;472
22.3.9;A Complete Example;473
23;Part XIII: TOOLS REPORTS;474
23.1;Chapter 31. Tool Demonstration: FORSEE;474
23.1.1;Abstract;474
23.1.2;1 Introduction;474
23.1.3;2 FORSEE;475
23.1.4;3 Acknowledgements;477
23.1.5;References;477
23.2;Chapter 32. Tool Demonstration: Tools for Process Algebras;480
23.2.1;1 Introduction;480
23.2.2;2 ECRINS;480
23.2.3;3 AUTO;481
23.2.4;4 MAUTO;482
23.2.5;5 AUTOGRAPH;482
23.2.6;References;482
23.3;Chapter 33. Tool Demonstration: A Cross Compiling Experiment: a PC Implementation of a LOTOS Spec;484
23.3.1;Abstract;484
23.3.2;1 INTRODUCTION;484
23.3.3;2 PROCEDURE: METHOD AND TOOLS;485
23.3.4;3 FUTURE WORK;487
23.3.5;References;487
23.4;Chapter 34. Tool Demonstration: The Lotosphere Integrated Tool Environment Lite;488
23.4.1;Abstract;488
23.4.2;1 Introduction;488
23.4.3;2 The Structure of Lite;489
23.4.4;3 The Components of Lite;489
23.4.5;4 More Information;491
23.4.6;Acknowledgements;491
23.4.7;Further Information;491
24;Part XIV: INVITED PAPER;492
24.1;Chapter 35. Superposition Refinement of Parallel Algorithms;492
24.1.1;Abstract;492
24.1.2;1 Introduction;492
24.1.3;2 Refinement calculus;494
24.1.4;3 Action systems formalism;496
24.1.5;4 Superposition refinement of action systems;499
24.1.6;5 A first superposition refinement: C2;501
24.1.7;6 Additional superposition steps;505
24.1.8;7 Conclusions;507
24.1.9;Acknowledgements;508
24.1.10;References;508
25;Part XV: VERIFICATION;512
25.1;Chapter 36. Specification and Verification of a Sliding Window Protocol in LOTOS;512
25.1.1;Abstract;512
25.1.2;1 Introduction;512
25.1.3;2 The Lotosphere Tool Environment;514
25.1.4;3 Specification of the Protocol;517
25.1.5;4 Computing the global behaviour;522
25.1.6;5 Partial Properties;524
25.1.7;6 Conclusion;525
25.1.8;Acknowledgements;526
25.1.9;References;526
25.2;Chapter 37. Protocol Verification System for SDL Specifications Based on Acyclic Expansion Algorithm and Temporal Logic;528
25.2.1;Abstract;528
25.2.2;1. Introduction;528
25.2.3;2. Outline of the System;529
25.2.4;3. Protocol Model;531
25.2.5;4. Requirements;534
25.2.6;5. Protocol Verification Method;535
25.2.7;6. Protocol Verification Example;536
25.2.8;7. Conclusion;539
25.2.9;Acknowledgements;543
25.2.10;References;543
26;Part XVI: PROCESS FOUNDATIONS;544
26.1;Chapter 38. Process Algebra Traces Augmented with Causal Relationships;544
26.1.1;Abstract;544
26.1.2;1 Introduction;544
26.1.3;2 Notation;545
26.1.4;3 Formal Treatment;546
26.1.5;4 Properties;551
26.1.6;5 Application;552
26.1.7;6 Implementation;554
26.1.8;7 Related Work;555
26.1.9;8 Conclusion;557
26.1.10;References;557
26.2;Chapter 39. Fairness in LOTOS;560
26.2.1;Abstract;560
26.2.2;1. INTRODUCTION;560
26.2.3;2. THEORETICAL FRAMEWORK;561
26.2.4;3. GROUPING LABELED TRANSITIONS;563
26.2.5;4. PROCESS, ALTERNATIVE AND CHANNEL FAIRNESS IN LOTOS;565
26.2.6;5. FORMALIZATION OF LOTOS FAIRNESS CONCEPTS;569
26.2.7;6. PROVING LIVENESS;573
26.2.8;7. ON THE FAIR EXECUTION OF LOTOS SPECIFICATIONS;574
26.2.9;8. CONCLUSIONS;574
26.2.10;ACKNOWLEDGEMENTS;574
26.2.11;REFERENCES;574
26.3;Chapter 40. A LOTOS Based Calculus with True Concurrency Semantics;576
26.3.1;Introduction;576
26.3.2;1 A Notation for Representing Pomsets;577
26.3.3;2 POtLOTOS - Partial Order tiny LOTOS;582
26.3.4;Conclusion;589
26.3.5;Bibliography;590