Description 
1 online resource (vii, 382 pages) : illustrations 
Series 
Lecture notes in computer science ; 407 

Lecture notes in computer science ; 407.

Contents 
Process calculi, from theory to practice: Verification tools  Testing equivalence as a bisimulation equivalence  The concurrency workbench  Argonaute: Graphical description, semantics and verification of reactive systems by using a process algebra  Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications  Verifying properties of large sets of processes with network invariants  A method for verification of trace and test equivalence  Projections of the reachability graph and environment models  Proving properties of elementary net systems with a specialpurpose theorem prover  Verification by abstraction and bisimulation  MEC : a system for constructing and analysing transition systems  Fair SMG and linear time model checking  Network grammars, communication behaviors and automatic verification  CCS, liveness, and local model checking in the linear time mucalculus  Implementing a model checking algorithm by adapting existing automated tools  Online modelchecking for finite linear temporal logic specifications  Timing assumptions and verification of finitestate concurrent systems  Specifying, programming and verifying realtime systems using a synchronous declarative language  Modal specifications  Automated verification of timed transition models  Temporal logic case study  The complexity of collapsing reachability graphs  What are the limits of model checking methods for the verification of real life protocols?  Requirement analysis for communication protocols  State exploration by transformation with lola  Parallel protocol verification: The twophase algorithm and complexity analysis  Formal verification of synchronous circuits based on stringfunctional semantics: The 7 paillet circuits in boyermoore  Combining CTL, trace theory and timing models  Localized verification of circuit descriptions  Verification of synchronous sequential machines based on symbolic execution  Parallel composition of lockstep synchronous processes for hardware validation: Divideandconquer composition 
Summary 
This volume contains the proceedings of a workshop held in Grenoble in June 1989. This was the first workshop entirely devoted to the verification of finite state systems. The workshop brought together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of finite state systems. The goal at the workshop was to compare verification methods and tools to assist the applications designer. The papers in this volume review verification techniques for finite state systems and evaluate their relative advantages. The techniques considered cover various specification formalisms such as process algebras, automata and logics. Most of the papers focus on exploitation of existing results in three application areas: hardware design, communication protocols and realtime systems 
Bibliography 
Includes bibliographical references 
Notes 
Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002. http://purl.oclc.org/DLF/benchrepro0212 MiAaHDL 

digitized 2010 HathiTrust Digital Library committed to preserve pda MiAaHDL 

Print version record 
Subject 
Computer network protocols  Congresses


Computer network protocols


Endlicher Automat


Verifikation


Protocoles de réseaux d'ordinateurs  Congrès.


Grenoble <1989>

Genre/Form 
Conference papers and proceedings

Form 
Electronic book

Author 
Sifakis, J. (Joseph), 1946

ISBN 
9783540469056 

3540469052 
