상세정보

LOTOS (Language Of Temporal Ordering Specification) became an international standard in 1989, although application of preliminary versions of the language to communication services and protocols of the ISO/OSI family dates back to 1984. This history of the use of LOTOS made it apparent that more advantages than the pure production of standard reference documents were to be expected from the use of such formal description techniques.
LOTOSphere: Software Development with LOTOS describes in depth a five year project that moved LOTOS out of the ISO tower into software engineering practice. LOTOS became a vehicle for efficient, yet formally based industrial software specification, design, verification, implementation and testing.
LOTOSphere: Software Development with LOTOS is divided into six parts. The first introduces the reader to LOTOS and the project LOTOSphere. The five remaining each treat an important part of the software development life cycle using LOTOS. This is the first book to give a comprehensive treatment of the use of these formal description techniques in a software engineering environment. It will thus be a valuable reference for researchers and software developers and can also be used as a text for an advanced course on the subject.


LOTOS (Language Of Temporal Ordering Specification) became an international standard in 1989, although application of preliminary versions of the language to communication services and protocols of the ISO/OSI family dates back to 1984. This history of the use of LOTOS made it apparent that more advantages than the pure production of standard reference documents were to be expected from the use of such formal description techniques.
LOTOSphere: Software Development with LOTOS describes in depth a five year project that moved LOTOS out of the ISO tower into software engineering practice. LOTOS became a vehicle for efficient, yet formally based industrial software specification, design, verification, implementation and testing.
LOTOSphere: Software Development with LOTOS is divided into six parts. The first introduces the reader to LOTOS and the project LOTOSphere. The five remaining each treat an important part of the software development life cycle using LOTOS. This is the first book to give a comprehensive treatment of the use of these formal description techniques in a software engineering environment. It will thus be a valuable reference for researchers and software developers and can also be used as a text for an advanced course on the subject.

정보제공 :

CONTENTS
PREFACE = xiii
Part Ⅰ Introduction and overview = 1
 1 LOTOSPHERE AN ATTEMPT TOWARDS A DESIGN CULTURE / Chris   A. Vissers ; Luis Ferreira Pires ; Jeroen van de Lagemaat = 3
  1 Introduction = 3
  2 Elements of a Design Culture = 5
  3 The Lotosphere Project = 15
  4 Lotosphere and the Elements of a Design Culture = 16
  5 Conclusions = 25
  REFERENCES = 25
 2 THE LOTOSPHERE DESIGN METHODOLOGY / Juan Quemada ; Azcorra ;  Santiago Pavon = 29
  1 Introduction = 29
  2 Design by Stepwise Refinement using LOTOS = 30
  3 Formal Design = 36
  4 Implementation of Prototyping = 45
  5 Assessment = 48
  6 Example The Two Key System = 54
  REFERENCES = 58
 3 DESIGN AND IMPLEMENTATION STRATEGIES / Jeroen Schot ; Luis Ferreira Pires = 59
  1 Introduction = 59
  2 Structuring of the Implementation Phase = 60
  3 Correctness Preserving Transformations = 63
  4 Requirements for Implementation = 66
  5 Mapping onto Implementation Components = 70
  6 An Implementation Example = 72
  7 Conclusions = 84
  REFERENCES = 84
 4 GETTING TO USE THE LOTOSPHERE INTEGRATED TOOL ENVIRONMENT / Jose A. Manas = 87
  1 Introduction = 87
  2 A Sample Specification The Case of NIM = 89
  3 Getting the Specification Right = 91
  4 Getting the Right Specification = 92
  5 Realizing the Specification = 102
  6 Lite and Minilite Components = 104
  7 Conclusions = 106
  REFERENCES = 107
 5 LOTOS INDUSTRIAL APPLICATIONS / Edwin Wiedmer = 109
  1 Introduction = 109
  2 LOTOS Application ISDN and Mini-Mail = 110
  3 LOTOS Application OSI Transaction Processing = 113
  4 Experience with Methods and Tools = 114
  5 Some Industrial Users of LOTOS = 117
  6 Conclusion = 119
  REFERENCES = 119
 6 APPLYING LOTOS TO OSI APLICATION LAYER PROTOCOLS / Robert E. Booth = 121
  1 Introduction = 121
  2 The OSI Context = 123
  3 OSI Perspectives on the Lotosphere Methodology = 124
  4 A Hybrid Development Trajectory = 129
  5 Achievments = 131
  6 Conclusions = 132
  REFERENCES = 133
