Skip to main content
SpringerLink
Log in

Verification of Temporal Properties of Processes in a Setting with Data

  • Conference paper
  • First Online:
Book cover Algebraic Methodology and Software Technology (AMAST 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1548))

Abstract

We define a value-based modal µ-calculus, built from firstorder formulas, modalities, and fixed point operators parameterized by data variables, which allows to express temporal properties involving data. We interpret this logic over µCrl terms defined by linear process equations. The satisfaction of a temporal formula by a µCrl term is translated to the satisfaction of a first-order formula containing parameterized fixed point operators. We provide proof rules for these fixed point operators and show their applicability on various examples.

This work has been funded by the grant no. 97-09 of the Ercim fellowship programme for collaboration between Inria and Cwi.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andersen, H.R.: Model Checking and Boolean Graphs. Theoretical Computer Science, 126(1):3–30, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  2. Arnold, A., Crubillé, P.: A Linear Algorithm to Solve Fixed-Point Equations on Transition Systems. Information Processing Letters, 29:57–66, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  3. Bezem, M.A., Groote, J.F.: Invariants in Process Algebra with Data. In: Jonsson, B., Parrow, J. (eds.): Proceedings of CONCUR’94 (Uppsala, Sweden), LNCS 836, pp. 401–416, Springer Verlag, 1994.

    Google Scholar 

  4. Bezem, M.A., Groote, J.F.: A Correctness Proof of a One Bit Sliding Window Protocol in µcrl. The Computer Journal, 37(4):289–307, 1994.

    Article  Google Scholar 

  5. Bosscher, D., Ponse, A.: Translating a Process Algebra with Symbolic Data Values to Linear Format. In: Engberg, U.H., Larsen, K.G., Skou, A. (eds.), Proceedings of TACAS’95 (Aarhus, Denmark), BRICS Notes Series, pp. 119–130, University of Aarhus, 1995.

    Google Scholar 

  6. van Dalen, D.: Logic and Structure. Springer Verlag, 1994.

    Google Scholar 

  7. Dam, M.: Model Checking Mobile Processes. Information and Computation, 129:35–51, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  8. Fredlund, L.-Ä., Groote, J.F., Korver, H.: Formal Verification of a Leader Election Protocol in Process Algebra. Theoretical Computer Science, 177:459–486, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  9. Groote, J.F.: A Note on n Similar Parallel Processes. In: Gnesi, S., Latella, D. (eds.), Proceedings of the 2nd ERCIM Int. Workshop on Formal Methods for Industrial Critical Systems (Cesena, Italy), pp. 65–75, 1997. (See also Report CS-R9626, CWI, Amsterdam, 1996).

    Google Scholar 

  10. Groote, J.F., Mateescu, R.: Verification of Temporal Properties of Processes in a Setting with Data. Technical Report SEN-R9804, CWI, Amsterdam, 1998.

    Google Scholar 

  11. Groote, J.F., Monin, F., Springintveld, J.: A Computer Checked Algebraic Verification of a Distributed Summing Protocol. Computer Science Report 97/14, Dept. of Math. and Comp. Sci., Eindhoven University of Technology, 1997.

    Google Scholar 

  12. Groote, J.F., van de Pol, J.C.: A Bounded Retransmission Protocol for Large Data Packets. A Case Study in Computer Checked Verification. In: Wirsing, M., Nivat, M. (eds.), Proceedings of AMAST’96 (Munich, Germany), LNCS 1101, pp. 536–550, Springer Verlag, 1996.

    Google Scholar 

  13. Groote, J.F., Ponse, A.: The Syntax and Semantics of πCRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.), Algebra of Communicating Processes, Workshops in Computing, pp. 26–62, 1994.

    Google Scholar 

  14. Groote, J.F., Springintveld, J.: Focus Points and Convergent Process Operators. A Proof Strategy for Protocol Verification. Technical Report 142, Logic Group Preprint Series, Utrecht University, 1995. (See also Technical Report CS-R9566, CWI, Amsterdam, 1995).

    Google Scholar 

  15. Kindler, A., Reisig, W., Völzer, H., Walter, R.: Petri Net Based Verification of Distributed Algorithms: an Example. Formal Aspects of Computing, 9:409–424, 1997.

    Article  MATH  Google Scholar 

  16. Kozen, D.: Results on the Propositional µ-calculus. Theoretical Computer Science 27, pp. 333–354, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  17. Manna, Z., Pnueli, A.: Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs. Science of Computer Programming 32:257–289, 1984.

    Article  MathSciNet  Google Scholar 

  18. Queille, J-P., Sifakis, J.: Fairness and Related Properties in Transition Systems — a Temporal Logic to Deal with Fairness. Acta Informatica, 19:195–220, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  19. Rathke, J., Hennessy, M.: Local Model Checking for a Value-Based Modal µ-calculus. Technical Report 5/96, School of Cognitive and Computing Sciences, University of Sussex, 1996.

    Google Scholar 

  20. Shankland, C.: The Tree Identify Protocol of IEEE 1394. In: Groote, J.F., Luttik, B., van Wamel, J. (eds.), Proceedings of the 3rd ERCIM Int. Workshop on Formal Methods for Industrial Critical Systems (Amsterdam, The Netherlands), pp. 299–319, 1998.

    Google Scholar 

  21. Tarski, A.: A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics 5, pp. 285–309, 1955.

    MATH  MathSciNet  Google Scholar 

  22. Vergauwen, B., Lewi, J.: A Linear Algorithm for Solving Fixed-Point Equations on Transition Systems. Proceedings of CAAP’92 (Rennes, France), LNCS 581, pp. 322–341, Springer Verlag, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cwi, P.O. Box 94079, NL-1090 GB, Amsterdam, The Netherlands

    Jan Friso Groote

  2. Eindhoven University of Technology, P.O. Box 513, NL-5600 MB, Eindhoven, The Netherlands

    Jan Friso Groote

  3. Inria Rhône-Alpes / VASY group, 655, avenue de l’Europe, F-38330, Montbonnot Saint Martin, France

    Radu Mateescu

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Informática, Pontifícia Laboratório de Métodos Formais, Universidade Católica do Rio de Janeiro, Rua Marquês De São Vicente, 225, 22453-900, Rio de Janeiro, RJ, Brazil

    Armando M. Haeberer

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Groote, J.F., Mateescu, R. (1998). Verification of Temporal Properties of Processes in a Setting with Data. In: Haeberer, A.M. (eds) Algebraic Methodology and Software Technology. AMAST 1999. Lecture Notes in Computer Science, vol 1548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49253-4_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-49253-4_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65462-9

  • Online ISBN: 978-3-540-49253-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation