Part 1 Support for protocol engineering with LOTOS: VLib - infinite virtual libraries for LOTOS, C. Pecheur; goal-driven LOTOS execution, E. Brinksma and H. Eertink; dynamic state machines with multiway synchronization, channels and shared variables, G. Karjoth. Part 2 Verification methods and tools: a verification tool for value-passing processes, H. Lin; a validation environment for LOTOS, B. Ghribi and L. Logrippo; on the verification of temporal properties, P. Godefroid and G. Holzmann. Part 3 Time and probabilities in formal design: multimedia in temporal LOTOS - a lip-synchronization algorithm, T. Regan; specification of real-time probabilistic behaviour, M. Fang et al; semi-Markovian analysis of protocol performance, P. Kritzinger and G. Wheeler. Part 4 Application of formal methods to real protocol case studies: formal description techniques at work - an ISDN Q.931 implementation using LOTOS, A. Azcorra et al; formal specification, validation and performance evaluation of the Xpress transfer protocol, S. Budkowski et al; an evolutionary approach to the development of complex protocol standards, C. Andrae et al; assessment of Estelle and EDT through real case studies, S. Haddad. Part 5 Conformance test generation and coverage: conformance testing of protocol machines without reset, M .Yao et al; refusal graphs for conformance tester generation and simplification - a computational framework, K. Drira et al; automated generation of test purposes for the OSI distributed transaction processing protocol, R.M. Baker and F. Brady; a metric based theory of test selection and coverage, J. Alilovic-Curgus and S.T. Vuong. Part 6 Methods for synthesizing and transforming formal descriptions: synthesis of protocols and protocol converters using the submodule construction approach, S.G. Kelekar and G.W. Hart; specifying and proving communication closedness in protocols, W. Janssen and J. Zwiers; action refinement in LOTOS, J.-P. Courtiat and D.E. Saidouni; an engineering approach to formal methods, K.J. Turner.
