Formal Methods for Protocol Engineering and Distributed Systems

Preface. Committee Members. List of Referees. Invited Talk I. Part One: Test I. 1. Conforming configurations in EFSM; A. Petrenko, et al. 2. Remote testing can be as powerful as local testing; C. Jard, et al. 3. Hit-or-Jump: An algorithm for embedded testing with applications to IN services; A. Cavalli, et al. Part Two: FDTs I. 4. Scalable and Object Oriented SDL State(chart)s; B. Moller-Pedersen, D. Nogva. 5. Prototyping Framework for SDL with Evolving Semantics; P. Csurgay. 6. Framework for Automatic SDL to C++ Translation; D. Trossen, et al. Part Three: Test II. 7. Stress Testing of Distributed Multimedia Software Systems; J. Zhang, et al. 8. Fair Testing through Probabilistic Testing; M. Nunez, D. Ruperez. 9. A Formal Approach to Conformance Testing of Distributed Routing Protocols; J. Bi, J. Wu. Invited Talk II. Part Four: FDTs II. 10. Deriving Activity Thread Implementations from Formal Descriptions Using Transition Reordering; P. Langendorfer, H. Konig. 11. A Graphical Parallel Composition Operator for Process Algebras; H. Garavel, M. Sighireanu. 12. Guaranteeing liveness in an object calculus through behavioural typing; E. Najm, et al. Part Five: Model Checking. 13. Black Box Checking; D. Peled, et al. 14. An Optimizing Compiler for Efficient Model Checking; Y. Dong, C.R. Ramakrishnan. 15. Exploiting Symmetry when Model-Checking Software; P. Godefroid. Part Six: Verification. 16. User-Friendly Verification; P.-A. Hsiung, F. Wang. 17. Specification and Verification of Synchronous Hardware using LOTOS; J. He, K.J. Turner. 18. Provably Correct Hardware Compilation using Timing Diagrams; M. Schenke, M. Dossis. Invited Talk III. Part Seven: Test III. 19. An enhanced model for testing asynchronous communicating systems; M. Kim, et al. 20. Interoperability Test Suite Derivation for the TCP; S. Seol. 21. Coverage analysis for embedded testing and an application; J. Zhu, S.T. Vuong. Part Eight: FDTs III. 22. A Formal Description Technology: Graphic E-LOTOS; L. Wen, et al. 23. Global Timed Bisimulation: An Introduction; D. de Frutos-Escrig, et al. 24. Protocol Synthesis for Real-Time Applications; A. Khoumsi, et al. Part Nine: Case Studies. 25. Verifying an infinite family of inductions simultaneously using data independence and FDR; S.J. Creese and A.W. Roscoe. 26. Specification and execution of tests using tMsc; I. Ober, A. Kerbrat. 27. Model-Checking A Secure Group Communication Protocol: A Case Study; A.J. Hu, et al. Part Ten: Invited Papers. 28. Software Model Checking; G.J. Holzmann, M.H. Smith. List of Contributors. Short Papers.