Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings (Q1188590)

[The articles of this volume will not be indexed individually.] The proceedings are the result of the first international meeting entirely devoted to the verification of finite state concurrent systems. They concern the development and the use of the methods, tools and theories for automatic verification/validation of these systems. The emphasis is not only on new research results but also on applications of existing results to real verification problems. Papers included are organized in 5 parts. The first part (the most ample one) concerns process algebras and systems of communicating processes and presents mostly verification tools/frameworks for comparison of transition systems modulo some equivalence by using reduction or an axiomatic approach. The second part on model checking is devoted to linear-time and branching-time temporal logics, whereas part three is largely dedicated to timed aspects of finite state real-time concurrent systems. Part 4 concerns some theoretical and practical areas of analysis and validation of communication protocols. The final part is mostly devoted to synchronous processes and their use in hardware specification and validation. Contents: \textit{G. Boudol}, \textit{V. Roy}, \textit{R. de Simone} and \textit{D. Vergamini}, Process calculi, from theory to practice: Verification tools (pp. 1-10); \textit{R. Cleaveland} and \textit{M. Hennessy}, Testing equivalence as a bisimulation equivalence (pp. 11-23); \textit{R. Cleaveland}, \textit{J. Parrow} and \textit{B. Steffen}, The concurrency workbench (pp. 24-37); \textit{F. Maraninchi}, Argonaute: Graphical description, semantics and verification of reactive systems by using a process algebra (pp. 38-53); \textit{R. De Nicola}, \textit{P. Inverardi} and \textit{M. Nesi}, Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications (pp. 54-67); \textit{P. Wolper} and \textit{V. Lovinfosse}, Verifying properties of large sets of processes with network invariants (pp. 68-80); \textit{L. Christoff}, A method for verification of trace and test equivalence (pp. 81-88); \textit{H. Krumm}, Projections of the reachability graph and environment models (pp. 89-96); \textit{H. Tuominen}, Proving properties of elementary net systems with a special-purpose theorem prover (pp. 97-104); \textit{H. Zuidweg}, Verification by abstraction and bisimulation (pp. 105-116); \textit{A. Arnold}, MEC: A system for constructing and analysing transition systems (pp. 117-132); \textit{H. Barringer}, \textit{M. D. Fisher} and \textit{G. D. Gough}, Fair SMG and linear time model checking (pp. 133-150); \textit{Z. Shtadler} and \textit{O. Grumberg}, Network grammars, communication behaviors and automatic verification (pp. 151-165); \textit{C. Stirling} and \textit{D. Walker}, CCS, liveness, and local model checking in the linear time mu-calculus (pp. 166-178); \textit{B. Jonsson}, \textit{A. H. Khan} and \textit{J. Parrow}, Implementing a model checking algorithm by adapting existing automated tools (pp. 179-188); \textit{C. Jard} and \textit{T. Jeron}, On-line model checking for finite linear temporal logic specifications (pp. 189-196); \textit{D. L. Dill}, Timing assumptions and verification of finite-state concurrent systems (pp. 197-212); \textit{N. Halbwachs}, \textit{D. Pilaud}, \textit{F. Ouabdesselam} and \textit{A.-C. Glory}, Specifying, programming and verifying real-time systems using a synchronous declarative language (pp. 213-231); \textit{K. G. Larsen}, Modal specifications (pp. 232-246); \textit{J. S. Ostroff}, Automated verification of timed transition models (pp. 247-256); \textit{W. G. Wood}, Temporal logic case study (pp. 257-263); \textit{S. Aggarwal}, \textit{D. Barbara}, \textit{W. Cunto} and \textit{M. Garey}, Complexity of collapsing reachability graphs (pp. 264-274); \textit{S. Graf}, \textit{J. L. Richier}, \textit{C. Rodriguez} and \textit{J. Voiron}, What are the limits of model checking methods for the verification of real life protocols? (pp. 275-285); \textit{P. Azema}, \textit{F. Vernadat} and \textit{J.-C. Lloret}, Requirement analysis for communication protocols (pp. 286-293); \textit{J. Quemada}, \textit{S. Pavon} and \textit{A. Fernandez}, State exploration by transformation with LOLA (pp. 294-302); \textit{M. C. Yuang} and \textit{A. Kershenbaum}, Parallel protocol verification: The two-phase algorithm and complexity analysis (pp. 303-316); \textit{A. Bronstein} and \textit{C. L. Talcott}, Formal verification of synchronous circuits based on string-functional semantics: The 7 paillet circuits in Boyer-Moore (pp. 317-333); \textit{J. R. Burch}, Combining CTL, trace theory and timing models (pp. 334-348); \textit{J. Staunstrup}, \textit{S. J. Garland} and \textit{J. V. Guttag}, Localized verification of circuit descriptions (pp. 349-364); \textit{O. Coudert}, \textit{C. Berthet} and \textit{J. C. Madre}, Verification of synchronous sequential machines based on symbolic execution (pp. 365- 373); \textit{G. C. Gopalakrishnan}, \textit{N. S. Mani} and \textit{V. Akella}, Parallel composition of lockstep synchronous processes for hardware validation: Divide-and-conquer composition (pp. 374-382).