Protocol specification, testing and verification (PSTV) brings together contributions from researchers and practitioners interested in the application of formal methods to the design, description, analysis, implementation and testing of complex and safety-critical systems such as distributed systems or communication protocols and services. The 20 selected papers included in this publication provide a comprehensive account of the current state-of-the-art in this field. They consider, in particular, protocol engineering, improvement of formal methods, verification and synthesis methods, conformance testing and application to real case studies. Two invited papers complete the volume and address the industrial applicability of the techniques. Researchers, computer scientists and post-graduate students concerned with data communications and computer networks should find the book offers a valuable insight into this rapidly developing arena.
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.