Part Ⅱ SPECIFICATION AND TRANSFORMATION = 135
 7 LOTOS SPECIFICATION STYLE FOR OSI / Ken J. Turner ; Marten van Sinderen = 137
  1 Introduction = 137
  2 Specification Elements for OSI Services = 139
  3 Specification Elements for OSI Protocols = 149
  4 Conclusion = 158
  REFERENCES = 158
 8 CORRECTNESS PRESERVING TRANSFORMATIONS FOR THE EARLY PHASES OF SOFTWARE DEVELOPMENT / Tommaso Bolognesi ; David De Frutos ; Rom Langerak ; Diego Latella = 161
  1 Introduction = 161
  2 The running example a Programmable Sound Sequencer = 162
  3 Gate splitting = 164
  4 Inverse expansion = 168
  5 Splitting processes = 173
  6 Regrouping parallel processes = 175
  7 Conlusions = 179
  REFERENCES = 180
 9 CORRECTNESS PRESERVING TRANSFORMATIONS FOR THE LATE  PHASES OF SOFTWARE DEVELOPMENT / Alessandro Fantechi ; B         Mekhanet ; Elie Najm ; P. Cunha ; J. Queiroz = 181
  1 Introduction = 181
  2 Transformations applicable to the late phases of the design trajectory = 182
  3 Description of Museum Security System = 188
  4 A 3-way 2-way rendez-vous transformation = 189
  5 LOTOS to LOTOMATON phase = 193
  6 Realisation phase = 195
  7 Discussion and Conlusion = 198
  REFERENCES = 198
 10 A CASE STUDY ON PROTOCOL DESIGN / Jean-Pierre Couriat ; Djamel-Eddine Saidouni = 201
  1 Introduction = 201
  2 Specification of the user's requirements = 202
  3 The design trajectory = 205
  4 Assessment = 213
  5 Conclusin = 216
  REFERENCES = 217
Part Ⅲ ANALYSIS = 219
 11 EXECUTING LOTOS SPECIFICATIONS THE SMILE TOOL / Henk Eertink = 221
  1 Introduction = 221
  2 Symbolic simulation = 221
  3 Symbolic simulation in SMILE = 226
  4 Functionality of SMILE = 228
  5 Advanced functionalities of SMILE = 231
  6 Implementation = 233
  7 Future developments and availability = 233
  REFERENCES = 234
 12 A PRAGMATIC APPROACH TO VERIFICATION VALIDATION AND COMPILATION / Tomas de Miguel ; Arturo Azcorra ; Juan Quemada ; Jose    A. Manas = 235
  1 Introduction = 235
  2 Validation = 236
  3 Verification = 243
  4 Compilation = 247
  5 Conclusions = 252
  REFERENCES = 253
 13 AN EXERCISE IN PROTOCOL VERIFICATION / Stefania Gnesi ; Eric Madelaine ; Gioia Ristori = 255
  1 Introduction = 255
  2 Behaviour Oriented Style versus Basic Lotos = 257
  3 Verification tools in lite = 259
  4 A Secure Datagram Protocol = 262
  5 Conclusion = 277
  REFERENCES = 277
 14 A TOOL FOR CHECKING ADT COMPLETENESS AND CONSISTENCY / Dietmar Wolz = 281
  1 Introduction = 281
  2 Algebraic Specifications with Conditional Equations = 282
  3 Criteria for the applicability of narrowing and rewriting = 284
  4 Example for data type checking = 288
  5 Implementation limitations and performance = 290
  6 Relation to Persistency and Completion = 291
  7 Conclusion = 292
  REFERENCES = 293
 15 DEFIVING TESTS FROM LOTOOS SPECKFICATIONS / Clazien D. Wezeman = 295
  1 Introduction = 295
  2 Notation = 296
  3 The CO-OP method and LOTOS = 297
  4 Concise presentations of Compulsory and Options = 301
  5 Initial behaviour of a tester = 303
  6 Subsequent tester behaviour = 306
  7 The alternative CO-OP method = 308
  8 The full LOTOS CO-OP method = 309
  9 Conclusions = 313
  REFERENCES = 314
