PRESS: analysis of Process Rewrite Systems

• Introduction
• Examples
• Credits
• Download
• References

PRESS is a tool for computing finite representations of the forward/backward reachable configurations of multi-threaded programs with dynamic creation of processes and (recursive) procedure calls. Such programs are modeled using Process Rewrite Systems. Reachable configurations are computed modulo several term structural equivalences [BT03, Tou03, ST06].

Process Rewrite Systems (PRS for short) [May98] is a finite set of rules of the form t -> t' where t and t' are terms built up from the idle process ("0"), a finite set of process variables ("X"), sequential composition ("·"), and asynchronous parallel composition ("||"). The semantics of PRSs considers terms modulo a structural equivalence (=) which expresses the fact that "0" is a neutral element of "·" and "||", that "·" is associative, and that "||" is associative and commutative. It is easy to see that with this semantics, PRS subsumes well-known models such as pushdown automata and Petri nets. Examples of programs modeled using PRS can be found in [BT03, Tou03, ST06].

PRESS can also analyze O-PRS systems [ST06], which is the extension of PRS with a new parallel operator "O" that is associative but not commutative, and hence it preserves the order between parallel processes. This parallel operator is needed to model programs where the order between parallel processes is important, such as the concurrent lexer described in [ST06].

Unfortunately, while reachability between terms is decidable for PRS [May98], it becomes undecidable for O-PRS due to the associativity of "O" [ST06]. Despite this undecidability, PRESS tackles the reachability problem between two (infinite) sets of terms. Since process terms can be seen as trees, (bottom-up) tree automata are used to represent (infinite) sets of terms. To sidestep the undecidability problem, PRESS proceeds as follows:

• First, it follows the approach used in [BT03, Tou03, ST06] and performs the exact reachability analysis of O-PRS modulo restricted equivalences that omit the associativity of "O" (the cause of undecidability). Indeed, as discussed in [BT03, Tou03], the reachability analysis modulo all the equivalences can be shown in many cases to be reducible to computing representatives of the reachability set modulo some stronger equivalence.
• In case the associativity of "O" cannot be avoided, the tool computes representatives of underapproximations of the reachability sets by allowing the ordered processes to communicate only a fixed number of times k . These approximations enable the discovery of bugs in the system. Then, increasing k allows to compute better underapproximations. Moreover, if for k and k+1 the computed underapproximations are the same, then we know that the tool has computed an exact representative of the reachability set. Note that the computed underapproximations are exact if the ordered processes can only perform a bounded number of communications.

Several toy examples are available in the package (input directory). Moreover, a description of a concurrent lexer can be found in [ST06].

PRESS is written, debugged, maintained and improved by Mihaela Sighireanu and Tayssir Touili.

You can download the PRESS tool via HTTP.

For installing PRESS you need:

• Ocaml 3.04 or greater.
• make for recompiling under Unix.
• Timbuk library (Copyright 2000-2003 Thomas Genet), see http://www.irisa.fr/lande/genet/timbuk/.

ST06

M. Sighireanu and T. Touili, Bounded Communication Reachability Analysis of O-Process Rewrite Systems. In Proc. of 8th International Workshop on Verification of Infinite-State Systems (Infinity'06).

BT03

A. Bouajjani and T. Touili, Reachability Analysis of Process Rewrite Systems. In Proc. Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03).

Tou03

T. Touili, Analyse symbolique de systèmes infinis basée sur les automates: Application à la vérification de systèmes paramétrés et dynamiques. PhD. thesis, 2003.

BT05

A. Bouajjani and T. Touili, On Computing Reachability Sets of Process Rewrite Systems. In Proc. 16th Intern. Conf. on Rewriting Techniques and Applications (RTA'05).

May98

R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Sytems. PhD thesis, 1998.

Last updated: Tue Jul 18 16:19:27 CEST 2006