Formal Methods for Protocol Engineering and Distributed Systems

by Wu, Jianping; Chanson, Samual T.; Gao, Quiang

• ISBN13: 9780792386469
• ISBN10: 0792386469
• Format: Hardcover
• Copyright: 1999-09-01
• Publisher: Kluwer Academic Pub

Summary

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.

Table of Contents

Preface	ix
Committee Members	xi
List of Referees	xii
Invited Talk I
PART ONE Test I
Confirming configurations in EFSM	5	(20)
A. Petrenko
S. Boroday
R. Groz
Remote testing can be as powerful as local testing	25	(16)
Claude Jard
Thierry Jeron
Lenaick Tanguy
Cesar Viho
Hit-or-Jump: An algorithm for embedded testing with applications to IN services	41	(18)
Ana Cavalli
David Lee
Christian Rinderknecht
Fatiha Zaidi
PART TWO FDTs I
Scalable and Object Oriented SDL State(chart)s	59	(16)
Birger Moller-Pedersen
Dagbjorn Nogva
Prototyping Framework for SDL with Evolving Semantics	75	(20)
Peter Csurgay
Framework for Automatic SDL to C++ Translation	95	(24)
Dirk Trossen
Christian Cseh
Roman Kogan
PART THREE Test II
Stress Testing of Distributed Multimedia Software Systems	119	(16)
Jian Zhang
Shing-Chi Cheung
Samuel T. Chanson
Fair Testing through Probabilistic Testing	135	(16)
Manuel Nunez
David Ruperez
A Formal Approach to Conformance Testing of Distributed Routing Protocols	151	(18)
Jun Bi
Jianping Wu
Invited Talk II
PART FOUR FDTs II
Deriving Activity Thread Implementations from Formal Descriptions Using Transition Reordering	169	(16)
Peter Langendorfer
Hartmut Konig
A Graphical Parallel Composition Operator for Process Algebras	185	(18)
Hubert Garavel
Mihaela Sighireanu
Guaranteeing liveness in an object calculus through behavioural typing	203	(22)
Elie Najm
Abdelkrim Nimour
Jean-Bernard Stefani
PART FIVE Model Checking
Black Box Checking	225	(16)
Doron Peled
Moshe Y. Vardi
Mihalis Yannakakis
An Optimizing Compiler for Efficient Model Checking	241	(16)
Yifei Dong
C.R. Ramakrishnan
Exploiting Symmetry when Model-Checking Software	257	(22)
Patrice Godefroid
PART SIX Verification
User-Friendly Verification	279	(16)
Pao-Ann Hsiung
Farn Wang
Specification and Verification of Synchronous Hardware using LOTOS	295	(18)
Ji He
Kenneth J. Turner
Provably Correct Hardware Compilation using Timing Diagrams	313	(24)
Michael Schenke
Michael Dossis
Invited Talk III
PART SEVEN Test III
An enhanced model for testing asynchronous communicating systems	337	(20)
Myungchul Kim
Jaehwi Shin
Samuel T. Chanson
Sungwon Kang
Interoperability Test Suite Derivation for the TCP	357	(20)
Soonuk Seol
Myungchul Kim
Sungwon Kang
Yongbum Park
Younghan Choe
Coverage analysis for embedded testing and an application*	377	(12)
Jinsong Zhu
Son T. Vuong
PART EIGHT FDTs III
A Formal Description Technology: Graphic E-LOTOS*	389	(12)
Li Wen
Ye Xinming
Liu Zhiyong
Global Timed Bisimulation: An Introduction*	401	(16)
David de Frutos-Escrig
Natalia Lopez
Manuel Nunez
Protocol Synthesis for Real-Time Applications*	417	(20)
Ahmed Khoumsi
Gregor v. Bochmann
Rachida Dssouli
PART NINE Case Studies
Verifying an infinite family of inductions simultaneously using data independence and FDR	437	(16)
S. J. Creese
A. W. Roscoe
Specification and execution of tests using tMsc	453	(16)
Iulian Ober
Alain Kerbrat
Model-Checking A Secure Group Communication Protocol: A Case Study*	469	(12)
Alan J. Hu
Rui Li
Xizheng Shi
Son Vuong
PART TEN Invited Papers
Soft are Model Checking	481	(18)
Gerard J. Holzmann
Margaret H. Smith
List of Contributors	499