Part Ⅳ IMPLEMENTATION = 317
 16 THE COLOS COMPILER / Ken Warkentyne ; Erec Dubuis = 319
  1 Introduction = 319
  2 Functional Description = 320
  3 Restrictions and Annotations = 321
  4 Some Hints on Using COLOS = 327
  5 Future Work = 329
  REFERENCES = 329
  APPENDIX A The a predicate = 330
   A.1 The B Predicate = 330
 17 TP PROTOCOL FROM SPECIFICATION TO IMPLEMENTATION / Jng Widya ; Gert-Jan van der Heijden ; Francois Juillot = 333
  1 Introduction = 333
  2 Transaction Processing = 334
  3 The Design Methodology = 335
  4 TP Design Trajectory = 336
  5 First Design Cycle = 337
  6 Second Design Cycle = 345
  7 Status of the Specifications = 345
  8 Experiences = 346
  9 Conclusions = 347
  REFERENCES = 348
 18 REALIZATION OF CCR IN C / Val Jones = 349
  1 Introduction = 349
  2 The Lotosphere Development Trajectory = 350
  3 Compilation using TOPO = 351
  4 Transformation to "high-level" C = 355
  5 Comparison of the two approaches = 364
  6 Conclusions = 366
  REFERENCES = 367
 19 ALTO AN INTERACTIVE TRANSFORMATION TOOL FOR LOTOS AND LOTOMATON / Elie Najm ; A. Serhrouchni ; A. Lakas ; Eric. Madelaine ; Robert. de Simone = 369
  1 Intorduction = 369
  2 The LOTOMATON Framework = 370
  3 The ALTO Tool = 384
  4 Conclusion = 387
  REFERENCES = 388
Part Ⅴ GRAPHICAL LOTOS = 389
 20 G-LOTOS A GRAPHICAL LANGUAGE FOR CONCURRENT SYSTEMS / Tommaso Bolognesi ; Elie Najm ; Paul A.J. Tilanus = 391
  1 Introduction = 391
  2 Processes and actions = 392
  3 Behaviour diagrams = 395
  4 Data = 411
  5 Complete specification = 414
  6 A movie interpretation = 424
  7 LOTOS specification of the Museum Control System = 428
  8 Textual LOTOS to G-LOTOS conversion table = 430
  9 Conclusions = 435
  REFEREBCES = 436
 21 GLOW 3.0-A GRAPHICAL LOTOS BROWSER / Tommaso Bolognesi ; Maurizion Caneve ; Elena Salvatori = 439
  1 Introduction = 439
  2 The user's view = 439
  3 Tool architecture = 446
  4 Conclusions = 450
  REFERENCES = 450
Part Ⅵ LOTOS ENHANCEMENTS = 451
 22 ENHANCEMENTS OF LOTOS / Ed Brinksma ; George Leih = 453
  1 Introduction = 453
  2 Design Principles of Modular LOTOS = 454
  3 Data Revisions = 456
  4 Modularization Concepts = 460
  5 Discussion = 464
  REFERENCES = 465
 23 DATA SPECIFICATIONS IN MODULAR LOTOS / Rudolph Roth ; Jan de Meer ; Silke Storp = 467
  1 Introduction = 467
  2 Data Specification Case Study = 467
  3 Modular LOTOS Enhancements for Data Specifications = 470
  4 Conclusion = 478
  REFERENCES = 479
INDEX = 481