Frank Huch
ABSTRACT
We present an approach for the verification of Erlang programs using abstract interpretation and model checking. In general model checking for temporal logics like LTL and Erlang programs is undecidable. Therefore we define a frame-work for abstract interpretations for a core fragment of Erlang. In this framework it is guaranteed, that the abstract operational semantics preserves all paths of the standard operational semantics. We consider properties that have to hold on all paths of a system, like properties in LTL. If these properties can be proved for the abstract operational semantics, they also hold for the Erlang program. They can be proved with model checking if the abstract operational semantics is a finite transition system. Therefore we introduce a example abstract interpretation, which has this property. We have implemented this approach as a prototype and were able to prove properties like mutual exclusion or the absence of deadlocks and lifelocks for some Erlang programs.
- ANN98.T. Amtoft, H. Riis Nielson, and F. Nielson. Behaviour analysis and safety conditions: A case study in CML. Lecture Notes in Computer Science, 1382:255-269, 1998.]]Google Scholar
Cross Ref
- AWV93.J. Armstrong, M. Williams, and R. Virding. Concurrent Programming in Erlang. Prentice- Hall, Englewood Cliffs, N J, 1993.]] Google ScholarDigital Library
- CC77.P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the ~th A CM Symposium on Principles of Programming Languages, Los Angeles, pages 238-252, New York, NY, 1977. ACM.]] Google ScholarDigital Library
- CPS90.R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In J. Sifakis, editor, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of L NCS, pages 24-37, Berlin, June 1990. Springer.]] Google ScholarDigital Library
- DaF98.M. Darn and L. ~. Fredlund. On the verification of open distributed sy.stems. In Proc. of the A CM Symposium on Applied Computing, 28:532-540, June 1998.]] Google ScholarDigital Library
- DP98.Matthew B. Dwyer and Corina S. Pasareanu. Filter-based model checking of partial systems. In Proceedings of the A CM S~GSOFT Sixth International Symposium on the Foundation of Software Engineering, November 1998.]] Google ScholarDigital Library
- FFKD87.M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52(3):205- 237, 1987.]] Google ScholarDigital Library
- HDL98.J. Hatcliff, M. Dwyer, and S. Laubach. Staging static analyses using abstraction-based program specialization. Lecture Notes in Computer Science, 1490:134-148, 1998.]] Google ScholarDigital Library
- Hol97.G.J. Holzmann. The model checker spin. IEEE Trans. on Software Engineering, 23(5):279-295, May 1997. Special issue on Formal Methods in Software Practice.]] Google ScholarDigital Library
- HP99.K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Trans/er- STTT, to appear, 1999.]]Google Scholar
- Huc99.Frank Huch. Verification of erlang programs using abstract interpretation and model checking - extended version. Technical Report 99-02, RWTH Aachen, 1999.]]Google Scholar
- JN94.Neil D. Jones and Flemming Nielson. Abstract interpretation: a semantics-based tool for program analysis. In Handbook of Logic in Computer Science. Oxford University Press, 1994. 527-629.]] Google ScholarDigital Library
- LP85.Orna Lichtenstein and Amir Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Conference Record o/the Twelfth Annual A CM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, Louisiana, January 13-16, 1985. ACM SIGACT-SIGPLAN, ACM Press.]] Google ScholarDigital Library
- NN97.Hanne Riis Nielson and Flemming Nielson. Communication analysis for concurrent ML. In ML with Concurrency, Monographs in Computer Science, pages 185-235. Springer-Verlag, 1997.]]Google Scholar
- Pel94.D. Peled. Combining partial order reductions with on-the-fly model-checking. Lecture Notes in Computer Science, 818:377-390, 1994.]] Google ScholarDigital Library
- SS98.D. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. Lecture Notes in Computer Science, 1503:351-380, 1998.]]Google ScholarCross Ref
- Var96.M.Y. Vardi. An automata-theoretic approach to linear temporal logic. Lecture Notes in Computer Science, 1043:238ff., 1996.]]Google ScholarCross Ref
Index Terms
- Verification of Erlang programs using abstract interpretation and model checking
Recommendations
Verification of Erlang programs using abstract interpretation and model checking
We present an approach for the verification of Erlang programs using abstract interpretation and model checking. In general model checking for temporal logics like LTL and Erlang programs is undecidable. Therefore we define a frame-work for abstract ...
Abstract Model Checking of tccp programs
The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate to analyze by model checking timing properties of concurrent systems. However, even if ...
A semantic framework for the abstract model checking of tccp programs
Quantitative aspects of programming languages (QAPL 2004)The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if ...
Comments