Advertisement

Verification for robust specification

  • Doron Peled
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1275)

Abstract

The choice of a specification formalism for describing properties of concurrent systems is influenced by several factors. Two of them are adequate expressiveness and the availability of verification tools. A factor that is less often taken into consideration is the ability to provide robust specification. Informally, robust specifications cannot distinguish between behaviors that are essentially the same. The use of robust specifications can also provide some more practical advantages such as more manageable proof systems or more efficient automatic verification algorithms. We will present a formal definition for robustness in the framework of linear temporal logic, describe an algorithm for deciding robustness, and demonstrate how the knowledge of robustness can be exploited for verifying program correctness.

Keywords

Model Check Temporal Logic Proof System Transition Sequence Linear Temporal Logic 
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.
    R. Alur, K. McMillan, D. Peled, Deciding Global Partial-Order Properties, submitted for publication.Google Scholar
  2. 2.
    R. Alur, D. Peled, W. Penczek, Model-Checking of Causality Properties, 10th Symposium on Logic in Computer Science, IEEE, 1995, San Diego, USA, 90–100.Google Scholar
  3. 3.
    P. Godefroid, D. Pirottin, Refining dependencies improves partial order verification methods, 5th Conference on Computer Aided Verification, LNCS 697, Elounda, Greece, 1993, 438–449.Google Scholar
  4. 4.
    P. Godefroid, P. Wolper, A Partial Approach to Model Checking, 6th Annual IEEE Symposium on Logic in Computer Science, 1991, Amsterdam, 406–415.Google Scholar
  5. 5.
    S. Katz, D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, Distributed Computing 6 (1992), 107–120. A preliminary version appeared in Temporal Logic in Specification, UK, 1987, LNCS 398, 21–43.Google Scholar
  6. 6.
    L. Lamport, What good is temporal logic, Information Processing 83, Elsevier Science Publishers, 1983, 657–668.Google Scholar
  7. 7.
    Z. Manna, A. Pnueli, How to Cook a Temporal Proof System for Your Pet Language. Proceedings of the 10th ACM Symposium on Principles on Programming Languages, Austin, Texas, 1983, 141–151.Google Scholar
  8. 8.
    A. Mazurkiewicz, Trace Theory, Advances in Petri Nets 1986, Bad Honnef, Germany, LNCS 255, Springer, 1987, 279–324.Google Scholar
  9. 9.
    D. Peled, All from one, one for all, on model-checking using representatives, 5th Conference on Computer Aided Verification, Greece, 1993, LNCS, Springer, 409–423.Google Scholar
  10. 10.
    D. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8 (1996), 39–64.Google Scholar
  11. 11.
    D. Peled, A. Pnueli, Proving partial order properties. Theoretical Computer Science 126, 143–182, 1994.Google Scholar
  12. 12.
    D. Peled, Th. Wilke, Stutter-Invariant Temporal Properties are Expressible without the Nexttime Operator, submitted for publication.Google Scholar
  13. 13.
    D. Peled, Th. Wilke, P. Wolper, An Algorithmic Approach for Checking Closure Properties of ω-Regular Languages, to appear in CONCUR'96, 7th International Conference on Concurrency Theory, Piza, Italy, August 1996.Google Scholar
  14. 14.
    A. Pnueli, The temporal logic of programs, 18th FOGS, IEEE Symposium on Foundation of Computer Science, 1977, 46–57.Google Scholar
  15. 15.
    W. Thomas, Automata on Infinite Objects, in J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B, Elsevier, 1990, 133–191.Google Scholar
  16. 16.
    P.S. Thiagarajan, I. Walukiewicz, An Expressively Complete Linear Time Temporal Logic for Mazurkeiwicz Traces, Logic in Computer Science, 1997, Warsaw, Poland.Google Scholar
  17. 17.
    A. Valmari, Stubborn sets for reduced state space generation, 10th International Conference on Application and Theory of Petri Nets, Bonn, Germany, 1989, LNCS 483, Springer Verlag, 491–515.Google Scholar
  18. 18.
    A.P. Sistla, M.Y. Vardi, P. Wolper, The Complementation Problem for Büchi Automata with Applications to Temporal Logic, Theoretical Computer Science, 49 (1987), 217–237.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Doron Peled
    • 1
  1. 1.Bell LaboratoriesMurray HillUSA

Personalised recommendations