Advertisement

Unfolding parametric automata

  • Maxcos Veloso Peixoto
  • Laurent Fribourg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1380)

Abstract

In this paper, we describe a method for proving properties of parametric automata. These properties have the form p(L, S) ⟹ ζ(S), where p is a predicate characterizing the automaton, L is a list of parametric actions accepted by the automaton, S is a parametric state, and ζ a logic formula. In previous work, we proposed a bottom-up evaluation process for computing the set of all the consequences of p(L,S), then showing that it contains ζ(S). Such forward reasoning methods often do not terminate. We propose here instead a backward reasoning method which is driven by the conclusion ζ. The method consists essentially in transforming the program defining p by unfolding all the recursive clauses that do not leave invariant ζ. We have successfully applied this method to the verification of some functional properties of a parametric sliding window protocol.

Keywords

Logic Program Finite State Automaton Recursive Rule Arithmetic Formula Arithmetical Constraint 
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. 1.
    A. Arnold. “Verification and Comparison of Transition Systems”, Proc. TAPSOFT, 1993, pp.121–135.Google Scholar
  2. 2.
    A. Arnold and M. Nivat. “Comportements de processus”, Colloque AFCET “Les Mathematiques de l'Informatique”, 1982, pp. 35–68.Google Scholar
  3. 3.
    P. Azema et. al. “Specification and Verification of Distributed Systems using Prolog Interpreted Petri Nets”, Proc. of 7 th International Conference on Software Eng., 1984, Orlando.Google Scholar
  4. 4.
    G. Bochmann, R. Dssouli and W. Lopes de Souza. “Use of Prolog for Building Protocol Design Tools”, Proc. of the IFIP WG 6.1 5th Intl. Workshop on Protocol Specification, Testing and Verification, North-Holland, 1985, Toulouse-Moissac, pp.131–145.Google Scholar
  5. 5.
    P. Cousot and R. Cousot. “Abstract Interpretation: A Unified Lattice Model for Static Analysis Of Programs by Construction or Approximation of Fixpoints”, Conference Record of the 4th ACM Symposium on Programming Languages, 1977, Paris.Google Scholar
  6. 6.
    R. Dssouli and G. Bochmann. “Error Detection with Multiple Observers”, Proc. of the IFIP WG 6.1 5 th Intl. Workshop on Protocol Specification, Testing and Verification, North-Holland, 1985, Toulouse-Moissac, pp.483–494.Google Scholar
  7. 7.
    L. Fribourg. “Mixing List Recursion and Arithmetic”. Proc. 7 th IEEE Symp. on Logic in Computer Science, Santa Cruz, 1992, pp. 419–429.Google Scholar
  8. 8.
    L. Fribourg and M. Veloso Peixoto. “Concurrent Constraint Automata”, Technical Report LIENS 93-10, Ecole Normale Supérieure, May 1993 (poster presented at ILPS, 1993, Vancouver).Google Scholar
  9. 9.
    H. Garavel. “Protocole à FenÊtre Glissante”, Unpublished manuscript”, 1992.Google Scholar
  10. 10.
    G. Jard, J.F. Monin and R. Groz. “Experience in Implementing X.250 (a CCITT subset of Estelle) in VEDA”, Proc. of the IFIP WG 6.1 5th Intl. Workshop on Protocol Specification, Testing and Verification, North-Holland, 1985, Toulouse-Moissac, pp.483–494. pp.315–331.Google Scholar
  11. 11.
    L. Naish. “Verification of Logic Programs and Imperative Programs”, Constructing Logic Programs, J.M. Jacquet (ed.), Wiley, 1993, pp.143–164.Google Scholar
  12. 12.
    P. Revesz. “A Closed Form for Datalog Queries with Integer Order”. Proc. 3rd International Conference on Database Theory, Paris, 1990, pp. 187–201.Google Scholar
  13. 13.
    J. Richier, C. Rodriguez, J. Sifakis and J. Voiron. “Verification in XESAR of the Sliding Window Protocol”, Proc. of the IFIP WG 6.1 7 th Intl. Workshop on Protocol Specification, Testing and Verification, North-Holland, 1987, pp.235–248.Google Scholar
  14. 14.
    H. Tamaki, T. Sato. “Unfold/Fold Transformations of Logic Programs”. Proc. 2 th International Logic Programming Conference, Uppsala, 1984, pp. 127–138.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Maxcos Veloso Peixoto
    • 1
  • Laurent Fribourg
    • 2
  1. 1.U.F.F.Niterói, R.J.Brazil
  2. 2.L.I.E.N.S (URA 1327 CNRS)ParisFrance

Personalised recommendations