Abstracting concurrent systems to depth-bounded systems
Concurrent systems are hard to write; they are just as hard to verify. A common strategy to prove properties of these systems automatically consists of using an abstraction algorithm which extracts an abstract model of the system, usually expressed as a very restricted model of computation with decidable properties; then the abstract model is verified using a dedicated model checker. In this talk we will first present Soter, a safety checker for Erlang we built and presented at SAS13. Soter abstracts Erlang programs to Petri Nets and uses BFC to model check the generated net. The limitations of Petri Nets will motivate the use of depth-bounded systems as the target formalism of the abstraction step. Depth-bounded systems (DBS) are a very rich class of systems subsuming many known classes including Petri Nets, but still have useful decidable properties. Unfortunately it is not possible to decide if a process is depth-bounded or not. This makes it difficult to use DBS as an abstract model. We will sketch some ideas attempting to solve this issue. We start from an arbitrary system, not necessarily depth-bounded, and focus on coverability. We start to model check the system as if it were depth-bounded, and abstract it on the fly just when it is needed to ensure the verification will terminate.