This work is the sixth in a series of volumes concentrating on formal techniques applicable to distributed systems and protocols. The initial focus on techniques standardized by ISO and CCITT (Estelle, LOTOS, and SDL), widened in previous volumes to, for example, CCS, CSP, ASN.1, Z, Actor, VDM and RAISE, is yet again expanded. A strong theoretical component is balanced by a practical one, with papers included from the industrial as well as the academic communities. Offering a comprehensive presentation of the state of the art in theory, application, tools and industrialization of formal techniques, the publication provides an excellent orientation for the newcomer. By bringing together both researchers and practitioners, it also opens the communication between these groups vital for a continued cross-fertilization of knowledge and ideas for the future.
Part 1 Verification: validating simulations between large
nondeterministic specifications, R. Civalero et al; compressing the state
space representation of LOTOS specifications, J. Quemada et al; towards a
modular specification and verification of protocols within a layered
architecture, Y. Souissi. Part 2 LOTOS: specification and detection of IN
service interference using LOTOS, O.C. Dahl and E. Najm; DILL - specifying
digital logic in LOTOS, K.J. Turner and R.O. Sinnott; incremental
construction approach for distributed system specifications, F. Khendek and
G.v. Bochmann. Part 3 Invited talk: the challenges facing formal definition
techniques, C.H. West. Part 4 Automata and Estelle: increasing the
concurrency in Estelle, J. Bredereke and R. Gotzhein; experiments in data
flow analysis of communicating finite state machines, S.P. Iyer; integrating
Estelle ASN.1 for automatic implementation, A. Lo and R. Lai; an Estelle
compiler for multiprocessor platforms, S. Fischer and B. Hofmann. Part 5
Industrial reports: overview - survey of formal methods in industry, G.I.
Parkin and S. Austin; an integrated specification support system for
communication software design based on stepwise refinement and graphical
representation, K. Sarashina et al; an industrial experience on development
with LOTOS and SDL, G. Leon et al; a formal model of SONET's
alarm-surveillance procedures and their simulation, S. Narain et al. Part 6
Time and algebra: modelling systems by probabilistic process algebra - an
event structures approach, J.-P. Katoen et al; requirement specification for
real-time and hybrid systems, H. He and H. Zedan; a recursive process algebra
for queues, H. Yenigun et al; what do message sequence charts mean?, P.B.
Ladkin and S. Leue. Part 7 Testing: TESTGEN+ - an integrated environment for
protocol test suite generation, selection and validation, S.T. Vuong and S.
Lee; test generation by exposing control and data dependencies within system
specifications in SDL, H. Ural and A. Williams; on the existence and
production of state identification machines for labelled transition systems,
J. Arkko; improving conformance testing for LOTOS, A. Cavalli et al. Part 8
Protocols and formal specification: correctness of at-most-once message
delivery protocols, B.W. Lampson et al; an object oriented method for
implementing layered protocols, A. Divin and C. Petitpierre; formalization
based on understanding, M.M. Marques et al; cumulating constraints on the
"when" and the "what", T. Bolognesi and G. Ciaccio. Part 9 Timed-LOTOS: LOTOS
enhancement to specify time constraint among non-adjacent actions using first
order logic, A. Nakata et al; time versus abstraction in formal description,
H. Bowman et al; an enhanced version of timed LOTOS and its application to a
case study, L. Leonard and G. Leduc.
