This book presents the latest worldwide results in theory and practice of formal techniques for networked and distributed systems. The theme of the book is addressed by specialized papers in the following areas: + Formal Methods in Software Development, + Process Algebra, + Timed Automata, + Theories and Applications of Verification, + Distributed Systems Testing, + Test Sequence Derivation. In addition, the last part of the book contains special contributions by leading researchers in the above areas to add breadth and give more perspectives to the results. This volume contains the selected proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2001), which was sponsored by the International Federation for Information Processing (IFIP) and held in Cheju Island, Korea in August 2001. FORTE 2001 combines two prestigious conferences, FORTE (Formal Description Techniques for Distributed Systems and Communication Protocols) and PSTV (Protocol Specification Testing and Verification), and has more than 20 years of history. Formal Techniques for Networked and Distributed Systems will be essential reading for researchers and engineers working in the fields of communications, test equipment R&D, and telecommunications, as well as to software engineering tool developers.
Author(s): Myungchul Kim, Byoungmoon Chin, Sungwon Kang, Danhyung Lee
Series: IFIP Advances in Information and Communication Technology
Edition: 1
Publisher: Springer
Year: 2001
Language: English
Pages: 472
0792374703......Page 1
Contents......Page 6
Preface......Page 10
Program Committee and Reviewers......Page 12
Part One FORMAL METHODS IN SOFTWARE DEVELOPMENT I......Page 14
1. Automated Derivation of ILP Implementations from SDL Specifications......Page 16
2. Stepwise Design with Message Sequence Charts......Page 32
3. Formal Synthesis and Control of Soft Embedded Real-Time Systems......Page 48
Part Two DISTRIBUTED SYSTEMS TESTING......Page 65
4. Towards a Formal Framework for Interoperability Testing......Page 66
5. Distributed Test using Logical Clock......Page 82
6. Diagnosing Multiple Faults in Communicating Finite State Machines......Page 98
7. From Active to Passive: Progress in Testing of Internet Routing Protocols......Page 114
Part Three TIMED AUTOMATA......Page 130
8. Time and Action Lock Freedom Properties for Timed Automata......Page 132
9. Compiling Real-Time Scenarios into a Timed Automaton......Page 148
10. Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas......Page 164
Part Four PROCESS ALGEBRA......Page 180
11. PAMR: A Process Algebra for the Management of Resources in Concurrent Systems......Page 182
12. A Symbolic Semantics and Bisimulation for Full LOTOS......Page 198
13. Implementing a Modal Logic over Data and Processes using XTL......Page 214
Part Five APPLICATIONS OF VERIFICATION......Page 230
14. Formal Verification of Peephole Optimizations in Asynchronous Circuits......Page 232
15. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram......Page 248
16. Verifying a Sliding Window Protocol using PVS......Page 264
Part Six TEST SEQUENCE DERIVATION......Page 280
17. Test Sequence Selection......Page 282
18. Executable Test Sequence for the Protocol Data Flow Property......Page 298
19. A Method to Generate Conformance Test Sequences for FSM with Timer System Call......Page 314
Part Seven FORMAL METHODS IN SOFTWARE DEVELOPMENT II......Page 330
20. A Tool for Generating Specifications from a Family of Formal Requirements......Page 332
21. Patterns and Rules for Behavioural Subtyping......Page 348
Part Eight THEORIES OF VERIFICATION......Page 364
22. Verification of Dense Time Properties using Theories of Untimed Process Algebra......Page 366
23. Testing Liveness Properties: Approximating Liveness Properties by Safety Properties......Page 382
24. SVL: A Scripting Language for Compositional Verification......Page 390
Part Nine INVITED PAPERS......Page 406
25. On Formal Techniques in Protocol Engineering – Example Challenges......Page 408
26. A PKI-Based End-to-End Secure Infrastructure for Mobile E-Commerce......Page 434
27. A Family of Resource-Bound Real-Time Process Algebras......Page 456
28. Survivability Analysis of Networked Systems......Page 472
