Formal methods for distributed system development: October 10-13, 2000, Pisa, Italy
This book addresses Formal Methods (FMs) applicable to the specification, verification, implementation, and testing of complex distributed systems and communication protocols. The early, pioneering phases in the development of Formal Methods, with their conflicts between evangelistic and skeptical attitudes, are essentially over. Many Fms have reached maturity, and a number of papers in this book report on successful experiences in specifying and verifying real distributed systems and protocols. The main topics covered are:
Formal Methods for Distributed System Development compiles the proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing, and Verification (PSTV XX), which was sponsored by the International Federation for Information Processing (IFIP) and held in Pisa, Italy, in October 2000.
This volume is suitable as a secondary text for graduate-level courses on software engineering, distributed systems, and communications, and as a reference both for researchers and for industry practitioners.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Verification of a Sliding Window Protocol Using IOA and MONA
A Priori Verification of Reactive Systems
From Rulebased to Automatabased Testing
20 other sections not shown
Other editions - View all
abstract action acyclic analysis approach asynchronous circuits automata automaton behaviour broadcaster cache circuits clock component Computer Science configuration constraints defined definition denote described eait edge EFSM environment equivalent event sequences example exclusiveU explicit belief atoms fault fault coverage Figure finite finite state machines Formal Methods formal verification formula function global graph HMSC IEEE implementation initial IPN module keywords labeled labelled transition systems language linear load test LOTOS machines macro step model checking multicast Multiclock Esterel multiset network topology node non-faulty operational semantics operator OSPF output packet path performance Proc process algebra processors Proposition protocol quasi-equivalent reachable relation represented rewriting router router-node rules safety properties satisfaction satisfies scenarios semantics sharedU Signalling FSM simulation Software specification spi calculus Statecharts structure subset synchronization techniques temporal logic test suite Theorem timer tion tool transition system tuple User Model FSM variables verification