Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2008: FM 2008: Formal Methods pp 148–164Cite as

A Model Checking Language for Concurrent Value-Passing Systems

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5014))

Abstract

Modal μ-calculus is an expressive specification formalism for temporal properties of concurrent programs represented as Labeled Transition Systems (Ltss). However, its practical use is hampered by the complexity of the formulas, which makes the specification task difficult and error-prone. In this paper, we propose Mcl (Model Checking Language), an enhancement of modal μ-calculus with high-level operators aimed at improving expressiveness and conciseness of formulas. The main Mcl ingredients are parameterized fixed points, action patterns extracting data values from Lts actions, modalities on transition sequences described using extended regular expressions and programming language constructs, and an infinite looping operator specifying fairness. We also present a method for on-the-fly model checking of Mcl formulas on finite Ltss, based on the local resolution of boolean equation systems, which has a linear-time complexity for alternation-free and fairness formulas. Mcl is supported by the Evaluator 4.0 model checker developed within the Cadp verification toolbox.

This is a preview of subscription content, 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

Learn about 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. TCS 126(1), 3–30 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. ANSI. Small Computer System Interface-2. Standard X3.131-1994

    Google Scholar 

  3. Armoni, R., Fix, L., Flaisher, A., et al.: The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Arts, T., Benac Earle, C., Derrick, J.: Development of a Verified Erlang Program for Resource Locking. STTT 5(2–2), 205–220 (2004)

    Google Scholar 

  5. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)

    Google Scholar 

  6. Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)

    Google Scholar 

  7. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  8. Cleaveland, R., Steffen, B.: A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. FMSD 2(2), 121–147 (1993)

    MATH  Google Scholar 

  9. Dam, M.: Model Checking Mobile Processes (Full version). Research Report RR 94:1, Swedish Institute of Computer Science, Kista, Sweden (1994)

    Google Scholar 

  10. De Nicola, R., Vaandrager, F.W.: Action versus State Based Logics for Transition Systems. In: LITP 1990. Lncs, vol. 469, pp. 407–419 (1990)

    Google Scholar 

  11. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: ICSE 1999, pp. 411–420 (1999)

    Google Scholar 

  12. Emerson, E.A., Halpern, J.Y.: Sometimes and Not Never Revisited: On Branching versus Linear Time Temporal Logic. J. ACM 33(1), 151–178 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  13. Emerson, E.A., Lei, C.-L.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In: LICS 1986, pp. 267–278 (1986)

    Google Scholar 

  14. Fischer, M.J., Ladner, R.E.: Propositional Dynamic Logic of Regular Programs. JCSS 18(2), 194–211 (1979)

    MATH  MathSciNet  Google Scholar 

  15. Garavel, H.: OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  16. Garavel, H., Hermanns, H.: On Combining Functional Verification and Performance Evaluation Using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410–429. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Groote, J.F., Willemse, T.A.C.: Parameterised Boolean Equation Systems. TCS 343, 332–369 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  19. Groote, J.F., Mateescu, R.: Verification of Temporal Properties of Processes in a Setting with Data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 74–90. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  20. Halpern, J.Y., Reif, J.H.: The Propositional Dynamic Logic of Deterministic, Wellstructured Programs. TCS 27(1–2), 127–165 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  21. Hamaguchi, K., Hiraishi, H., Yajima, S.: Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. In: CAV 1990. Lncs, vol. 531 (1990)

    Google Scholar 

  22. Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2003)

    Google Scholar 

  23. IEEE. PSL: Property Specification Language. Std. P1850, IEEE (2004)

    Google Scholar 

  24. ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Int. Std. 8807, ISO — OSI, Genève (1989)

    Google Scholar 

  25. Joubert, C., Mateescu, R.: Distributed On-the-Fly Model Checking and Test Case Generation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 126–145. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  26. Kozen, D.: Results on the Propositional μ-calculus. TCS 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  27. Larsen, K.G.: Proof Systems for Hennessy-Milner logic with Recursion. In: Dauchet, M., Nivat, M. (eds.) CAAP 1988. LNCS, vol. 299, pp. 215–230. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  28. Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. In: VERSAL 8, Bertz Verlag, Berlin (1997)

    Google Scholar 

  29. Mateescu, R.: Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus. In: VMCAI 1998. University Ca’Foscari of Venice (1998)

    Google Scholar 

  30. Mateescu, R.: Efficient Diagnostic Generation for Boolean Equation Systems. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 251–265. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  31. Mateescu, R.: CÆSAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems. STTT 8(1), 37–56 (2006)

    Article  MathSciNet  Google Scholar 

  32. Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. SCP 46(3), 255–281 (2003)

    MATH  MathSciNet  Google Scholar 

  33. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  34. Pnueli, A.: A Temporal Logic of Concurrent Programs. TCS 13, 45–60 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  35. 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 

  36. Rathke, J., Hennessy, M.: Local Model Checking for a Value-Based Modal μ-calculus. Report 5/96, Univ. of Sussex (1996)

    Google Scholar 

  37. Salaün, G., Serwe, W., Thonnart, Y., Vivet, P.: Formal Verification of CHP Specifications with CADP — Illustration on an Asynchronous Network-on-Chip. In: ASYNC 2007, pp. 73–82. IEEE, Los Alamitos (2007)

    Google Scholar 

  38. Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)

    Google Scholar 

  39. Streett, R.: Propositional Dynamic Logic of Looping and Converse. Information and Control 54, 121–141 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  40. Tarjan, R.E.: Depth First Search and Linear Graph Algorithms. SIAM J. of Computing 1(2), 146–160 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  41. Thomas, W.: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Lncs, vol. 354

    Google Scholar 

  42. Vergauwen, B., Lewi, J.: A Linear Algorithm for Solving Fixed-Point Equations on Transition Systems. In: Raoult, J.-C. (ed.) CAAP 1992. LNCS, vol. 581, pp. 322–341. Springer, Heidelberg (1992)

    Google Scholar 

  43. Wolper, P.: A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping. Unpublished manuscript (1982)

    Google Scholar 

  44. Wolper, P.: Temporal Logic Can Be More Expressive. Information and Control 56(1/2), 72–99 (1983)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Rhône-Alpes / VASY, 655, avenue de l’Europe, F-38330, Montbonnot, St Martin, France

    Radu Mateescu & Damien Thivolle

Authors
  1. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Damien Thivolle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jorge Cuellar Tom Maibaum Kaisa Sere

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mateescu, R., Thivolle, D. (2008). A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-68237-0_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-68235-6

  • Online ISBN: 978-3-540-68237-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation