Skip to main content
SpringerLink
Log in

Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog

  • Conference paper
  • First Online:
Practical Aspects of Declarative Languages (PADL 2001)

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

Included in the following conference series:

Abstract

We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing, prototyping, and animating new specification languages. In particular, we present the new high-level specification language CSP(LP), unifying CSP with concurrent (constraint) logic programming, and which we hope can be used to formally reason both about logical and concurrent aspects of critical systems.

“Automated validation of Business Critical systems using Component-based Design,” EPSRC grant GR/M91013, with industrial collaborators IBM, ICL, Praxis Critical Systems, and Roke Manor Research.

“Infinite state MOdel Checking using partial evaluation and abstract interpretation,” EPSRC grant GR/N11667.

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. J.-R. Abrial. The B-Book. Cambridge University Press, 1996.

    Google Scholar 

  2. B. Bérard and L. Fribourg. Reachability analysis of (timed) petri nets using real arithmetic. In Proceedings of Concur’99, LNCS 1664, pages 178–193. Springer-Verlag, 1999.

    Google Scholar 

  3. J. Bowen. Animating the semantics of VERILOG using Prolog. Technical Report UNU/IIST Technical Report no. 176, United Nations University, Macau, 1999.

    Google Scholar 

  4. M. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing. To appear.

    Google Scholar 

  5. C. Consel and R. Marlet. Architecturing software using: A methodology for language development. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Proceedings of ALP/PLILP’98, LNCS 1490, pages 170–194. Springer-Verlag, 1998.

    Google Scholar 

  6. B. Cui, Y. Dong, X. Du, N. Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, A. Roychoudhury, S. A. Smolka, and D. S. Warren. Logic programming and model checking. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Proceedings of ALP/PLILP’98, LNCS 1490, pages 1–20. Springer-Verlag, 1998.

    Google Scholar 

  7. G. Delzanno and A. Podelski. Model checking in clp. In R. Cleaveland, editor, Proceedings of TACAS’99, LNCS 1579, pages 223–239. Springer-Verlag, 1999.

    Google Scholar 

  8. C. Ferreira and M. Butler. A process compensation language. In Proceedings IFM’2000, LNCS 1945, pages 61–76. Springer-Verlag, 2000.

    Google Scholar 

  9. Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 User Manual.

    Google Scholar 

  10. J. Gallagher. A system for specialising logic programs. Technical Report TR-91-32, University of Bristol, November 1991.

    Google Scholar 

  11. G. Gupta. Horn logic denotations and their applications. In The Logic Programming Paradigm: A 25 year perspective, pages 127–160. Springer-Verlag, April 1998.

    Google Scholar 

  12. S. Haridi, P. Van Roy, P. Brand, and C. Schulte. Programming languages for distributed applications. New Generation Computing, 16(3):223–261, 1998.

    Google Scholar 

  13. P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin, A. Smith, U. Ultes-Nitsche, and B. Walters. Questions and answers about ten formal methods. Technical report, Trento, Italy, July 1999. Extended version as technical report DSSE-TR-99-1, University of Southampton.

    Google Scholar 

  14. P. Henderson. Modelling architectures for dynamic systems. Technical report, University of Southampton, December 1999. Available at http://www.ecs.soton.ac.uk/~ph/arc.htm.

  15. C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

    Google Scholar 

  16. G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

  17. D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyzer. In Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.

    Google Scholar 

  18. J. Jørgensen and M. Leuschel. Efficiently generating efficient generating extensions in Prolog. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, International Seminar, LNCS 1110, pages 238–262, Schloß Dagstuhl, 1996. Springer-Verlag.

    Google Scholar 

  19. L. King, G. Gupta, and E. Pontelli. Verification of Bart controller: An approach based on horn logic and denotational semantics. submitted, 2000.

    Google Scholar 

  20. R. S. Lazic. A semantic study of data-independence with applications to the mechanical verification of concurrent systems. PhD thesis, Oxford University, 1997.

    Google Scholar 

  21. M. Leuschel and H. Lehmann. Solving coverability problems of Petri nets by partial deduction. In M. Gabbrielli and F. Pfenning, editors, Proceedings of PPDP’2000, pages 268–279. ACM Press, 2000.

    Google Scholar 

  22. M. Leuschel, B. Martens, and D. De Schreye. Controlling generalisation and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems, 20(1):208–258, January 1998.

    Article  Google Scholar 

  23. M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialisation. In A. Bossi, editor, Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR’99, LNCS 1817, pages 63–82, Venice, Italy, September 1999.

    Chapter  Google Scholar 

  24. R. Milner. Communication and Concurrency. Prentice Hall, 1989.

    Google Scholar 

  25. U. Nilsson and J. Lübcke. Constraint logic programming for local and symbolic model checking. In J. Lloyd, editor, Proceedings of CL’2000, LNAI 1861, pages 384–398, London, UK, 2000. Springer-Verlag.

    Google Scholar 

  26. J. C. Peralta, J. P. Gallagher, and H. Saglam. Analysis of imperative programs through analysis of constraint logic programs. In G. Levi, editor, Static Analysis. Proceedings of SAS’98, LNCS 1503, pages 246–261, Pisa, Italy, September 1998. Springer-Verlag.

    Chapter  Google Scholar 

  27. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In O. Grumberg, editor, Proceedings of CAV’97, LNCS 1254, pages 143–154. Springer-Verlag, 1997.

    Google Scholar 

  28. A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In IEEE Symposium on Foundations of Secure Systems, 1995.

    Google Scholar 

  29. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1999.

    Google Scholar 

  30. D. Sahlin. Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing, 12(1):7–51, 1993.

    Article  MATH  Google Scholar 

  31. J. B. Scattergood. Tools for CSP and Timed-CSP. PhD thesis, Oxford University, 1997.

    Google Scholar 

  32. E. Shapiro. The family of concurrent logic programming languages. ACM Computing Surveys, 21(3):413–510, 1989.

    Article  Google Scholar 

  33. G. Smolka. The Oz programming model. In J. van Leeuwen, editor, Computer Science Today, LNCS 1000, pages 324–343. Springer-Verlag, Berlin, 1995.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electronics and Computer Science, University of Southampton, SO17 1BJ, Highfield, Southampton, UK

    Michael Leuschel

Authors
  1. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, State University of New York, Stony Brook, 11794, NY, USA

    I. V. Ramakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Leuschel, M. (2001). Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog. In: Ramakrishnan, I.V. (eds) Practical Aspects of Declarative Languages. PADL 2001. Lecture Notes in Computer Science, vol 1990. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45241-9_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-45241-9_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41768-2

  • Online ISBN: 978-3-540-45241-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation