Advertisement

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

  • Michael Leuschel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1990)

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.

Keywords

Specification Verification Concurrency Implementation Compilation 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    J.-R. Abrial. The B-Book. Cambridge University Press, 1996.Google Scholar
  2. [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. [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. [4]
    M. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing. To appear.Google Scholar
  5. [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. [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. [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. [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. [9]
    Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 User Manual.Google Scholar
  10. [10]
    J. Gallagher. A system for specialising logic programs. Technical Report TR-91-32, University of Bristol, November 1991.Google Scholar
  11. [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. [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. [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. [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. [15]
    C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
  16. [16]
    G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.Google Scholar
  17. [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. [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. [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. [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. [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. [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.CrossRefGoogle Scholar
  23. [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.CrossRefGoogle Scholar
  24. [24]
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  25. [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. [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.CrossRefGoogle Scholar
  27. [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. [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. [29]
    A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1999.Google Scholar
  30. [30]
    D. Sahlin. Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing, 12(1):7–51, 1993.zbMATHCrossRefGoogle Scholar
  31. [31]
    J. B. Scattergood. Tools for CSP and Timed-CSP. PhD thesis, Oxford University, 1997.Google Scholar
  32. [32]
    E. Shapiro. The family of concurrent logic programming languages. ACM Computing Surveys, 21(3):413–510, 1989.CrossRefGoogle Scholar
  33. [33]
    G. Smolka. The Oz programming model. In J. van Leeuwen, editor, Computer Science Today, LNCS 1000, pages 324–343. Springer-Verlag, Berlin, 1995.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Michael Leuschel
    • 1
  1. 1.Department of Electronics and Computer ScienceUniversity of SouthamptonHighfield, SouthamptonUK

Personalised recommendations