Emanuele D'Osualdo
Jonathan Kochems
ABSTRACT
This paper presents Soter, a fully-automatic program analyser and verifier for Erlang modules. The fragment of Erlang accepted by Soter includes the higher-order functional constructs and all the key features of actor concurrency, namely, dynamic and possibly unbounded spawning of processes and asynchronous message passing. Soter uses a combination of static analysis and infinite-state model checking to verify safety properties specified by the user. Given an Erlang module and a set of properties, Soter first extracts an abstract (approximate but sound) model in the form of an actor communicating system (ACS), and then checks if the properties are satisfied using a Petri net coverability checker, BFC. To our knowledge, Soter is the first fully-automatic, infinite-state model checker for a large fragment of Erlang. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties such as mutual-exclusion and boundedness of mailboxes. Though the ACS coverability problem is Expspace-complete, Soter can analyse these problems surprisingly efficiently.
- G. Agha. Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge, MA, USA, 1986. Google Scholar
Digital Library
- J. Armstrong. Erlang. CACM, 53(9):68, 2010. Google ScholarDigital Library
- F. Cesarini and S. Thompson. Erlang Programming - A Concurrent Approach to Software Development. O'Reilly, 2009. Google ScholarDigital Library
- M. Christakis and K. Sagonas. Detection of asynchronous message passing errors using static analysis. PADL, pages 5--18, 2011. Google ScholarDigital Library
- E. D'Osualdo, J. Kochems, and C.-H. L. Ong. Automatic verification of Erlang-style concurrency. Technical report, University of Oxford DCS, 2012. http://mjolnir.cs.ox.ac.uk/soter/soterpaper.pdf.Google Scholar
- L. Fredlund and H. Svensson. McErlang: a model checker for a distributed functional programming language. In ICFP, pages 125--136, 2007. Google ScholarDigital Library
- Q. Guo and J. Derrick. Verification of timed Erlang/OTP components using the process algebra μCRL. In Erlang Workshop, pages 55--64, 2007. Google ScholarDigital Library
- A. Kaiser, D. Kroening, and T. Wahl. Efficient coverability analysis by proof minimization. In CONCUR, 2012. Google ScholarDigital Library
- T. Lindahl and K. Sagonas. Practical type inference based on success typings. In PPDP, pages 167--178, 2006. Google ScholarDigital Library
Index Terms
- Soter: an automatic safety verifier for erlang
Recommendations
A Case Study on Verifying a Supervisor Component Using McErlang
In this paper we present a work in progress on the formal verification of a process supervisor using the McErlang model checker. The process supervisor is an alternative implementation of the standard supervisor behaviour of Erlang/OTP. This ...
Verification of Concurrent Programs Using Petri Net Unfoldings
Verification, Model Checking, and Abstract InterpretationAbstractGiven a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be ...
Model Checking Control Flow Petri Nets Using PAT
ICCSA '13: Proceedings of the 2013 13th International Conference on Computational Science and Its ApplicationsAs a program can be modeled as data structures and control flows, the program verification problem can be reduced into verification of control flows with respect to the program data. Although a control flow can be represented as a Petri Net, the ...
Comments