Ebook: Formal Methods for Protocol Engineering and Distributed Systems: FORTE XII / PSTV XIX’99 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specificat

Formal Methods for Protocol Engineering and Distributed Systems addresses formal description techniques (FDTs) applicable to distributed systems and communication protocols. It aims to present the state of the art in theory, application, tools an industrialization of FDTs. Among the important features presented are:

• FDT-based system and protocol engineering;
• FDT application to distributed systems;
• Protocol engineeering;
• Practical experience and case studies.

Formal Methods for Protocol Engineering and Distributed Systems contains the proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing, and Verification, which was sponsored by the International Federation for Information Processing (IFIP) and was held in Beijing, China, in October 1999.
This volume is suitable as a secondary text for a graduate level course on Distributed Systems or Communications, and as a reference for researchers and industry practitioners.

---

---

Content:
Front Matter....Pages i-xii
Front Matter....Pages 1-1
Confirming configurations in EFSM....Pages 5-24
Remote testing can be as powerful as local testing....Pages 25-40
Hit-or-Jump: An Algorithm for Embedded Testing with Applications to in Services....Pages 41-56
Scalable and Object Oriented SDL State(chart)s....Pages 59-73
Prototyping Framework for SDL with Evolving Semantics....Pages 75-94
Framework for Automatic SDL to C++ Translation....Pages 95-115
Stress Testing of Distributed Multimedia Software Systems....Pages 119-133
Fair Testing Through Probabilistic Testing....Pages 135-150
A Formal Approach to Conformance Testing of Distributed Routing Protocols....Pages 151-163
Front Matter....Pages 165-165
Deriving Activity Thread Implementations from Formal Descriptions Using Transition Reordering....Pages 169-184
A Graphical Parallel Composition Operator for Process Algebras....Pages 185-202
Guaranteeing Liveness in an Object Calculus Through Behavioral Typing....Pages 203-221
Black Box Checking....Pages 225-240
An Optimizing Compiler for Efficient Model Checking....Pages 241-256
Exploiting Symmetry When Model-Checking Software....Pages 257-275
User-Friendly Verification....Pages 279-294
Specification and Verification of Synchronous Hardware using LOTOS....Pages 295-312
Provably Correct Hardware Compilation Using Timing Diagrams....Pages 313-331
Front Matter....Pages 333-333
An enhanced model for testing asynchronous communicating systems....Pages 337-356
Interoperability Test Suite Derivation for the TCP....Pages 357-376
Front Matter....Pages 333-333
Coverage Analysis for Embedded Testing and an Application....Pages 377-386
A Formal Description Technology: Graphical E-LOTOS....Pages 389-400
Global Timed Bisimulation: An Introduction....Pages 401-416
Protocol Synthesis for Real-Time Applications....Pages 417-433
Verifying an infinite family of inductions simultaneously using data independence and FDR....Pages 437-452
Specification and execution of tests using tMsc....Pages 453-468
Model-Checking a Secure Group Communication Protocol: A Case Study....Pages 469-478
Software Model Checking....Pages 481-497
Back Matter....Pages 499-499

---

Content:
Front Matter....Pages i-xii
Front Matter....Pages 1-1
Confirming configurations in EFSM....Pages 5-24
Remote testing can be as powerful as local testing....Pages 25-40
Hit-or-Jump: An Algorithm for Embedded Testing with Applications to in Services....Pages 41-56
Scalable and Object Oriented SDL State(chart)s....Pages 59-73
Prototyping Framework for SDL with Evolving Semantics....Pages 75-94
Framework for Automatic SDL to C++ Translation....Pages 95-115
Stress Testing of Distributed Multimedia Software Systems....Pages 119-133
Fair Testing Through Probabilistic Testing....Pages 135-150
A Formal Approach to Conformance Testing of Distributed Routing Protocols....Pages 151-163
Front Matter....Pages 165-165
Deriving Activity Thread Implementations from Formal Descriptions Using Transition Reordering....Pages 169-184
A Graphical Parallel Composition Operator for Process Algebras....Pages 185-202
Guaranteeing Liveness in an Object Calculus Through Behavioral Typing....Pages 203-221
Black Box Checking....Pages 225-240
An Optimizing Compiler for Efficient Model Checking....Pages 241-256
Exploiting Symmetry When Model-Checking Software....Pages 257-275
User-Friendly Verification....Pages 279-294
Specification and Verification of Synchronous Hardware using LOTOS....Pages 295-312
Provably Correct Hardware Compilation Using Timing Diagrams....Pages 313-331
Front Matter....Pages 333-333
An enhanced model for testing asynchronous communicating systems....Pages 337-356
Interoperability Test Suite Derivation for the TCP....Pages 357-376
Front Matter....Pages 333-333
Coverage Analysis for Embedded Testing and an Application....Pages 377-386
A Formal Description Technology: Graphical E-LOTOS....Pages 389-400
Global Timed Bisimulation: An Introduction....Pages 401-416
Protocol Synthesis for Real-Time Applications....Pages 417-433
Verifying an infinite family of inductions simultaneously using data independence and FDR....Pages 437-452
Specification and execution of tests using tMsc....Pages 453-468
Model-Checking a Secure Group Communication Protocol: A Case Study....Pages 469-478
Software Model Checking....Pages 481-497
Back Matter....Pages 499-499
....