Systems with procedures

The Edinburgh site has worked on the verification of systems with (possible recursive and mutually recursive) procedures [ES01c,EKS01]. They can be seen as automata extended with one stack. In the presence of recursion the size of the stack may grow arbitrarily, and so the system may exhibit an infinite state space. In the absence of recursion, procedure calls can in principle be replaced by the body of the procedure (inlining), yielding a flat systems; however, this may make the size of the system blow-up.

In the protocols area this work finds two applications:

• Large protocols, like some of the studied by the Grenoble site, make extensive use of procedures (usually non recursive).
• Functional languages like Erlang, used by Ericsson to implement protocols, are inherently recursive. Any model-checking approach requires modeling the stack.

In [ES01c], one presents a model-checker for Boolean programs with (possibly recursive) procedures and the temporal logic LTL. The checker is guaranteed to terminate even for (usually faulty) programs in which the depth of the recursion is not bounded. The algorithm uses automata to finitely represent possibly infinite sets of stack contents and BDDs to compactly represent finite sets of values of Boolean variables. The checker is illustrated with some examples, and compared with the Bebop tool of Ball and Rajamani.

In [EKS01], one examines an extension of the model-checking problem for LTL, namely model-checking with regular valuations. The problem is solved via two different techniques, with an eye on efficiency -- both techniques can be shown to be essentially optimal. These methods are applicable to problems in different areas, e.g., data flow analysis, analysis of systems with checkpoints, etc., and provide a general, unifying and efficient framework for solving these problems.

The problem of analyzing programs based on recursive procedures is also addressed in [BHM01]. This paper introduces a more refined model called BPA(Z) that can model not only recursive dependencies, but also the passing of an integer parameter to subroutines. Moreover, this parameter can be tested against conditions expressible in Presburger-arithmetic. This new and more expressive model can still be analyzed automatically. The authors define Z-input 1-CM, a new class of one-counter machines that take integer numbers as input, to describe sets of configurations of BPA(Z). It is shown that the ${\it Post}^*$ (the set of successors) of a set of BPA(Z)-configurations described by a Z-input 1-CM can be effectively constructed. The ${\it Pre}^*$ (set of predecessors) of a regular set can be effectively constructed as well. However, the ${\it Pre}^*$ of a set described by a Z-input 1-CM cannot be represented by a Z-input 1-CM in general and has an undecidable membership problem. The paper then develops a new temporal logic based on reversal-bounded counter machines that can be used to describe properties of BPA(Z), and shows that the model-checking problem is decidable for that logic.