Advertisement

Verification of distributed systems: An experiment

  • Didier Vergamini
Applications Of The Theory Of Automata
Part of the Lecture Notes in Computer Science book series (LNCS, volume 386)

Keywords

Temporal Logic Global System Finite Automaton Concurrent System Verification Method 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BK84]
    J. A. Bergstra and J. W. Klop. A complete inference system for regular processes with silent moves. Technical Report Report CS-R8420, CWI AMSTERDAM, 1984.Google Scholar
  2. [Bou85a]
    G. Boudol. Algèbre de processus et vérification. In Actes du Premier Colloque C 3, 1985.Google Scholar
  3. [Bou85b]
    G. Boudol. Notes on algebraic calculi of processes. In K. Apt Editor, editor, Logics and Models for Concurrent Systems, Springer-Verlag, 1985.Google Scholar
  4. [BS80]
    G. Bochmann and C. Sunshine. Formal methods in communication protocol design. IEEE TRANSACTIONS ON COMMUNICATIONS, 30(4), 1980.Google Scholar
  5. [BT82]
    G. Berthelot and R. Terrat. Petri nets theory for the correctness of protocols. IEEE TRANSACTIONS ON COMMUNICATIONS, 30(12), 1982.Google Scholar
  6. [C*85]
    E. Clarke et al. Using temporal logic for automatic verification of finte state systems. In K. Apt Editor, editor, Logics and Models for Concurrent Systems, Springer-Verlag, 1985.Google Scholar
  7. [Hai82]
    B. Hailpern. Verifying concurrent processes using temporal logic. Lectures Notes in Computer Science, 129, 1982.Google Scholar
  8. [HM85]
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137–161, 1985.CrossRefGoogle Scholar
  9. [Hoa78]
    C.A.R. Hoare. Communicating sequential processes. Communication of the ACM, 21:666–676, 1978.Google Scholar
  10. [Lip75]
    R. Lipton. Reduction: a method of proving properties on parallel programs. Communication of the ACM, 18(12), 1975.Google Scholar
  11. [Mil79]
    R. Milner. Flowgraphs and flow algebras. Journal of the ACM, 26:794–818, 1979.CrossRefGoogle Scholar
  12. [Mil80]
    R. Milner. A Calculus of Communicating Systems. Volume 92 of Lectures Notes in Computer Science, Springer-Verlag, 1980.Google Scholar
  13. [Mil83]
    R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 267–310, 1983.Google Scholar
  14. [Mil84]
    R. Milner. A complete inference system for a class of regular behaviour. Journal of Computer and Systems Sciences, 28:439–466, 1984.CrossRefGoogle Scholar
  15. [Mil86]
    R. Milner. A Complete Axiomatisation for Observational Congruence of Finite-state Behaviours. Technical Report ECS-LFCS-86-8, LFCS University of Edinburgh, 1986.Google Scholar
  16. [Par81]
    D. Park. Concurrency and automata on infinite sequences. Lectures Notes in Computer Science, 104:167–183, 1981.Google Scholar
  17. [Pnu85]
    A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt Editor, editor, Logics and Models for Concurrent Systems, Springer-Verlag, 1985.Google Scholar
  18. [Sif84]
    J. Sifakis. Properties preserving homomorphisms of transition systems. Lectures Notes in Computer Science, 164:458–473, 1984.Google Scholar
  19. [Ste76]
    N. V. Stenning. A data transfert protocol. Computer Networks, 1:99–110, 1976.CrossRefGoogle Scholar
  20. [Ver87]
    D. Vergamini. Vérification de réseaux d'automates finis par équivalences observationnelles: le système AUTO. Thèse de doctorat Sciences, Université de Nice, 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Didier Vergamini
    • 1
  1. 1.CericsValbonne CedexFrance

Personalised recommendations