Automatic Verification Methods for Finite State Systems

1. Front Matter

   PDF

2. Process calculi, from theory to practice: Verification tools

   • Gérard Boudol, Valérie Roy, Robert de Simone, Didier Vergamini

   Pages 1-10

3. Testing equivalence as a bisimulation equivalence

   • Rance Cleaveland, Matthew Hennessy

   Pages 11-23

4. The concurrency workbench

   • Rance Cleaveland, Joachim Parrow, Bernhard Steffen

   Pages 24-37

5. Argonaute: Graphical description, semantics and verification of reactive systems by using a process algebra

   • Florence Maraninchi

   Pages 38-53

6. Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications

   • R. De Nicola, P. Inverardi, M. Nesi

   Pages 54-67

7. Verifying properties of large sets of processes with network invariants

   • Pierre Wolper, Vinciane Lovinfosse

   Pages 68-80

8. A method for verification of trace and test equivalence

   • Ivan Christoff

   Pages 81-88

9. Projections of the reachability graph and environment models

   • Heiko Krumm

   Pages 89-96

10. Proving properties of elementary net systems with a special-purpose theorem prover

    • Heikki Tuominen

    Pages 97-104

11. Verification by abstraction and bisimulation

    • Han Zuidweg

    Pages 105-116

12. MEC : a system for constructing and analysing transition systems

    • André Arnold

    Pages 117-132

13. Fair SMG and linear time model checking

    • Howard Barringer, Michael D. Fisher, Graham D. Gough

    Pages 133-150

14. Network grammars, communication behaviors and automatic verification

    • Ze'ev Shtadler, Orna Grumberg

    Pages 151-165

15. CCS, liveness, and local model checking in the linear time mu-calculus

    • Colin Stirling, David Walker

    Pages 166-178

16. Implementing a model checking algorithm by adapting existing automated tools

    • Bengt Jonsson, Ahmed Hussain Khan, Joachim Parrow

    Pages 179-188

17. On-line model-checking for finite linear temporal logic specifications

    • Claude Jard, Thierry Jeron

    Pages 189-196

18. Timing assumptions and verification of finite-state concurrent systems

    • David L. Dill

    Pages 197-212

19. Specifying, programming and verifying real-time systems using a synchronous declarative language

    • N. Halbwachs, D. Pilaud, F. Ouabdesselam, A-C. Glory

    Pages 213-231

20. Modal specifications

    • Kim Guldstrand Larsen

    Pages 232-246

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 real-time systems.

• Automat
• Realzeitbetrieb
• Spezifikation (Software)
• Verifikation
• automata
• communication
• real-time
• tools
• verification

Policies and ethics