PICASSO: a PI-CAlculus-based Static SOftware analyzer

Manual

Dependencies

To compile and run Picasso from the sources you will need sbt 0.12 (or a more recent version).

When proving termination of depth-bounded processes Picasso uses the additional tools: ARMC, Princess, Z3

Overview

Picasso is a tool for reachability analysis of mobile processes. From a technical perspective Picasso focuses on depth-bounded processes (a subset of the π-calculus) and the problem it tries to solve of the control-state reachability (or covering) problem. The core algorithm is a saturation algorithm based on forward exploration of the state-space with widening.

Picasso has currently one main frontend that works on graph rewriting systems. Additional frontends are for a simple actor language (with boolean variables and names as data) and for the Scala language (as a compiler plug-in).

How to run the graph rewriting system version

Picasso can directly reads graph rewriting systems. This version offers a greater degree of flexibility but can quite painful to write by hand. When using Picasso from the SVN repository the runGraph.sh script run Picasso with for graph rewriting systems. The script takes as argument one input file, and computes the cover of the graph rewriting system contained in the file. It is possible to get more details of the computation using the -v option (twice for debug output). The result can be saved in an html report using the -r option.

BNF grammar of the graph rewriting systems

A node consists of an identifier and a label. The identifier is unique to the node. On the other hand many nodes can have the same label. In case the label is not known, it is possible to have a special wildcard label (denoted _). Furthermore, it is possible to specify the multiplicity (nesting depth) of a node using *.

An edge is given by a pair of nodes. Optionally, the edge can be labelled.

A graph is given by a sequence of edges. In case a node is not connected, it can be declared by prefixing it with "node".

A mapping is a dictionary between nodes identifiers. It is given by a sequence of pairs.

A transition transform a subgraph (pre) into another one (post). The pre is matched within a larger graph (subgraph) and then replaced by the post. To preserve the connections with the rest of the graph during the replacement, the nodes in pre and post need to be connected by mappings. The forward mapping (==>) maps non-wildcard nodes from pre into non-wildcard nodes of post. The backward mapping (<==) maps wildcard nodes of post to wildcard nodes of pre. It is also possible to specify an inhibitory pattern that prevent the transition from firing.

A system is given by an initial state (a graph), a sequence of transitions, and, optionally, a target state.

Graph rewriting system example

Here is a simple client-server example. The process consists of one single server thread, an environment thread, and an unbounded number of client threads. In each loop iteration of a client, the client non-deterministically chooses to either wait for a response from the server, or to send a new request to the server. Requests are sent asynchronously and carry both the address of the server and the client. In each iteration of the server loop, the server waits for incoming requests and then asynchronously sends a response back to the client using the client's address received in the request. The environment thread models the fact that new clients can enter the system at anytime. In each iteration of the environment thread, it spawns a new client thread. The initial state of the system consists only of the server and the environment thread.

init
  (e, env) -> (s, server) [S]

transition "new client" 
pre
  (e, env) -> (s, server) [S]
post
  (e, env) -> (s, server) [S]
  (c, client) -> (s, server) [S]
==>
  e -> e
  s -> s
<==

transition "request" 
pre
  (c, client) -> (s, server) [S]
post
  (c, client) -> (s, server) [S]
  (m, msg) ->  (s, server) [S]
  (m, msg) ->  (c, client) [C]
==>
  s -> s
  c -> c
<==

transition "reply" 
pre
  (m, msg) -> (s, server) [S]
  (m, msg) -> (c, _) [C]
post
  (r, reply) -> (c, _) [C]
  node (s, server)
==>
  s -> s
<==
  c -> c

transition "receive reply" 
pre
  (r, reply) -> (c, _) [C]
post
  node (c, _)
==>
<==
  c -> c

How to run the basic version

The so-called basic input language is a layer of syntactic sugar on top of the π-calculus. The goal is to have an human readable language that looks like some of the simple/early actor languages.

EBNF grammar of the basic frontend

TODO short intro

A literal is either true, false, or a string literal.

A pattern is either a wild card, a literal, an identifier, or a constructor (algebraic data type).

An expression is either a wild card (for undefined values), a literal, an identifier, or a constructor (algebraic data type).

A process is a sequence of statements.

An actor is just a syntactic unit that binds the free parameters occurring in a process.

The initial configuration of the system is a list of actors. Identifiers in the arguments of the actors are assume to be top-level bounds names.

Type system of the basic frontend

TODO

Example

Here is a simple ping-pong example inspired from a scala example. There are two main difference compared to the scala version. First, we do not yet support integers. Therefore, we have replaced the counter by non-deterministic choice. Second, in scala each actor has its own channel. In out language the notions of channels (names) and processes are decoupled like in the π-calculus. Thus, the receive operations has to explicitly specify what it is receiving from.

Ping(self, pong)
  while true do
    select
      case self ? Start() =>
        pong ! Ping(self)
      case self ? SendPing() =>
        pong ! Ping(self)
      case self ? Pong() =>
        if random() then
          self ! SendPing()
        else
          begin
            pong ! Stop();
            exit()
          end

Pong(self)
  while true do
    select
      case self ? Ping(sender) => sender ! Pong()
      case self ? Stop() => exit()

Main()
  begin
    val ping := newChannel();
    val pong := newChannel();
    new Ping(ping, pong);
    new Pong(pong);
    ping ! Start()
  end

initial
  Main()

How to run the scala compiler plug-in

TODO