Implementing an LTL-to-Büchi translator in Erlang: a protest experience report

ABSTRACT

In order to provide a nice user experience in McErlang, a model checker for Erlang programs, we needed an LTL-to-Büchi translator. This paper reports on our experiences implementing a translator in Erlang using well known algorithms described in literature. We followed a property driven development schema, where QuickCheck properties were formulated before writing the implementation. We successfully implement an LTL-to-Büchi translator, where the end result performs on par (or better) than two well known reference implementations.

References

1. Thomas Arts, Laura M. Castro, and John Hughes. Testing Erlang data types with Quviq QuickCheck. In ERLANG '08: Proc. of the 7th ACM SIGPLAN workshop on ERLANG, pages 1--8, New York, NY, USA, 2008. ACM.
2. Kent Beck. Test-driven development : by example. Addison-Wesley, Boston, MA, 2003.
3. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method. and Philos. Sci., 1960.
4. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8 (2): 244--263, 1986.
5. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 2000.
6. C. Benac Earle, L-Å. Fredlund, J. A. Iglesias, and A. Ledezma. Verifying Robocup teams. In Proc. 5th International Workshop, Mochart 2008, pages 34--48. Springer, 2008.
7. K. Etessami and G. Holzmann. Optimizing Büchi automata. In CONCUR '00: Proc. of the 11th International Conference on Concurrency Theory, pages 153--167, London, UK, 2000. Springer-Verlag.
8. McVodka L-Å. Fredlund and J.J. Sánchez Penas. Model checking a VoD server using McErlang. In In proceedings of the 2007 Eurocast conference, Feb 2007.
9. L-Å. Fredlund and H. Svensson. McErlang: A model checker for a distributed functional programming language. In Proc. of International Conference on Functional Programming (ICFP). ACM SIGPLAN, 2007.
10. P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In CAV '01: Proc. of the 13th International Conference on Computer Aided Verification, pages 53--65, London, UK, 2001. Springer-Verlag.
11. R. Gerth, D. A. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pages 3--18, London, UK, UK, 1996. Chapman & Hall, Ltd.
12. D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In FORTE '02: Proc. of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, pages 308--326, London, UK, 2002. Springer-Verlag.
13. T. A. Henzinger, O. Kupferman, and S. K. Rajamani. Fair simulation. In Information and Computation, pages 273--287. Springer-Verlag, 1997.
14. J. Hughes. QuickCheck testing for fun and profit. In Michael Hanus, editor, Practical Aspects of Declarative Languages, volume 4354 of phLNCS, pages 1--32. Springer-Verlag, Berlin Heidelberg, 2007.
15. P. Kanellakis and S. Smolka. CCS expressions, finite state processes, and three problems of equivalence. In PODC '83: Proc. of the second annual ACM symposium on Principles of distributed computing, pages 228--240, New York, NY, USA, 1983. ACM.
16. McErlang -- https://babel.ls.fi.upm.es/trac/McErlang/. (Web page, 2009).
17. A. Pnueli. The temporal logic of programs. In Foundations of Computer Science, 1977., 18th Annual Symposium on, pages 46--57, Nov 1977.
18. Project -- http://www.protest-project.eu()}ProTestWebProTest Project -- http://www.protest-project.eu. (Web page, 2009).
19. J-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th Colloquium on International Symposium on Programming, pages 337--351, London, UK, 1982. Springer-Verlag.
20. R. Sebastiani and S. Tonetta. "more deterministic" vs. "smaller" Büchi automata for efficient LTL model checking. In ph12th IFIP WG 10.5 Advanced Research Working Conference, CHARME. Springer-Verlag, 2003.
21. F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In CAV '00: Proc. of the 12th International Conference on Computer Aided Verification, pages 248--263, London, UK, 2000. Springer-Verlag.
22. H. Svensson and L-Å. Fredlund. A more accurate semantics for distributed Erlang. In Erlang '07: Proc. of the 2007 SIGPLAN workshop on Erlang Workshop, pages 43--54, New York, NY, USA, 2007. ACM.
23. H. Tauriainen and K. Heljanko. Testing LTL formula translation into Büchi automata. STTT, 4 (1): 57--70, 2002.
24. Heikki Tauriainen. lbtt 1.0.0 -- an LTL-to-Büchi translator testbench. Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2001. Software.
25. M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Proc. of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata, pages 238--266, Secaucus, NJ, USA, 1996. Springer-Verlag New York, Inc.
26. Moshe Y. Vardi. The Büchi complementation saga. In STACS 2007, volume 4393 of Lecture Notes in Computer Science, pages 12--22. Springer Berlin / Heidelberg, 2007.
27. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st IEEE Symposium on Logic in Computer Science (LICS'96), pages 332--344, New York, 1986. IEEE Computer.
28. Pierre Wolper, Moshe Y. Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths. In Foundations of Computer Science, 1983., 24th Annual Symposium on, pages 185--194, Nov. 1983.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging