Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation

TL;DR

This paper introduces a control-flow oriented static analysis framework for actor-based process calculi using abstract interpretation, enabling precise verification of communication behaviors and occurrence counting.

Contribution

It presents a novel control-flow based abstract interpretation approach for actor calculus, improving precision over previous data-flow type systems.

Findings

Able to verify communication properties of actor processes

Supports occurrence counting analysis

Handles complex behavioral interactions

Abstract

The actor model eases the definition of concurrent programs with non uniform behaviors. Static analysis of such a model was previously done in a data-flow oriented way, with type systems. This approach was based on constraint set resolution and was not able to deal with precise properties for communications of behaviors. We present here a new approach, control-flow oriented, based on the abstract interpretation framework, able to deal with communication of behaviors. Within our new analyses, we are able to verify most of the previous properties we observed as well as new ones, principally based on occurrence counting.