Declarative programming for verification: lessons and outlook

ABSTRACT

This paper summarises roughly ten years of experience using declarative programming for developing tools to validate formal specifications. More precisely, we present insights gained and lessons learned while implementing animators and model checkers in Prolog for various specification languages, ranging from process algebras such as CSP to model-based specifications such as Z and B.

REFERENCES

• 1: Alfred V. Aho , Monica S. Lam , Ravi Sethi , Jeffrey D. Ullman, Compilers: Principles, Techniques, and Tools (2nd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 2: F. Ambert, F. Bouquet, S. Chemin, S. Guenaud, B. Legeard, F. Peureux, M. Utting, and N. Vacelet. BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In Proceedings of FATES'02, Formal Approaches to Testing of Software, pages 105--120, August 2002.
• 3: Krzysztof R. Apt, Logic programming, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 4: Joe Armstrong, A history of Erlang, Proceedings of the third ACM SIGPLAN conference on History of programming languages, p.6-1-6-26, June 09-10, 2007, San Diego, California [doi>10.1145/1238844.1238850]
• 5: B-Core (UK) Ltd, Oxon, UK. B-Toolkit, On-line manual, 1999. Available at http://www.b-core.com/ONLINEDOC/Contents.html.
• 6: J. Bendisposto and M. Leuschel. BE4: The B extensible eclipse editing environment. In Proceedings of the 7th International B Conference (B2007), LNCS 4355, pages 270--273, Besancon, France, 2007. Springer-Verlag.
• 7: Béatrice Bérard , Laurent Fribourg, Reachability Analysis of (Timed) Petri Nets Using Real Arithmetic, Proceedings of the 10th International Conference on Concurrency Theory, p.178-193, August 24-27, 1999
• 8: Fabrice Bouquet , Bruno Legeard , Fabien Peureux, CLPS-B - A Constraint Solver for B, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.188-204, April 08-12, 2002
• 9: J. Bowen. Animating the semantics of VERILOG using Prolog. Technical Report UNU/IIST Technical Report no. 176, United Nations University, Macau, 1999.
• 10: M. Butler and M. Leuschel. Combining CSP and B for specification and property verification. In Proceedings of Formal Methods 2005, LNCS 3582, pages 221--236, Newcastle upon Tyne, 2005. Springer-Verlag.
• 11: Mats Carlsson , Greger Ottosson , Björn Carlson, An Open-Ended Finite Domain Constraint Solver, Proceedings of the9th International Symposium on Programming Languages: Implementations, Logics, and Programs: Including a Special Trach on Declarative Programming Languages in Education, p.191-206, September 03-05, 1997
• 12: Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996 [doi>10.1145/227595.227597]
• 13: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 14: M. Codish, B. Demoen, and K. F. Sagonas. Xsb as the natural habitat for general purpose program analysis. In ICLP, page 416, 1997.
• 15: Baoqiu Cui , Yifei Dong , Xiaoqun Du , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan , Abhik Roychoudhury , Scott A. Smolka , David Scott Warren, Logic Programming and Model Checking, Proceedings of the 10th International Symposium on Principles of Declarative Programming, p.1-20, September 16-18, 1998
• 16: G. Delzanno and A. Podelski. Constraint-based deductive model checking. STTT, 3(3):250--270, 2001.
• 17: Berndt Farwer , Michael Leuschel, Model checking object petri nets in prolog, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.20-31, August 24-26, 2004, Verona, Italy [doi>10.1145/1013963.1013970]
• 18: Michael J. Butler , Carla Ferreira, A Process Compensation Language, Proceedings of the Second International Conference on Integrated Formal Methods, p.61-76, November 01-03, 2000
• 19: Formal Systems (Europe) Ltd. Failures-Divergence Refinement - FDR2 User Manual (version 2.8.2).
• 20: M. A. Hewitt , Colin O'Halloran , Chris T. Sennett, Experiences with PiZA, an Animator for Z, Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation, p.37-51, April 03-04, 1997
• 21: P. Hill and J. Gallagher. Meta-programming in logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 421--497. Oxford Science Publications, Oxford University Press, 1998.
• 22: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 23: G. Hutton and E. Meijer. Monadic Parser Combinators. Technical Report NOTTCS-TR-96-4, Department of Computer Science, University of Nottingham, 1996.
• 24: Lawrence King , Gopal Gupta , Enrico Pontelli, Verification of a controller for bart: an approach based on horn logic and denotational semantics, High integrity software, Kluwer Academic Publishers, Norwell, MA, 2001
• 25: Michael Leuschel, Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog, Proceedings of the Third International Symposium on Practical Aspects of Declarative Languages, p.14-28, March 11-12, 2001
• 26: M. Leuschel and M. Butler. ProB: A model checker for B. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME 2003: Formal Methods, LNCS 2805, pages 855--874. Springer-Verlag, 2003.
• 27: Michael Leuschel , Michael Butler, ProB: an automated analysis toolset for the B method, International Journal on Software Tools for Technology Transfer (STTT), v.10 n.2, p.185-203, February 2008 [doi>10.1007/s10009-007-0063-9]
• 28: Michael Leuschel , Helko Lehmann, Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction, Proceedings of the First International Conference on Computational Logic, p.101-115, July 01, 2000
• 29: Michael Leuschel , Helko Lehmann, Solving coverability problems of petri nets by partial deduction, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.268-279, September 20-23, 2000, Montreal, Quebec, Canada [doi>10.1145/351268.351298]
• 30: Michael Leuschel , Bern Martens , Danny De Schreye, Controlling generalization and polyvariance in partial deduction of normal logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.208-258, Jan. 1998 [doi>10.1145/271510.271525]
• 31: Michael Leuschel , Thierry Massart, Infinite State Model Checking by Abstract Interpretation and Program Specialisation, Selected papers from the 9th International Workshop on Logic Programming Synthesis and Transformation, p.62-81, September 22-24, 1999
• 32: M. Leuschel and D. Plagge. Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. In Y. Aït-Ameur, F. Boniol, and V. Wiels, editors, Proceedings Isola 2007, Revue des Nouvelles Technologies de l'Information RNTI-SM-1, pages 73--84, 2007.
• 33: J. W. Lloyd, Foundations of logic programming, Springer-Verlag New York, Inc., New York, NY, 1984
• 34: B. Martens and D. De Schreye. Why untyped non-ground metaprogramming is not (much of) a problem. The Journal of Logic Programming, 22(1):47--99, 1995.
• 35: L. Naish. An introduction to MU-Prolog. Technical Report 82/2, Department of Computer Science, University of Melbourne, Melbourne, Australia, March 1982 (Revised July 1983).
• 36: Ulf Nilsson , Johan Lübcke, Constraint Logic Programming for Local and Symbolic Model-Checking, Proceedings of the First International Conference on Computational Logic, p.384-398, July 01, 2000
• 37: R. L. Pokorny and C. R. Ramakrishnan. Model checking linear temporal logic using tabled logic programming. In Proceedings Tabling in Parsing and Deduction TAPD 2000, Vigo, Spain, September 2000.
• 38: Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Terrance Swift , David Scott Warren, Efficient Model Checking Using Tabled Resolution, Proceedings of the 9th International Conference on Computer Aided Verification, p.143-154, June 22-25, 1997
• 39: P. B. Reintjes and S. Rajgopal. Multi/plex: Prolog tools for formal languages. In LPE, pages 81--87, 1993.
• 40: Armin Rigo, Representation-based just-in-time specialization and the psyco prototype for python, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.15-26, August 24-25, 2004, Verona, Italy [doi>10.1145/1014007.1014010]
• 41: A. W. Roscoe , C. A. R. Hoare , Richard Bird, The Theory and Practice of Concurrency, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 42: Konstantinos Sagonas , Terrance Swift , David S. Warren, XSB as an efficient deductive database engine, Proceedings of the 1994 ACM SIGMOD international conference on Management of data, p.442-453, May 24-27, 1994, Minneapolis, Minnesota, United States
• 43: K. Sagonas, T. Swift, D. S. Warren, J. Freire, P. Rao, B. Cui, E. Johnson, L. de Castro, R. F. Marques, S. Dawson, and M. Kifer. XSB Programmer's Manual. Available at http://xsb.sourceforge.net/.
• 44: J. B. Scattergood. Tools for CSP and Timed-CSP. PhD thesis, Oxford University, 1997.
• 45: Alexander Serebrenik , Tom Schrijvers , Bart Demoen, Improving prolog programs: Refactoring for prolog, Theory and Practice of Logic Programming, v.8 n.2, p.201-215, March 2008 [doi>10.1017/S1471068407003134]
• 46: S. SICS, Kista. SICStus Prolog User's Manual. Available at http://www.sics.se/sicstus.
• 47: Corinna Spermann , Michael Leuschel, ProB gets Nauty: Effective Symmetry Reduction for B and Z Models, Proceedings of the 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, p.15-22, June 17-19, 2008 [doi>10.1109/TASE.2008.33]
• 48: F. Steria, Aix-en-Provence. Atelier B, User and Reference Manuals, 1996. Available at http://www.atelierb.societe.com.
• 49: Edd Turner , Michael Leuschel , Corinna Spermann , Michael Butler, Symmetry Reduced Model Checking for B, Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, p.25-34, June 06-08, 2007 [doi>10.1109/TASE.2007.50]
• 50: Moshe Y. Vardi, Branching vs. Linear Time: Final Showdown, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.1-22, April 02-06, 2001
• 51: M. Winikoff, P. Dart, and E. Kazmierczak. Rapid prototyping using formal specifications. In Proceedings of the 21st Australasian Computer Science Conference, pages 279--294, Perth, Australia, February 1998.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
animation, formal methods, logic programming, model checking, verification